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

feat: Int.toNat simproc (#3440)

Browse source
This commit is contained in:
Leonardo de Moura 2024-02-21 09:12:14 -08:00 • committed by GitHub
parent 71cfbb26de
commit d55bab41bb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 18 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -91,11 +91,6 @@ builtin_simproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
let some v₂ ← Nat.fromExpr? e.appArg! | return .continue
return .done { expr := toExpr (v₁ ^ v₂) }
builtin_simproc [simp, seval] reduceAbs (natAbs _) := fun e => do
unless e.isAppOfArity ``natAbs 1 do return .continue
let some v ← fromExpr? e.appArg! | return .continue
return .done { expr := mkNatLit (natAbs v) }
builtin_simproc [simp, seval] reduceLT (( _ : Int) < _) := reduceBinPred ``LT.lt 4 (. < .)
builtin_simproc [simp, seval] reduceLE (( _ : Int) ≤ _) := reduceBinPred ``LE.le 4 (. ≤ .)
builtin_simproc [simp, seval] reduceGT (( _ : Int) > _) := reduceBinPred ``GT.gt 4 (. > .)
@ -105,4 +100,12 @@ builtin_simproc [simp, seval] reduceNe (( _ : Int) ≠ _) := reduceBinPred ``N
builtin_simproc [simp, seval] reduceBEq (( _ : Int) == _) := reduceBoolPred ``BEq.beq 4 (. == .)
builtin_simproc [simp, seval] reduceBNe (( _ : Int) != _) := reduceBoolPred ``bne 4 (. != .)
@[inline] def reduceNatCore (declName : Name) (op : Int → Nat) (e : Expr) : SimpM Step := do
unless e.isAppOfArity declName 1 do return .continue
let some v ← fromExpr? e.appArg! | return .continue
return .done { expr := mkNatLit (op v) }
builtin_simproc [simp, seval] reduceAbs (natAbs _) := reduceNatCore ``natAbs natAbs
builtin_simproc [simp, seval] reduceToNat (Int.toNat _) := reduceNatCore ``Int.toNat Int.toNat
end Int

10
tests/lean/run/simproc2.lean
View file

@ -10,3 +10,13 @@ example : foo x = 8 + 2 := by
fail_if_success simp [-Nat.reduceAdd]
simp only [Nat.reduceAdd]
rw [foo]
example (h : 0 = x) : (-2).toNat = x := by
simp
guard_target =ₛ 0 = x
assumption
example (h : 1 = x) : (1 : Int).toNat = x := by
simp
guard_target =ₛ 1 = x
assumption