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

fix: simp support for OfNat instances that are functions (#4481)

Browse source 
closes #4462
This commit is contained in:
Leonardo de Moura 2024-06-18 00:01:25 +02:00 • committed by GitHub
parent 3c4d6ba864
commit fca87da2d4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 27 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Simp/Main.lean
View file

@ -34,7 +34,7 @@ def Config.updateArith (c : Config) : CoreM Config := do
/-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/
def isOfNatNatLit (e : Expr) : Bool :=
e.isAppOfArity ``OfNat.ofNat 3 && e.appFn!.appArg!.isRawNatLit
e.isAppOf ``OfNat.ofNat && e.getAppNumArgs >= 3 && (e.getArg! 1).isRawNatLit
/--
If `e` is a raw Nat literal and `OfNat.ofNat` is not in the list of declarations to unfold,

26
tests/lean/run/4462.lean Normal file
View file

@ -0,0 +1,26 @@
def Matrix (α β R : Type) := α → β → R
instance [DecidableEq α] : OfNat (Matrix α α Nat) 1 where
ofNat x y := if x = y then 1 else 0
example [DecidableEq α] (x y : α) (h : x ≠ y) :
(1 : Matrix α α Nat) x y = 0 := by
guard_target =ₛ (1 : Matrix ..) x y = 0
fail_if_success simp
guard_target =ₛ (1 : Matrix ..) x y = 0
sorry
example [DecidableEq α] (x y : α) (h : x ≠ y) :
(1 : Matrix α α Nat) x y = 0 := by
guard_target =ₛ (1 : Matrix ..) x y = 0
fail_if_success dsimp
guard_target =ₛ (1 : Matrix ..) x y = 0
sorry
theorem one_eq [DecidableEq α] : (1 : Matrix α α Nat) x x = 1 := by
simp [OfNat.ofNat]
example [DecidableEq α] (x y : α) (h : x ≠ y) :
(1 : Matrix α α Nat) x y = 0 := by
guard_target =ₛ (1 : Matrix ..) x y = 0
simp [OfNat.ofNat, h]