From ad98df80fe766442eac1113c6a099999def7dc62 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Oct 2022 17:59:57 -0700
Subject: [PATCH] feat: `congr` theorems using `Iff`

closes #1763
---
 src/Init/Core.lean                               |  3 +++
 src/Lean/Meta/AppBuilder.lean                    |  7 +++++++
 src/Lean/Meta/Tactic/Simp.lean                   |  1 +
 src/Lean/Meta/Tactic/Simp/Main.lean              | 12 ++++++++++--
 src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean |  8 ++++----
 src/Lean/Util/Recognizers.lean                   |  6 ++++++
 tests/lean/1763.lean                             | 16 ++++++++++++++++
 tests/lean/1763.lean.expected.out                |  4 ++++
 8 files changed, 51 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/1763.lean
 create mode 100644 tests/lean/1763.lean.expected.out

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index bade81ce07..80bd05a339 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -676,6 +676,9 @@ theorem Iff.symm (h : a ↔ b) : b ↔ a :=
 theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
   Iff.intro Iff.symm Iff.symm
 
+theorem Iff.of_eq (h : a = b) : a ↔ b :=
+  h ▸ Iff.refl _
+
 theorem And.comm : a ∧ b ↔ b ∧ a := by
   constructor <;> intro ⟨h₁, h₂⟩ <;> exact ⟨h₂, h₁⟩
 
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index d8e5c84e8d..ee59df2fce 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -589,6 +589,13 @@ def mkLE (a b : Expr) : MetaM Expr := mkBinaryRel ``LE ``LE.le a b
 /-- Return `a < b`. This method assumes `a` and `b` have the same type. -/
 def mkLT (a b : Expr) : MetaM Expr := mkBinaryRel ``LT ``LT.lt a b
 
+/-- Given `h : a = b`, return a proof for `a ↔ b`. -/
+def mkIffOfEq (h : Expr) : MetaM Expr := do
+  if h.isAppOfArity ``propext 3 then
+    return h.appArg!
+  else
+    mkAppM ``Iff.of_eq #[h]
+
 builtin_initialize do
   registerTraceClass `Meta.appBuilder
   registerTraceClass `Meta.appBuilder.result (inherited := true)
diff --git a/src/Lean/Meta/Tactic/Simp.lean b/src/Lean/Meta/Tactic/Simp.lean
index aaadb53a41..30554e3d5c 100644
--- a/src/Lean/Meta/Tactic/Simp.lean
+++ b/src/Lean/Meta/Tactic/Simp.lean
@@ -18,5 +18,6 @@ builtin_initialize registerTraceClass `Meta.Tactic.simp.discharge (inherited :=
 builtin_initialize registerTraceClass `Meta.Tactic.simp.rewrite (inherited := true)
 builtin_initialize registerTraceClass `Meta.Tactic.simp.unify (inherited := true)
 builtin_initialize registerTraceClass `Debug.Meta.Tactic.simp
+builtin_initialize registerTraceClass `Debug.Meta.Tactic.simp.congr (inherited := true)
 
 end Lean
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index fffbe58046..9e87b662c1 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -488,7 +488,11 @@ where
         let val ← mkLambdaFVars zs r.expr
         unless (← isDefEq m val) do
           throwCongrHypothesisFailed
-        unless (← isDefEq h (← mkLambdaFVars xs (← r.getProof))) do
+        let mut proof ← r.getProof
+        if hType.isAppOf ``Iff then
+          try proof ← mkIffOfEq proof
+          catch _ => throwCongrHypothesisFailed
+        unless (← isDefEq h (← mkLambdaFVars xs proof)) do
           throwCongrHypothesisFailed
         /- We used to return `false` if `r.proof? = none` (i.e., an implicit `rfl` proof) because we
            assumed `dsimp` would also be able to simplify the term, but this is not true
@@ -515,6 +519,7 @@ where
     let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm)
     if c.hypothesesPos.any (· ≥ xs.size) then
       return none
+    let isIff := type.isAppOf ``Iff
     let lhs := type.appFn!.appArg!
     let rhs := type.appArg!
     let numArgs := lhs.getAppNumArgs
@@ -545,7 +550,10 @@ where
         trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed"
         return none
       let eNew ← instantiateMVars rhs
-      let proof ← instantiateMVars (mkAppN thm xs)
+      let mut proof ← instantiateMVars (mkAppN thm xs)
+      if isIff then
+        try proof ← mkAppM ``propext #[proof]
+        catch _ => return none
       congrArgs { expr := eNew, proof? := proof } extraArgs
     else
       return none
diff --git a/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
index fecade5fef..17868a869d 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpCongrTheorems.lean
@@ -52,9 +52,9 @@ builtin_initialize congrExtension : SimpleScopedEnvExtension SimpCongrTheorem Si
 def mkSimpCongrTheorem (declName : Name) (prio : Nat) : MetaM SimpCongrTheorem := withReducible do
   let c ← mkConstWithLevelParams declName
   let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType c)
-  match type.eq? with
+  match type.eqOrIff? with
   | none => throwError "invalid 'congr' theorem, equality expected{indentExpr type}"
-  | some (_, lhs, rhs) =>
+  | some (lhs, rhs) =>
     lhs.withApp fun lhsFn lhsArgs => rhs.withApp fun rhsFn rhsArgs => do
       unless lhsFn.isConst && rhsFn.isConst && lhsFn.constName! == rhsFn.constName! && lhsArgs.size == rhsArgs.size do
         throwError "invalid 'congr' theorem, equality left/right-hand sides must be applications of the same function{indentExpr type}"
@@ -67,9 +67,9 @@ def mkSimpCongrTheorem (declName : Name) (prio : Nat) : MetaM SimpCongrTheorem :
       for x in xs, bi in bis do
         if bi.isExplicit && !foundMVars.contains x.mvarId! then
           let rhsFn? ← forallTelescopeReducing (← inferType x) fun ys xType => do
-            match xType.eq? with
+            match xType.eqOrIff? with
             | none => pure none -- skip
-            | some (_, xLhs, xRhs) =>
+            | some (xLhs, xRhs) =>
               let mut j := 0
               for y in ys do
                 let yType ← inferType y
diff --git a/src/Lean/Util/Recognizers.lean b/src/Lean/Util/Recognizers.lean
index 98125141f3..fc074065fc 100644
--- a/src/Lean/Util/Recognizers.lean
+++ b/src/Lean/Util/Recognizers.lean
@@ -46,6 +46,12 @@ namespace Expr
 @[inline] def iff? (p : Expr) : Option (Expr × Expr) :=
   p.app2? ``Iff
 
+@[inline] def eqOrIff? (p : Expr) : Option (Expr × Expr) :=
+  if let some (_, lhs, rhs) := p.app3? ``Eq then
+    some (lhs, rhs)
+  else
+    p.iff?
+
 @[inline] def not? (p : Expr) : Option Expr :=
   p.app1? ``Not
 
diff --git a/tests/lean/1763.lean b/tests/lean/1763.lean
new file mode 100644
index 0000000000..619b4d6ed2
--- /dev/null
+++ b/tests/lean/1763.lean
@@ -0,0 +1,16 @@
+axiom P : Prop → Prop
+
+@[congr]
+axiom P_congr (a b : Prop) (h : a ↔ b) : P a ↔ P b
+
+theorem ex1 {p q : Prop} (h : p ↔ q) (h' : P q) : P p := by
+  simp [h]
+  assumption
+
+#print ex1
+
+theorem ex2 {p q : Prop} (h : p = q) (h' : P q) : P p := by
+  simp [h]
+  assumption
+
+#print ex2
diff --git a/tests/lean/1763.lean.expected.out b/tests/lean/1763.lean.expected.out
new file mode 100644
index 0000000000..b8c481d253
--- /dev/null
+++ b/tests/lean/1763.lean.expected.out
@@ -0,0 +1,4 @@
+theorem ex1 : ∀ {p q : Prop}, (p ↔ q) → P q → P p :=
+fun {p q} h h' => Eq.mpr (id (propext (P_congr p q h))) h'
+theorem ex2 : ∀ {p q : Prop}, p = q → P q → P p :=
+fun {p q} h h' => Eq.mpr (id (propext (P_congr p q (Iff.of_eq h)))) h'