feat({tactic + test}/congrm, logic/basic): `congrm = congr + pattern-…

…match` (#14153)

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](https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/variant.20syntax.20for.20.60congr'.60)

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



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

src/tactic/congrm.lean

@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2022 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner, Damiano Testa
+-/
+import tactic.interactive
+
+/-! `congrm`: `congr` with pattern-matching
+
+`congrm e` gives to the use the functionality of using `congr` with an expression `e` "guiding"
+`congr` through the matching.  This allows more flexibility than `congr' n`, which enters uniformly
+through `n` iterations.  Instead, we can guide the matching deeper on some parts of the expression
+and stop earlier on other parts.
+-/
+
+namespace tactic
+
+/--
+For each element of `list congr_arg_kind` that is `eq`, add a pair `(g, pat)` to the
+final list.  Otherwise, discard an appropriate number of initial terms from each list
+(possibly none from the first) and repeat.
+
+`pat` is the given pattern-piece at the appropriate location, extracted from the last `list expr`.
+It appears to be the list of arguments of a function application.
+
+`g` is possibly the proof of an equality?  It is extracted from the first `list expr`.
+-/
+private meta def extract_subgoals : list expr → list congr_arg_kind → list expr →
+  tactic (list (expr × expr))
+| (_ :: _ :: g :: prf_args) (congr_arg_kind.eq :: kinds)             (pat :: pat_args) :=
+  (λ rest, (g, pat) :: rest) <$> extract_subgoals prf_args kinds pat_args
+| (_ :: prf_args)           (congr_arg_kind.fixed :: kinds)          (_ :: pat_args) :=
+  extract_subgoals prf_args kinds pat_args
+| prf_args                  (congr_arg_kind.fixed_no_param :: kinds) (_ :: pat_args) :=
+  extract_subgoals prf_args kinds pat_args
+| (_ :: _ :: prf_args)      (congr_arg_kind.cast :: kinds)           (_ :: pat_args) :=
+  extract_subgoals prf_args kinds pat_args
+| _ _ [] := pure []
+| _ _ _ := fail "unsupported congr lemma"
+
+/--
+`equate_with_pattern_core pat` solves a single goal of the form `lhs = rhs`
+(assuming that `lhs` and `rhs` are unifiable with `pat`)
+by applying congruence lemmas until `pat` is a metavariable.
+Returns the list of metavariables for the new subgoals at the leafs.
+Calls `set_goals []` at the end.
+-/
+meta def equate_with_pattern_core : expr → tactic (list expr) | pat :=
+(applyc ``subsingleton.elim >> pure []) <|>
+(applyc ``rfl >> pure []) <|>
+if pat.is_mvar || pat.get_delayed_abstraction_locals.is_some then do
+  try $ applyc ``_root_.propext,
+  get_goals <* set_goals []
+else if pat.is_app then do
+  cl ← mk_specialized_congr_lemma pat,
+  H_congr_lemma ← assertv `H_congr_lemma cl.type cl.proof,
+  [prf] ← get_goals,
+  apply H_congr_lemma <|> fail "could not apply congr_lemma",
+  all_goals' $ try $ clear H_congr_lemma,  -- given the `set_goals []` that follows, is this needed?
+  set_goals [],
+  prf ← instantiate_mvars prf,
+  subgoals ← extract_subgoals prf.get_app_args cl.arg_kinds pat.get_app_args,
+  subgoals ← subgoals.mmap (λ ⟨subgoal, subpat⟩, do
+    set_goals [subgoal],
+    equate_with_pattern_core subpat),
+  pure subgoals.join
+else if pat.is_lambda then do
+  applyc ``_root_.funext,
+  x ← intro pat.binding_name,
+  equate_with_pattern_core $ pat.lambda_body.instantiate_var x
+else if pat.is_pi then do
+  applyc ``_root_.pi_congr,
+  x ← intro pat.binding_name,
+  equate_with_pattern_core $ pat.pi_codomain.instantiate_var x
+else do
+  pat ← pp pat,
+  fail $ to_fmt "unsupported pattern:\n" ++ pat
+
+/--
+`equate_with_pattern pat` solves a single goal of the form `lhs = rhs`
+(assuming that `lhs` and `rhs` are unifiable with `pat`)
+by applying congruence lemmas until `pat` is a metavariable.
+The subgoals for the leafs are prepended to the goals.
+--/
+meta def equate_with_pattern (pat : expr) : tactic unit := do
+congr_subgoals ← solve1 (equate_with_pattern_core pat),
+gs ← get_goals,
+set_goals $ congr_subgoals ++ gs
+
+end tactic
+
+namespace tactic.interactive
+open tactic interactive
+setup_tactic_parser
+
+/--
+Assume that the goal is of the form `lhs = rhs` or `lhs ↔ rhs`.
+`congrm e` takes an expression `e` containing placeholders `_` and scans `e, lhs, rhs` in parallel.
+
+It matches both `lhs` and `rhs` to the pattern `e`, and produces one goal for each placeholder,
+stating that the corresponding subexpressions in `lhs` and `rhs` are equal.
+
+Examples:
+```lean
+example {a b c d : ℕ} :
+  nat.pred a.succ * (d + (c + a.pred)) = nat.pred b.succ * (b + (c + d.pred)) :=
+begin
+  congrm nat.pred (nat.succ _) * (_ + _),
+/-  Goals left:
+⊢ a = b
+⊢ d = b
+⊢ c + a.pred = c + d.pred
+-/
+  sorry,
+  sorry,
+  sorry,
+end
+
+example {a b : ℕ} (h : a = b) : (λ y : ℕ, ∀ z, a + a = z) = (λ x, ∀ z, b + a = z) :=
+begin
+  congrm λ x, ∀ w, _ + a = w,
+  -- produces one goal for the underscore: ⊢ a = b
+  exact h,
+end
+```
+-/
+meta def congrm (arg : parse texpr) : tactic unit := do
+try $ applyc ``_root_.eq.to_iff,
+`(@eq %%ty _ _) ← target | fail "congrm: goal must be an equality or iff",
+ta ← to_expr ``((%%arg : %%ty)) tt ff,
+equate_with_pattern ta
+
+add_tactic_doc
+{ name := "congrm",
+  category := doc_category.tactic,
+  decl_names := [`tactic.interactive.congrm],
+  tags := ["congruence"] }
+
+end tactic.interactive

test/congrm.lean

@@ -0,0 +1,63 @@
+import tactic.congrm
+
+variables {X : Type*} [has_add X] [has_mul X] (a b c d : X) (f : X → X)
+
+example (H : a = b) : f a + f a = f b + f b :=
+by congrm f _ + f _; exact H
+
+example {g : X → X} (H : a = b) (H' : c + f a = c + f d) (H'' : f d = f b) :
+  f (g a) * (f d + (c + f a)) = f (g b) * (f b + (c + f d)) :=
+begin
+  congrm f (g _) * (_ + _),
+  { exact H },
+  { exact H'' },
+  { exact H' },
+end
+
+example (H' : c + (f a) = c + (f d)) (H'' : f d = f b) :
+  f (f a) * (f d + (c + f a)) = f (f a) * (f b + (c + f d)) :=
+begin
+  congrm f (f _) * (_ + _),
+  { exact H'' },
+  { exact H' },
+end
+
+example (H' : c + (f a) = c + (f d)) (H'' : f d = f b) :
+  f (f a) * (f d + (c + f a)) = f (f a) * (f b + (c + f d)) :=
+begin
+  congrm f (f _) * (_ + _),
+  { exact H'' },
+  { exact H' },
+end
+
+example {p q} [decidable p] [decidable q] (h : p ↔ q) :
+  ite p 0 1 = ite q 0 1 :=
+begin
+  congrm ite _ 0 1,
+  exact h,
+end
+
+example {p q} [decidable p] [decidable q] (h : p ↔ q) :
+  ite p 0 1 = ite q 0 1 :=
+begin
+  congrm ite _ 0 1,
+  exact h,
+end
+
+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
+
+example (h : 5 = 3) : (⟨5 + 1, dec_trivial⟩ : fin 10) = ⟨3 + 1, dec_trivial⟩ :=
+begin
+  congrm ⟨_ + 1, _⟩,
+  exact h,
+end
+
+example : true ∧ false ↔ (true ∧ true) ∧ false :=
+begin
+  congrm _ ∧ _,
+  exact (true_and true).symm,
+end