fix: structural equation proof generator

leanprover · Feb 21, 2024 · 1fa5dc8 · 1fa5dc8
1 parent 75272cb
commit 1fa5dc8
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -37,12 +37,12 @@ where
       return ()
     else if (← tryContradiction mvarId) then
       return ()
+    else if let some mvarId ← whnfReducibleLHS? mvarId then
+      go mvarId
     else if let some mvarId ← simpMatch? mvarId then
       go mvarId
     else if let some mvarId ← simpIf? mvarId then
       go mvarId
-    else if let some mvarId ← whnfReducibleLHS? mvarId then
-      go mvarId
     else match (← simpTargetStar mvarId {} (simprocs := {})).1 with
       | TacticResultCNM.closed => return ()
       | TacticResultCNM.modified mvarId => go mvarId

diff --git a/tests/lean/run/simp_eqn_bug.lean b/tests/lean/run/simp_eqn_bug.lean
@@ -0,0 +1,10 @@
+@[simp] def f (a : Nat) (xs : List Nat) : Nat :=
+  match a with
+  | 25 => 0
+  | _  => match xs with
+   | []    => a
+   | x::xs => x + f a xs
+
+example : f 25 xs = 0 := by apply f._eq_1
+example (h : a = 25 → False) : f a [] = a := by apply f._eq_2; assumption
+example (h : a = 25 → False) : f a (x::xs) = x + f a xs := by apply f._eq_3; assumption