[Merged by Bors] - feat({tactic + test}/congrm, logic/basic): congrm = congr + pattern-match

[adomani]

This PR defines a tactic congrm. If the goal is an equality, where the sides are "almost" equal, then calling congrm <expr_with_mvars_for_differences> will produce goals for each place where the given expression has metavariables and will try to close the goal assuming all equalities have been proven.

For instance,

example {a b : ℕ} (h : a = b) : (λ y : ℕ, ∀ z, a + a = z) = (λ x, ∀ z, b + a = z) :=
begin
  congrm λ x, ∀ w, _ + a = w,
  exact h,
end

works.

Zulip

Co-authored-by: Gabriel Ebner gebner@gebner.org

---

[eric-wieser]

That zulip link just goes to the channel; can you correct it?

[adomani]

Eric, thanks for noticing: I updated the link and the description of the PR.

[gebner]

A key feature of the congr tactic is that it uses the automatically generated congruence lemmas (mk_specialized_congr_lemma). This is what allows it to ignore subsingleton arguments and rewrite in dependent positions. For example on ite p a b = ite q a b we want the subgoal p = q but we cannot rw with p = q. Similarly on ite p a b = by classical; exact p a c we want the subgoal b = c but this requires knowing that decidable p is a subsingleton.

In other words, equate_with_pattern should do something like apply_eq_congr_core, except compute the congruence lemma from the pattern instead of the lhs.

It would also be cool if congr(m) could descend into lambdas and foralls. I wonder why we never implemented that.

[eric-wieser]

It would also be cool if congr(m) could descend into lambdas and foralls. I wonder why we never implemented that.

This is my biggest gripe with congr.

[robertylewis]

My only complaint is that the docs are a little on the technical side, with discussion of metavariables and so on! I think it might be clearer to write something like, "congrm e takes an expression e containing placeholders _. It matches both lhs and rhs to this pattern, and produces one goal for each placeholder, stating that the corresponding subexpressions in lhs and rhs are equal."

I think it would also be good to include one or two of the earlier tests in the docs as examples, rather than only giving the one that has binders in it.

[adomani]

Thanks, Rob! I updated the doc-string, making it hopefully more user-friendly!

I also added an example that should clarify better the intended use of the tactic.

[robertylewis]

Looks great!

[robertylewis]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests