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

fix: Int.reduceNeg simproc (#6468)

Browse source 
This PR fixes issue #6467 


closes #6467
This commit is contained in:
Leonardo de Moura 2024-12-28 23:58:09 +01:00 • committed by GitHub
parent 3fc74854d7
commit 5930db946c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 18 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
View file

@ -49,17 +49,13 @@ If they do, they must disable the following `simprocs`.
-/
builtin_dsimproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
unless e.isAppOfArity ``Neg.neg 3 do return .continue
let arg := e.appArg!
let_expr Neg.neg _ _ arg ← e | return .continue
if arg.isAppOfArity ``OfNat.ofNat 3 then
-- We return .done to ensure `Neg.neg` is not unfolded even when `ground := true`.
return .done e
else
let some v ← fromExpr? arg | return .continue
if v < 0 then
return .done <| toExpr (- v)
else
return .done <| toExpr v
return .done <| toExpr (- v)
/-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator. -/
builtin_dsimproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do

16
tests/lean/run/6467.lean Normal file
View file

@ -0,0 +1,16 @@
theorem confuses_the_user : -(no_index (OfNat.ofNat <| nat_lit 2)) = -2 := by
simp
theorem ex : -(no_index (OfNat.ofNat <| nat_lit 2)) = (2 : Int) := by
simp only [Int.reduceNeg]
guard_target =ₛ -2 = 2
sorry
theorem its_true_really : -(no_index (OfNat.ofNat <| nat_lit 2)) = -2 := by
rfl
example : -(-(no_index (OfNat.ofNat <| nat_lit 2))) = 2 := by
simp
example : -(no_index (-(no_index (OfNat.ofNat <| nat_lit 2)))) = -(-(-(-3+1))) := by
simp