feat: let congr! discharge equalities of BEq instances (#11179)

Adds a congruence lemma for `BEq` instances that makes use of `LawfulBEq` instances, and gives `congr!` the ability to use this congruence lemma. This is meant to help with diamonds that arise from interactions between Decidable and BEq instances.

This feature can be turned off using the `beqEq` configuration setting, like `congr! (config := { beqEq := false })`.

Mathlib/Logic/Basic.lean

@@ -1292,3 +1292,20 @@ theorem not_beq_of_ne [BEq α] [LawfulBEq α] {a b : α} (ne : a ≠ b) : ¬(a =
 theorem beq_eq_decide [BEq α] [LawfulBEq α] {a b : α} : (a == b) = decide (a = b) := by
   rw [← beq_iff_eq a b]
   cases a == b <;> simp
+
+@[ext]
+theorem beq_ext (inst1 : BEq α) (inst2 : BEq α)
+    (h : ∀ x y, @BEq.beq _ inst1 x y = @BEq.beq _ inst2 x y) :
+    inst1 = inst2 := by
+  have ⟨beq1⟩ := inst1
+  have ⟨beq2⟩ := inst2
+  congr
+  funext x y
+  exact h x y
+
+theorem lawful_beq_subsingleton (inst1 : BEq α) (inst2 : BEq α)
+    [@LawfulBEq α inst1] [@LawfulBEq α inst2] :
+    inst1 = inst2 := by
+  apply beq_ext
+  intro x y
+  simp only [beq_eq_decide]

Mathlib/Tactic/Congr!.lean

@@ -6,6 +6,7 @@ Authors: Kyle Miller
 import Lean.Elab.Tactic.Config
 import Lean.Elab.Tactic.RCases
 import Mathlib.Lean.Meta.CongrTheorems
+import Mathlib.Logic.Basic
 import Mathlib.Tactic.Relation.Rfl
 import Std.Logic
 
@@ -107,6 +108,9 @@ structure Congr!.Config where
   `preferLHS`, `partialApp` and `maxArgs` and transparency settings. It acts as if `sameFun := true`
   and it ignores `typeEqs`. -/
   useCongrSimp : Bool := false
+  /-- Whether to use a special congruence lemma for `BEq` instances.
+  This synthesizes `LawfulBEq` instances to discharge equalities of `BEq` instances. -/
+  beqEq : Bool := true
 
 /-- A configuration option that makes `congr!` do the sorts of aggressive unfoldings that `congr`
 does while also similarly preventing `congr!` from considering partial applications or congruences
@@ -307,7 +311,6 @@ Applies the congruence generated congruence lemmas according to `config`.
 def Lean.MVarId.congrSimp? (config : Congr!.Config) (mvarId : MVarId) :
     MetaM (Option (List MVarId)) :=
   mvarId.withContext do
-    unless config.useCongrSimp do return none
     mvarId.checkNotAssigned `congrSimp?
     let some (_, lhs, rhs) := (← withReducible mvarId.getType').eq? | return none
     let (fst, snd) := if config.preferLHS then (lhs, rhs) else (rhs, lhs)
@@ -333,7 +336,7 @@ where
       observing? <| applyCongrThm? config mvarId congrThm.type congrThm.proof
   /-- Like `mkCongrSimp?` but takes in a specific arity. -/
   mkCongrSimpNArgs (f : Expr) (nArgs : Nat) : MetaM (Option CongrTheorem) := do
-    let f := (← instantiateMVars f).cleanupAnnotations
+    let f := (← Lean.instantiateMVars f).cleanupAnnotations
     let info ← getFunInfoNArgs f nArgs
     mkCongrSimpCore? f info
       (← getCongrSimpKinds f info) (subsingletonInstImplicitRhs := false)
@@ -444,19 +447,35 @@ def Lean.MVarId.subsingletonHelim? (mvarId : MVarId) : MetaM (Option (List MVarI
       return [eqmvar.mvarId!]
     failure
 
+/--
+Tries to apply `lawful_beq_subsingleton` to prove that two `BEq` instances are equal
+by synthesizing `LawfulBEq` instances for both.
+-/
+def Lean.MVarId.beqInst? (mvarId : MVarId) : MetaM (Option (List MVarId)) :=
+  observing? do withReducible <| mvarId.applyConst ``lawful_beq_subsingleton
+
 /--
 A list of all the congruence strategies used by `Lean.MVarId.congrCore!`.
 -/
 def Lean.MVarId.congrPasses! :
     List (String × (Congr!.Config → MVarId → MetaM (Option (List MVarId)))) :=
   [("user congr", userCongr?),
    ("hcongr lemma", smartHCongr?),
-   ("congr simp lemma", congrSimp?),
+   ("congr simp lemma", when (·.useCongrSimp) congrSimp?),
    ("Subsingleton.helim", fun _ => subsingletonHelim?),
+   ("BEq instances", when (·.beqEq) fun _ => beqInst?),
    ("obvious funext", fun _ => obviousFunext?),
    ("obvious hfunext", fun _ => obviousHfunext?),
    ("congr_implies", fun _ => congrImplies?'),
    ("congr_pi", fun _ => congrPi?)]
+where
+  /--
+  Conditionally runs a congruence strategy depending on the predicate `b` applied to the config.
+  -/
+  when (b : Congr!.Config → Bool) (f : Congr!.Config → MVarId → MetaM (Option (List MVarId)))
+      (config : Congr!.Config) (mvar : MVarId) : MetaM (Option (List MVarId)) := do
+    unless b config do return none
+    f config mvar
 
 structure CongrState where
   /-- Accumulated goals that `congr!` could not handle. -/
@@ -517,7 +536,7 @@ where
         if ty.isArrow then
           if ← (isTrivialType ty.bindingDomain!
                 <||> (← getLCtx).anyM (fun decl => do
-                        return (← instantiateMVars decl.type) == ty.bindingDomain!)) then
+                        return (← Lean.instantiateMVars decl.type) == ty.bindingDomain!)) then
             -- Don't intro, clear it
             let mvar ← mkFreshExprSyntheticOpaqueMVar ty.bindingBody! (← mvarId.getTag)
             mvarId.assign <| .lam .anonymous ty.bindingDomain! mvar .default
@@ -533,7 +552,7 @@ where
   isTrivialType (ty : Expr) : MetaM Bool := do
     unless ← Meta.isProp ty do
       return false
-    let ty ← instantiateMVars ty
+    let ty ← Lean.instantiateMVars ty
     if let some (lhs, rhs) := ty.eqOrIff? then
       if lhs.cleanupAnnotations == rhs.cleanupAnnotations then
         return true

scripts/noshake.json

@@ -276,6 +276,7 @@
    "Mathlib.Data.Fintype.Sigma",
    "Mathlib.Data.Fintype.Sum"],
   "Mathlib.Tactic.Continuity": ["Mathlib.Tactic.Continuity.Init"],
+  "Mathlib.Tactic.Congr!": ["Mathlib.Logic.Basic"],
   "Mathlib.Tactic.Choose": ["Mathlib.Logic.Function.Basic"],
   "Mathlib.Tactic.CategoryTheory.Slice":
   ["Mathlib.CategoryTheory.Category.Basic"],

test/congr.lean

@@ -309,3 +309,28 @@ example {α} [AddCommMonoid α] [PartialOrder α] {a b c d e f g : α} :
     (a + b) + (c + d) + (e + f) + g ≤ a + d + e + f + c + b + g := by
   ac_change a + d + e + f + c + g + b ≤ a + d + e + f + c + g + b
   rfl
+
+/-!
+Lawful BEq instances are "subsingletons".
+-/
+
+example (inst1 : BEq α) [LawfulBEq α] (inst2 : BEq α) [LawfulBEq α] (xs : List α) (x : α) :
+    @List.erase _ inst1 xs x = @List.erase _ inst2 xs x := by
+  congr!
+
+/--
+error: unsolved goals
+case h.e'_2
+α : Type ?u.83134
+inst1 : BEq α
+inst✝¹ : LawfulBEq α
+inst2 : BEq α
+inst✝ : LawfulBEq α
+xs : List α
+x : α
+⊢ inst1 = inst2
+-/
+#guard_msgs in
+example (inst1 : BEq α) [LawfulBEq α] (inst2 : BEq α) [LawfulBEq α] (xs : List α) (x : α) :
+    @List.erase _ inst1 xs x = @List.erase _ inst2 xs x := by
+  congr! (config := { beqEq := false })