feat: congr(...) congruence quotations and port congrm tactic (#2544

)

Adds a term elaborator for `congr(...)` "congruence quotations". For example, if `hf : f = f'` and `hx : x = x'`, then we have `congr($hf $x) : f x = f' x'`. This supports the functions having implicit arguments, and it has support for subsingleton instance arguments. So for example, if `s t : Set X` are sets with `Fintype` instances and `h : s = t` then `congr(Fintype.card $h) : Fintype.card s = Fintype.card t` works.

Ports the `congrm` tactic as a convenient frontend for applying a congruence quotation to the goal. Holes are turned into congruence holes. For example, `congrm 1 + ?_` uses `congr(1 + $(?_))`. Placeholders (`_`) do not turn into congruence holes; that's not to say they have to be identical on the LHS and RHS, but `congrm` itself is responsible for finding a congruence lemma for such arguments.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>

Mathlib.lean

@@ -2994,6 +2994,7 @@ import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Common
 import Mathlib.Tactic.ComputeDegree
 import Mathlib.Tactic.Congr!
+import Mathlib.Tactic.Congrm
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Continuity
 import Mathlib.Tactic.Continuity.Init
@@ -3117,6 +3118,7 @@ import Mathlib.Tactic.SudoSetOption
 import Mathlib.Tactic.SwapVar
 import Mathlib.Tactic.TFAE
 import Mathlib.Tactic.Tauto
+import Mathlib.Tactic.TermCongr
 import Mathlib.Tactic.ToAdditive
 import Mathlib.Tactic.ToExpr
 import Mathlib.Tactic.ToLevel

Mathlib/Analysis/Convex/Gauge.lean

@@ -66,12 +66,8 @@ theorem gauge_def : gauge s x = sInf ({ r ∈ Set.Ioi (0 : ℝ) | x ∈ r • s
 
 /-- An alternative definition of the gauge using scalar multiplication on the element rather than on
 the set. -/
-theorem gauge_def' : gauge s x = sInf ({ r ∈ Set.Ioi (0 : ℝ) | r⁻¹ • x ∈ s }) := by
-  -- Porting note: used `congrm`
-  rw [gauge]
-  apply congr_arg
-  ext
-  simp only [mem_setOf, mem_Ioi]
+theorem gauge_def' : gauge s x = sInf {r ∈ Set.Ioi (0 : ℝ) | r⁻¹ • x ∈ s} := by
+  congrm sInf {r | ?_}
   exact and_congr_right fun hr => mem_smul_set_iff_inv_smul_mem₀ hr.ne' _ _
 #align gauge_def' gauge_def'
 

Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

@@ -447,10 +447,7 @@ theorem SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf [TopologicalAd
   rw [p.withSeminorms_iff_nhds_eq_iInf,
     TopologicalAddGroup.ext_iff inferInstance (topologicalAddGroup_iInf fun i => inferInstance),
     nhds_iInf]
-  -- Porting note: next three lines was `congrm (_ = ⨅ i, _)`
-  refine Eq.to_iff ?_
-  congr
-  funext i
+  congrm _ = ⨅ i, ?_
   exact @comap_norm_nhds_zero _ (p i).toSeminormedAddGroup
 #align seminorm_family.with_seminorms_iff_topological_space_eq_infi SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf
 
@@ -472,10 +469,7 @@ theorem SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf [u : UniformSpace
   rw [p.withSeminorms_iff_nhds_eq_iInf,
     UniformAddGroup.ext_iff inferInstance (uniformAddGroup_iInf fun i => inferInstance),
     toTopologicalSpace_iInf, nhds_iInf]
-  -- Porting note: next three lines was `congrm (_ = ⨅ i, _)`
-  refine Eq.to_iff ?_
-  congr
-  funext i
+  congrm _ = ⨅ i, ?_
   exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup
 #align seminorm_family.with_seminorms_iff_uniform_space_eq_infi SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf
 

Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

@@ -545,7 +545,7 @@ theorem liftProp_id (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y) :
 theorem liftPropAt_iff_comp_inclusion (hG : LocalInvariantProp G G' P) {U V : Opens M} (hUV : U ≤ V)
     (f : V → M') (x : U) :
     LiftPropAt P f (Set.inclusion hUV x) ↔ LiftPropAt P (f ∘ Set.inclusion hUV : U → M') x := by
-  change (_ ∧ _) ↔ (_ ∧ _); congr! 1 -- Porting note: was `congrm _ ∧ _`
+  congrm ?_ ∧ ?_
   · simp [continuousWithinAt_univ,
       (TopologicalSpace.Opens.openEmbedding_of_le hUV).continuousAt_iff]
   · apply hG.congr_iff

Mathlib/Geometry/Manifold/MFDeriv.lean

@@ -222,8 +222,7 @@ def MDifferentiableAt (f : M → M') (x : M) :=
 
 theorem mdifferentiableAt_iff_liftPropAt (f : M → M') (x : M) :
     MDifferentiableAt I I' f x ↔ LiftPropAt (DifferentiableWithinAtProp I I') f x := by
-  -- porting note: was `congrm ∧`
-  apply Iff.and
+  congrm ?_ ∧ ?_
   · rw [continuousWithinAt_univ]
   · -- porting note: `rfl` wasn't needed
     simp [DifferentiableWithinAtProp, Set.univ_inter]; rfl

Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

@@ -216,8 +216,7 @@ theorem SmoothFiberwiseLinear.locality_aux₂ (e : LocalHomeomorph (B × F) (B 
   refine' ⟨Φ, U, hU', hΦ, h2Φ, hU, fun p hp => _⟩
   rw [hU] at hp
   rw [heuφ ⟨p.fst, hp.1⟩ ⟨hux _, hp.2⟩]
-  -- porting note: replaced `congrm` with manual `congr_arg`
-  refine congr_arg (Prod.mk _) ?_
+  congrm (_, ?_)
   rw [hΦφ]
   apply hux
 #align smooth_fiberwise_linear.locality_aux₂ SmoothFiberwiseLinear.locality_aux₂

Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

@@ -365,11 +365,10 @@ theorem coe_T_zpow (n : ℤ) : ↑ₘ(T ^ n) = !![1, n; 0, 1] := by
   induction' n using Int.induction_on with n h n h
   · rw [zpow_zero, coe_one, Matrix.one_fin_two]
   · simp_rw [zpow_add, zpow_one, coe_mul, h, coe_T, Matrix.mul_fin_two]
-    -- Porting note: was congrm !![_, _; _, _]
-    ring_nf
+    congrm !![_, ?_; _, _]
+    rw [mul_one, mul_one, add_comm]
   · simp_rw [zpow_sub, zpow_one, coe_mul, h, coe_T_inv, Matrix.mul_fin_two]
-    -- Porting note: was congrm !![_, _; _, _]
-    ring_nf
+    congrm !![?_, ?_; _, _] <;> ring
 #align modular_group.coe_T_zpow ModularGroup.coe_T_zpow
 
 @[simp]

Mathlib/Mathport/Syntax.lean

@@ -29,6 +29,7 @@ import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Constructor
+import Mathlib.Tactic.Congrm
 import Mathlib.Tactic.Continuity
 import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.Conv
@@ -162,8 +163,6 @@ open Lean Parser.Tactic
 
 /- S -/ syntax (name := hint) "hint" : tactic
 
-/- M -/ syntax (name := congrM) "congrm " term : tactic
-
 /- S -/ syntax (name := rcases?) "rcases?" casesTarget,* (" : " num)? : tactic
 /- S -/ syntax (name := rintro?) "rintro?" (" : " num)? : tactic
 

Mathlib/NumberTheory/Modular.lean

@@ -368,8 +368,7 @@ theorem g_eq_of_c_eq_one (hc : (↑ₘg) 1 0 = 1) : g = T ^ (↑ₘg) 0 0 * S *
   conv_lhs => rw [Matrix.eta_fin_two (↑ₘg)]
   rw [hc, hg]
   simp only [coe_mul, coe_T_zpow, coe_S, mul_fin_two]
-  -- Porting note: Was `congrm !![_, _; _, _] <;> ring`.
-  congr! 3 <;> [skip; congr! 1; congr! 2] <;> ring
+  congrm !![?_, ?_; ?_, ?_] <;> ring
 #align modular_group.g_eq_of_c_eq_one ModularGroup.g_eq_of_c_eq_one
 
 set_option maxHeartbeats 250000 in

Mathlib/Order/OrderIsoNat.lean

@@ -228,10 +228,9 @@ theorem WellFounded.monotone_chain_condition' [Preorder α] :
 theorem WellFounded.monotone_chain_condition [PartialOrder α] :
     WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m :=
   WellFounded.monotone_chain_condition'.trans <| by
-  -- porting note: was congrm ∀ a, ∃ n, ∀ m (h : n ≤ m), (_ : Prop)
-  congr! 4
-  rename_i a n m
-  simp (config := {contextual := true}) [lt_iff_le_and_ne, fun h => a.mono h]
+  congrm ∀ a, ∃ n, ∀ m h, ?_
+  rw [lt_iff_le_and_ne]
+  simp [a.mono h]
 #align well_founded.monotone_chain_condition WellFounded.monotone_chain_condition
 
 /-- Given an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a partially-ordered

Mathlib/Tactic.lean

@@ -26,6 +26,7 @@ import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Common
 import Mathlib.Tactic.ComputeDegree
 import Mathlib.Tactic.Congr!
+import Mathlib.Tactic.Congrm
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Continuity
 import Mathlib.Tactic.Continuity.Init
@@ -149,6 +150,7 @@ import Mathlib.Tactic.SudoSetOption
 import Mathlib.Tactic.SwapVar
 import Mathlib.Tactic.TFAE
 import Mathlib.Tactic.Tauto
+import Mathlib.Tactic.TermCongr
 import Mathlib.Tactic.ToAdditive
 import Mathlib.Tactic.ToExpr
 import Mathlib.Tactic.ToLevel

Mathlib/Tactic/Common.lean

@@ -34,6 +34,7 @@ import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Congr!
+import Mathlib.Tactic.Congrm
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.Conv
@@ -100,6 +101,7 @@ import Mathlib.Tactic.SuccessIfFailWithMsg
 import Mathlib.Tactic.SudoSetOption
 import Mathlib.Tactic.SwapVar
 import Mathlib.Tactic.Tauto
+import Mathlib.Tactic.TermCongr
 -- TFAE imports `Mathlib.Data.List.TFAE` and thence `Mathlib.Data.List.Basic`.
 -- import Mathlib.Tactic.TFAE
 import Mathlib.Tactic.ToExpr

Mathlib/Tactic/Congrm.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2023 Moritz Doll, Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll, Gabriel Ebner, Damiano Testa, Kyle Miller
+-/
+import Mathlib.Tactic.TermCongr
+
+/-!
+# The `congrm` tactic
+
+The `congrm` tactic ("`congr` with matching")
+is a convenient frontend for `congr(...)` congruence quotations.
+Roughly, `congrm e` is `refine congr(e')`, where `e'` is `e` with every `?m` placeholder
+replaced by `$(?m)`.
+-/
+
+namespace Mathlib.Tactic
+open Lean Parser Tactic Elab Tactic Meta
+
+initialize registerTraceClass `Tactic.congrm
+
+/--
+`congrm e` is a tactic for proving goals of the form `lhs = rhs`, `lhs ↔ rhs`, `HEq lhs rhs`,
+or `R lhs rhs` when `R` is a reflexive relation.
+The expression `e` is a pattern containing placeholders `?_`,
+and this pattern is matched against `lhs` and `rhs` simultaneously.
+These placeholders generate new goals that state that corresponding subexpressions
+in `lhs` and `rhs` are equal.
+If the placeholders have names, such as `?m`, then the new goals are given tags with those names.
+
+Examples:
+```lean
+example {a b c d : ℕ} :
+    Nat.pred a.succ * (d + (c + a.pred)) = Nat.pred b.succ * (b + (c + d.pred)) := by
+  congrm Nat.pred (Nat.succ ?h1) * (?h2 + ?h3)
+  /-  Goals left:
+  case h1 ⊢ a = b
+  case h2 ⊢ d = b
+  case h3 ⊢ c + a.pred = c + d.pred
+  -/
+  sorry
+  sorry
+  sorry
+
+example {a b : ℕ} (h : a = b) : (fun y : ℕ => ∀ z, a + a = z) = (fun x => ∀ z, b + a = z) := by
+  congrm fun x => ∀ w, ?_ + a = w
+  -- ⊢ a = b
+  exact h
+```
+
+The `congrm` command is a convenient frontend to `congr(...)` congruence quotations.
+If the goal is an equality, `congrm e` is equivalent to `refine congr(e')` where `e'` is
+built from `e` by replacing each placeholder `?m` by `$(?m)`.
+The pattern `e` is allowed to contain `$(...)` expressions to immediately substitute
+equality proofs into the congruence, just like for congruence quotations.
+-/
+syntax (name := congrM) "congrm " term : tactic
+
+elab_rules : tactic
+  | `(tactic| congrm $expr:term) => do
+    -- Wrap all synthetic holes `?m` as `c(?m)` to form `congr(...)` pattern
+    let pattern ← expr.raw.replaceM fun stx =>
+      if stx.isOfKind ``Parser.Term.syntheticHole then
+        pure <| stx.mkAntiquotNode `term
+      else if stx.isAntiquots then
+        -- Don't look into `$(..)` expressions
+        pure stx
+      else
+        pure none
+    trace[Tactic.congrm] "pattern: {pattern}"
+    -- Chain together transformations as needed to convert the goal to an Eq if possible.
+    liftMetaTactic fun g => do
+      return [← (← g.iffOfEq).liftReflToEq]
+    -- Apply `congr(...)`
+    withMainContext do
+      let gStx ← Term.exprToSyntax (← getMainTarget)
+      -- Gives the expected type to `refine` as a workaround for its elaboration order.
+      evalTactic <| ← `(tactic| refine (congr($(⟨pattern⟩)) : $gStx))