From 09ddf76029279eec4a9103fbc8596b0f883f2f98 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Jun 2022 18:30:11 -0700
Subject: [PATCH] feat: `simp_all` now uses dependent hypotheses for
 simplification

However, it does not simplify them.

closes #1194
---
 src/Lean/Meta/Tactic/Simp/SimpAll.lean | 10 +++++++---
 tests/lean/run/1194.lean               |  6 ++++++
 2 files changed, 13 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/1194.lean

diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
index f835817a69..09bd05f99a 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
@@ -28,7 +28,8 @@ structure State where
 abbrev M := StateRefT State MetaM
 
 private def initEntries : M Unit := do
-  let hs ← getNondepPropHyps (← get).mvarId
+  let hs ← withMVarContext (← get).mvarId do getPropHyps
+  let hsNonDeps ← getNondepPropHyps (← get).mvarId
   let mut simpThms := (← get).ctx.simpTheorems
   for h in hs do
     let localDecl ← getLocalDecl h
@@ -37,8 +38,11 @@ private def initEntries : M Unit := do
       let proof  := localDecl.toExpr
       let id     ← mkFreshUserName `h
       simpThms ← simpThms.addTheorem proof (name? := id)
-      let entry : Entry := { fvarId := fvarId, userName := localDecl.userName, id := id, type := (← instantiateMVars localDecl.type), proof := proof }
-      modify fun s => { s with entries := s.entries.push entry, ctx.simpTheorems := simpThms }
+      modify fun s => { s with ctx.simpTheorems := simpThms }
+      if hsNonDeps.contains h then
+        -- We only simplify nondependent hypotheses
+        let entry : Entry := { fvarId := fvarId, userName := localDecl.userName, id := id, type := (← instantiateMVars localDecl.type), proof := proof }
+        modify fun s => { s with entries := s.entries.push entry }
 
 private abbrev getSimpTheorems : M SimpTheoremsArray :=
   return (← get).ctx.simpTheorems
diff --git a/tests/lean/run/1194.lean b/tests/lean/run/1194.lean
new file mode 100644
index 0000000000..849a53cecc
--- /dev/null
+++ b/tests/lean/run/1194.lean
@@ -0,0 +1,6 @@
+variable {f: Fin l} {f₀: Fin 0} (h: l = 0) (h': (h▸f) = f₀)
+example: l = 0              := by simp_all
+example (h'': l ≠ 0): False := by simp_all
+
+example: l = 0              := by simp[*] at *
+example (h'': l ≠ 0): False := by simp[*] at *