max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: structural equation proof generator (#3444)

Browse source 
See new test.
This commit is contained in:
Leonardo de Moura 2024-02-21 11:42:39 -08:00 • committed by GitHub
parent ddd6342737
commit e5d2cbceaa
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/PreDefinition/Structural/Eqns.lean
View file

@ -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

10
tests/lean/run/simp_eqn_bug.lean Normal file
View file

@ -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