From bef161caf75a71ece51edc0d2fa14a677b5f390d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 Jan 2022 14:39:01 -0800
Subject: [PATCH] feat: add better support for discharging equation theorem
 hypotheses

---
 src/Lean/Meta/Tactic/Simp/Main.lean | 23 +++++++++++++
 tests/lean/run/eqnsAtSimp3.lean     | 52 +++++++++++++++++++++++++++++
 2 files changed, 75 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 4deac82cb6..cf8cd9a533 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -414,12 +414,35 @@ def main (e : Expr) (ctx : Context) (methods : Methods := {}) : MetaM Result :=
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
     simp e methods ctx |>.run' {}
 
+partial def isEqnThmHypothesis (e : Expr) : Bool :=
+  e.isForall && go e
+where
+  go (e : Expr) : Bool :=
+    if e.isForall then
+      go e.bindingBody!
+    else
+      e.isConstOf ``False
+
 abbrev Discharge := Expr → SimpM (Option Expr)
 
+def dischargeUsingAssumption (e : Expr) : SimpM (Option Expr) := do
+  (← getLCtx).findDeclRevM? fun localDecl => do
+    if localDecl.isAuxDecl then
+      return none
+    else if (← isDefEq e localDecl.type) then
+      return some localDecl.toExpr
+    else
+      return none
+
 namespace DefaultMethods
 mutual
   partial def discharge? (e : Expr) : SimpM (Option Expr) := do
+    if isEqnThmHypothesis e then
+      let r ← dischargeUsingAssumption e
+      if r.isSome then
+        return r
     let ctx ← read
+    trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
     if ctx.dischargeDepth >= ctx.config.maxDischargeDepth then
       trace[Meta.Tactic.simp.discharge] "maximum discharge depth has been reached"
       return none
diff --git a/tests/lean/run/eqnsAtSimp3.lean b/tests/lean/run/eqnsAtSimp3.lean
index adec7fff29..d634112389 100644
--- a/tests/lean/run/eqnsAtSimp3.lean
+++ b/tests/lean/run/eqnsAtSimp3.lean
@@ -23,3 +23,55 @@ theorem ex2 (x : Nat) (y : Nat) (h : y ≠ 5) : ∃ z, g (x+1) y = 2 * z := by
   trace_state
   apply Exists.intro
   rfl
+
+theorem ex3 (x : Nat) (y : Nat) (h : y = 5 → False) : ∃ z, f (x+1) y = 2 * z := by
+  simp [f, h]
+  trace_state
+  apply Exists.intro
+  rfl
+
+@[simp] def f2 (x y z : Nat) : Nat :=
+  match x, y, z with
+  | 0,   0, 0 => 1
+  | 0,   y, z => y
+  | x+1, 5, 6 => 2 * f2 x 0 1
+  | x+1, y, z => 2 * f2 x y z
+
+
+#check f2._eq_4
+
+theorem ex4 (x y z : Nat) (h : y = 5 → z = 6 → False) : ∃ w, f2 (x+1) y z = 2 * w := by
+  simp [f2, h]
+  trace_state
+  apply Exists.intro
+  rfl
+
+theorem ex5 (x y z : Nat) (h1 : y ≠ 5) : ∃ w, f2 (x+1) y z = 2 * w := by
+  simp [f2, h1]
+  apply Exists.intro
+  rfl
+
+theorem ex6 (x y z : Nat) (h2 : z ≠ 6) : ∃ w, f2 (x+1) y z = 2 * w := by
+  simp [f2, h2]
+  apply Exists.intro
+  rfl
+
+@[simp] def f3 (x y z : Nat) : Nat :=
+  match x, y, z with
+  | 0,   0, 0 => 1
+  | 0,   y, z => y
+  | x+1, 5, 6 => 4 * f3 x 0 1
+  | x+1, 6, 4 => 3 * f3 x 0 1
+  | x+1, y, z => 2 * f3 x y z
+
+#check f3._eq_5
+
+theorem ex7 (x y z : Nat) (h2 : z ≠ 6) (h3 : y ≠ 6) : ∃ w, f3 (x+1) y z = 2 * w := by
+  simp [f3, h2,  h3]
+  apply Exists.intro
+  rfl
+
+theorem ex8 (x y z : Nat) (h2 : y = 5 → z = 6 → False) (h3 : y = 6 → z = 4 → False) : ∃ w, f3 (x+1) y z = 2 * w := by
+  simp [f3, h2,  h3]
+  apply Exists.intro
+  rfl