From a7323c98053ea992210f11b03e8fbeddcde57cb2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 21 Oct 2023 16:39:39 -0700
Subject: [PATCH] feat: use `forall_prop_domain_congr` in `simp` tactic

closes #1926
---
 src/Lean/Meta/Tactic/Simp/Main.lean | 36 ++++++++++++++++++++++++++++-
 tests/lean/run/1926.lean            | 10 ++++++++
 2 files changed, 45 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/1926.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index a1b2c1f63b..45f27b0b57 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -723,7 +723,41 @@ where
     if e.isArrow then
       simpArrow e
     else if (← isProp e) then
-      withLocalDecl e.bindingName! e.bindingInfo! e.bindingDomain! fun x => withNewLemmas #[x] do
+      /- The forall is a proposition. -/
+      let domain := e.bindingDomain!
+      if (← isProp domain) then
+        /-
+        The domain of the forall is also a proposition, and we can use `forall_prop_domain_congr`
+        IF we can simplify the domain.
+        -/
+        let rd ← simp domain
+        if let some h₁ := rd.proof? then
+          /- Using
+          ```
+          theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop}
+              (h₁ : p₁ = p₂)
+              (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a)
+              : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a)
+          ```
+          Remark: we should consider whether we want to add congruence lemma support for arbitrary `forall`-expressions.
+          Then, the theroem above can be marked as `@[congr]` and the following code deleted.
+          -/
+          let p₁ := domain
+          let p₂ := rd.expr
+          let q₁ := mkLambda e.bindingName! e.bindingInfo! p₁ e.bindingBody!
+          let result ← withLocalDecl e.bindingName! e.bindingInfo! p₂ fun a => withNewLemmas #[a] do
+            let prop := mkSort levelZero
+            let h₁_substr_a := mkApp6 (mkConst ``Eq.substr [levelOne]) prop (mkLambda `x .default prop (mkBVar 0)) p₂ p₁ h₁ a
+            let q_h₁_substr_a := e.bindingBody!.instantiate1 h₁_substr_a
+            let rb ← simp q_h₁_substr_a
+            let h₂ ← mkLambdaFVars #[a] (← rb.getProof)
+            let q₂ ← mkLambdaFVars #[a] rb.expr
+            let result ← mkForallFVars #[a] rb.expr
+            let proof := mkApp6 (mkConst ``forall_prop_domain_congr) p₁ p₂ q₁ q₂ h₁ h₂
+            return { expr := result, proof? := proof }
+          return result
+      let domain ← dsimp domain
+      withLocalDecl e.bindingName! e.bindingInfo! domain fun x => withNewLemmas #[x] do
         let b := e.bindingBody!.instantiate1 x
         let rb ← simp b
         let eNew ← mkForallFVars #[x] rb.expr
diff --git a/tests/lean/run/1926.lean b/tests/lean/run/1926.lean
new file mode 100644
index 0000000000..b90a705dcb
--- /dev/null
+++ b/tests/lean/run/1926.lean
@@ -0,0 +1,10 @@
+example (q : p → Prop) (h : p = True)
+  (h' : ∀(q : True → Prop), (∀ x, q x) ↔ q True.intro) :
+    (∀ h', q h') ↔ q (h.symm ▸ trivial) := by
+  simp only [h, h']
+
+theorem forall_true_left : ∀ (p : True → Prop), (∀ (x : True), p x) ↔ p True.intro := sorry
+
+example (p : Prop) (q : p → Prop) (h : p) :
+  (∀ (h2 : p), q h2) ↔ q h :=
+by simp only [h, forall_true_left]