feat: add congr tactic

RELEASES.md

@@ -1,6 +1,8 @@
 Unreleased
 ---------
 
+* Add tactic `congr (num)?`. See doc string for additional details.
+
 * [Missing doc linter](https://github.com/leanprover/lean4/pull/1390)
 
 * `match`-syntax notation now checks for unused alternatives. See issue [#1371](https://github.com/leanprover/lean4/issues/1371).

src/Init/Tactics.lean

@@ -493,6 +493,15 @@ syntax (name := sleep) "sleep" num : tactic
 macro "exists " es:term,+ : tactic =>
   `(tactic| (refine ⟨$es,*, ?_⟩; try trivial))
 
+/--
+Apply congruence (recursively) to goals of the form `⊢ f as = f bs` and `⊢ HEq (f as) (f bs)`.
+The optional parameter is the depth of the recursive applications. This is useful when `congr` is too aggressive
+in breaking down the goal.
+For example, given `⊢ f (g (x + y)) = f (g (y + x))`, `congr` produces the goals `⊢ x = y` and `⊢ y = x`,
+while `congr 2` produces the intended `⊢ x + y = y + x`.
+-/
+syntax (name := congr) "congr " (num)? : tactic
+
 end Tactic
 
 namespace Attr

src/Lean/Elab/Tactic.lean

@@ -21,3 +21,4 @@ import Lean.Elab.Tactic.Meta
 import Lean.Elab.Tactic.Unfold
 import Lean.Elab.Tactic.Cache
 import Lean.Elab.Tactic.Calc
+import Lean.Elab.Tactic.Congr

src/Lean/Elab/Tactic/Congr.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Congr
+import Lean.Elab.Tactic.Basic
+
+namespace Lean.Elab.Tactic
+
+namespace Lean.Elab.Tactic
+@[builtinTactic Parser.Tactic.congr] def evalCongr : Tactic := fun stx =>
+  match stx with
+  | `(tactic| congr $[$n?]?) =>
+    let hugeDepth := 1000000
+    let depth := n?.map (·.getNat) |>.getD hugeDepth
+    liftMetaTactic fun mvarId => mvarId.congrN depth
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic
+
+

src/Lean/Meta/Tactic.lean

@@ -28,3 +28,4 @@ import Lean.Meta.Tactic.Rename
 import Lean.Meta.Tactic.LinearArith
 import Lean.Meta.Tactic.AC
 import Lean.Meta.Tactic.Refl
+import Lean.Meta.Tactic.Congr

src/Lean/Meta/Tactic/Congr.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.CongrTheorems
+import Lean.Meta.Tactic.Assert
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Refl
+import Lean.Meta.Tactic.Assumption
+
+namespace Lean
+open Meta
+
+/--
+Postprocessor after applying congruence theorem.
+Tries to close new goals using `Eq.refl`, `HEq.refl`, and `assumption`.
+It also tries to apply `heq_of_eq`, and clears `fvarId`.
+-/
+private def congrPost (fvarId : FVarId) (mvarIds : List MVarId) : MetaM (List MVarId) :=
+  mvarIds.filterMapM fun mvarId => do
+    let mvarId ← mvarId.heqOfEq
+    try mvarId.refl; return none catch _ => pure ()
+    try mvarId.hrefl; return none catch _ => pure ()
+    if (← mvarId.assumptionCore) then return none
+    let mvarId ← mvarId.tryClear fvarId
+    return some mvarId
+
+/--
+Asserts the given congruence theorem as fresh hypothesis, and then applies it.
+Return the `fvarId` for the new hypothesis and the new subgoals.
+-/
+private def applyCongrThm? (mvarId : MVarId) (congrThm : CongrTheorem) : MetaM (Option (FVarId × List MVarId)) := do
+  let mvarId ← mvarId.assert (← mkFreshUserName `h_congr_thm) congrThm.type congrThm.proof
+  let (fvarId, mvarId) ← mvarId.intro1P
+  let mvarIds ← mvarId.apply (mkFVar fvarId)
+  return some (fvarId, mvarIds)
+
+/--
+Try to apply a `simp` congruence theorem.
+-/
+def MVarId.congr? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `congr
+    let target ← mvarId.getType'
+    let some (_, lhs, _) := target.eq? | return none
+    unless lhs.isApp do return none
+    let some congrThm ← mkCongrSimp? lhs.getAppFn | return none
+    let some (fvarId, mvarIds) ← applyCongrThm? mvarId congrThm | return none
+    congrPost fvarId mvarIds
+
+/--
+Try to apply a hcongr congruence theorem. This kind of theorem is used by
+the congruence closure module.
+-/
+def MVarId.hcongr? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  mvarId.withContext do
+    mvarId.checkNotAssigned `congr
+    let target ← mvarId.getType'
+    let some (_, lhs, _, _) := target.heq? | return none
+    unless lhs.isApp do return none
+    let congrThm ← mkHCongr lhs.getAppFn
+    trace[Meta.debug] "congrThm: {congrThm.type}"
+    let some (fvarId, mvarIds) ← applyCongrThm? mvarId congrThm | return none
+    congrPost fvarId mvarIds
+
+/--
+Given a goal of the form `⊢ f as = f bs` or `⊢ HEq (f as) (f bs)`, try to apply congruence.
+It takes proof irrelevance into account, the fact that `Decidable p` is a subsingleton.
+It tries to close new subgoals using `Eq.refl`, `HEq.refl`, and `assumption`.
+-/
+def MVarId.congr (mvarId : MVarId) : MetaM (List MVarId) := do
+  if let some mvarIds ← mvarId.congr? then
+    return mvarIds
+  else if let some mvarIds ← mvarId.hcongr? then
+    return mvarIds
+  else
+    throwTacticEx `congr mvarId "failed to apply congruence"
+
+/--
+Applies `congr` recursively up to depth `n`.
+-/
+def MVarId.congrN (mvarId : MVarId) (n : Nat) : MetaM (List MVarId) := do
+  let (_, s) ← go n mvarId |>.run #[]
+  return s.toList
+where
+  go (n : Nat) (mvarId : MVarId) : StateRefT (Array MVarId) MetaM Unit := do
+    match n with
+    | 0 => modify (·.push mvarId)
+    | n+1 =>
+      let some mvarIds ← observing? (m := MetaM) mvarId.congr
+        | modify (·.push mvarId)
+      mvarIds.forM (go n)
+end Lean
+

tests/lean/run/congrTactic.lean

@@ -0,0 +1,32 @@
+example (h : a = b) : Nat.succ (a + 1) = Nat.succ (b + 1) := by
+  congr
+
+example (h : a = b) : Nat.succ (a + 1) = Nat.succ (b + 1) := by
+  congr 1
+  show a + 1 = b + 1
+  rw [h]
+
+def f (p : Prop) (a : Nat) (h : a > 0) [Decidable p] : Nat :=
+  if p then
+    a - 1
+  else
+    a + 1
+
+example (h : a = b) : f True (a + 1) (by simp_arith) = f (0 = 0) (b + 1) (by simp_arith) := by
+  congr
+  decide
+
+example (h : a = b) : f True (a + 1) (by simp_arith) = f (0 = 0) (b + 1) (by simp_arith) := by
+  congr 1
+  · decide
+  · show a + 1 = b + 1
+    rw [h]
+
+example (h₁ : α = β) (h₂ : α = γ) (a : α) : HEq (cast h₁ a) (cast h₂ a) := by
+  congr
+  · subst h₁ h₂; rfl
+  · subst h₁ h₂; apply heq_of_eq; rfl
+
+example (f : Nat → Nat) (g : Nat → Nat) : f (g (x + y)) = f (g (y + x)) := by
+  congr 2
+  rw [Nat.add_comm]