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

chore: simp_arith has been deprecated (#7043)

Browse source 
This PR deprecates the tactics `simp_arith`, `simp_arith!`,
`simp_all_arith` and `simp_all_arith!`. Users can just use the `+arith`
option.
This commit is contained in:
Leonardo de Moura 2025-02-11 19:55:45 -08:00 • committed by GitHub
parent fb2e5e5555
commit 2a67a49f31
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
59 changed files with 264 additions and 153 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/examples/bintree.lean
View file

@ -179,7 +179,7 @@ local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
`(tactic|
(have h : $lhs = $rhs :=
-- TODO: replace with linarith
by simp_arith at *; apply Nat.le_antisymm <;> assumption
by simp +arith at *; apply Nat.le_antisymm <;> assumption
try subst $lhs))
/-!

6
src/Init/Data/Array/BasicAux.lean
View file

@ -17,13 +17,13 @@ theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : a
private theorem List.size_toArrayAux (as : List α) (bs : Array α) : (as.toArrayAux bs).size = as.length + bs.size := by
induction as generalizing bs with
| nil => simp [toArrayAux]
| cons a as ih => simp_arith [toArrayAux, *]
| cons a as ih => simp +arith [toArrayAux, *]
private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Array α} (h : as.toArrayAux cs = bs.toArrayAux ds) (hlen : cs.size = ds.size) : as = bs ∧ cs = ds := by
match as, bs with
| [], [] => simp [toArrayAux] at h; simp [h]
| a::as, [] => simp [toArrayAux] at h; rw [← h] at hlen; simp_arith [size_toArrayAux] at hlen
| [], b::bs => simp [toArrayAux] at h; rw [h] at hlen; simp_arith [size_toArrayAux] at hlen
| a::as, [] => simp [toArrayAux] at h; rw [← h] at hlen; simp +arith [size_toArrayAux] at hlen
| [], b::bs => simp [toArrayAux] at h; rw [h] at hlen; simp +arith [size_toArrayAux] at hlen
| a::as, b::bs =>
simp [toArrayAux] at h
have : (cs.push a).size = (ds.push b).size := by simp [*]

6
src/Init/Data/Array/Lemmas.lean
View file

@ -1675,7 +1675,7 @@ theorem getElem_append_right' (l₁ : Array α) {l₂ : Array α} {i : Nat} (hi
rw [getElem_append_right] <;> simp [*, Nat.le_add_left]
theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂) (h : l₁.size = i) :
l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
l[i]'(eq ▸ h ▸ by simp +arith) = a := Option.some.inj <| by
rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]
simp
@ -2337,10 +2337,10 @@ theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j
← getElem?_toList]
split <;> rename_i h₂
· simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp +arith) h)).symm
split <;> rename_i h₃
· simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp +arith) h)).symm
simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
· rw [H]; split <;> rename_i h₂

10
src/Init/Data/Array/Mem.lean
View file

@ -12,11 +12,11 @@ namespace Array
theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by
cases as with | _ as =>
exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)
exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp +arith)
theorem sizeOf_get [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf (as.get i h) < sizeOf as := by
cases as with | _ as =>
simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp_arith)
simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp +arith)
@[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _ h
@ -29,8 +29,8 @@ macro "array_get_dec" : tactic =>
-- subsumed by simp
-- | with_reducible apply sizeOf_get
-- | with_reducible apply sizeOf_getElem
| (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_get ..)); simp_arith
| (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_getElem ..)); simp_arith
| (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_get ..)); simp +arith
| (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_getElem ..)); simp +arith
)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
@ -45,7 +45,7 @@ macro "array_mem_dec" : tactic =>
| with_reducible
apply Nat.lt_of_lt_of_le (Array.sizeOf_lt_of_mem ?h)
case' h => assumption
simp_arith)
simp +arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)

16
src/Init/Data/List/BasicAux.lean
View file

@ -178,15 +178,15 @@ theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.
induction as generalizing i with
| nil => cases i with
| zero => simp [List.get]
| succ => simp_arith at h'
| succ => simp +arith at h'
| cons a as ih =>
cases i with simp at h
| succ i => apply ih; simp [h]
theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as := by
induction h with
| head => simp_arith
| tail _ _ ih => exact Nat.lt_trans ih (by simp_arith)
| head => simp +arith
| tail _ _ ih => exact Nat.lt_trans ih (by simp +arith)
/-- This tactic, added to the `decreasing_trivial` toolbox, proves that
`sizeOf a < sizeOf as` when `a ∈ as`, which is useful for well founded recursions
@ -197,7 +197,7 @@ macro "sizeOf_list_dec" : tactic =>
| with_reducible
apply Nat.lt_of_lt_of_le (sizeOf_lt_of_mem ?h)
case' h => assumption
simp_arith)
simp +arith)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)
@ -211,8 +211,8 @@ theorem append_cancel_left {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs =
theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as = cs := by
match as, cs with
| [], [] => rfl
| [], c::cs => have aux := congrArg length h; simp_arith at aux
| a::as, [] => have aux := congrArg length h; simp_arith at aux
| [], c::cs => have aux := congrArg length h; simp +arith at aux
| a::as, [] => have aux := congrArg length h; simp +arith at aux
| a::as, c::cs => injection h with h₁ h₂; subst h₁; rw [append_cancel_right h₂]
@[simp] theorem append_cancel_left_eq (as bs cs : List α) : (as ++ bs = as ++ cs) = (bs = cs) := by
@ -227,11 +227,11 @@ theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as
theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
match as, i with
| a::as, ⟨0, _⟩ => simp_arith [get]
| a::as, ⟨0, _⟩ => simp +arith [get]
| a::as, ⟨i+1, h⟩ =>
have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
apply Nat.lt_trans ih
simp_arith
simp +arith
theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
(antisymm : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)

2
src/Init/Data/List/Lemmas.lean
View file

@ -1563,7 +1563,7 @@ theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {i : Nat} (hi :
rw [getElem_append_right] <;> simp [*, le_add_left]
theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
l[i]'(eq ▸ h ▸ by simp +arith) = a := Option.some.inj <| by
rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h]
simp

4
src/Init/Data/List/Sort/Lemmas.lean
View file

@ -152,8 +152,8 @@ theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
| a::l, b::r =>
rw [cons_merge_cons]
split
· simp_arith [length_merge s l (b::r)]
· simp_arith [length_merge s (a::l) r]
· simp +arith [length_merge s l (b::r)]
· simp +arith [length_merge s (a::l) r]
/--
The elements of `merge le xs ys` are exactly the elements of `xs` and `ys`.

2
src/Init/Data/Nat/Lemmas.lean
View file

@ -1011,7 +1011,7 @@ theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x
| 0 => simp
| x + 1 =>
rw [Nat.mul_succ, Nat.add_assoc _ m, mul_add_div m_pos x (m+y), div_eq]
simp_arith [m_pos]; rw [Nat.add_comm, Nat.add_sub_cancel]
simp +arith [m_pos]; rw [Nat.add_comm, Nat.add_sub_cancel]
theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
match x with

2
src/Init/Data/Nat/Power2.lean
View file

@ -9,7 +9,7 @@ import Init.Data.Nat.Linear
namespace Nat
theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
have : power * 2 = power + power := by simp_arith
have : power * 2 = power + power := by simp +arith
rw [this, Nat.sub_add_eq]
exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁

32
src/Init/Meta.lean
View file

@ -1509,25 +1509,35 @@ This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/
declare_simp_like_tactic simpAutoUnfold "simp! " (autoUnfold := true)
/-- `simp_arith` is shorthand for `simp` with `arith := true` and `decide := true`.
This enables the use of normalization by linear arithmetic. -/
declare_simp_like_tactic simpArith "simp_arith " (arith := true) (decide := true)
/--
`simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
-/
syntax (name := simpArith) "simp_arith " optConfig (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
/-- `simp_arith!` is shorthand for `simp_arith` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/
declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " (arith := true) (autoUnfold := true) (decide := true)
/--
`simp_arith!` has been deprecated. It was a shorthand for `simp! +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
-/
syntax (name := simpArithBang) "simp_arith! " optConfig (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
/-- `simp_all!` is shorthand for `simp_all` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/
declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " (autoUnfold := true)
/-- `simp_all_arith` combines the effects of `simp_all` and `simp_arith`. -/
declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " (arith := true) (decide := true)
/--
`simp_all_arith` has been deprecated. It was a shorthand for `simp_all +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
-/
syntax (name := simpAllArith) "simp_all_arith" optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic
/--
`simp_all_arith!` has been deprecated. It was a shorthand for `simp_all! +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
-/
syntax (name := simpAllArithBang) "simp_all_arith!" optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic
/-- `simp_all_arith!` combines the effects of `simp_all`, `simp_arith` and `simp!`. -/
declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " (arith := true) (autoUnfold := true) (decide := true)
/-- `dsimp!` is shorthand for `dsimp` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to

16
src/Init/SizeOfLemmas.lean
View file

@ -9,28 +9,28 @@ import Init.SizeOf
import Init.Data.Nat.Linear
@[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
cases a; simp_arith
cases a; simp +arith
@[simp] protected theorem BitVec.sizeOf (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1 := by
cases a; simp_arith
cases a; simp +arith
@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt8.toNat, BitVec.toNat]
cases a; simp +arith [UInt8.toNat, BitVec.toNat]
@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt16.toNat, BitVec.toNat]
cases a; simp +arith [UInt16.toNat, BitVec.toNat]
@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt32.toNat, BitVec.toNat]
cases a; simp +arith [UInt32.toNat, BitVec.toNat]
@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [UInt64.toNat, BitVec.toNat]
cases a; simp +arith [UInt64.toNat, BitVec.toNat]
@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 3 := by
cases a; simp_arith [USize.toNat, BitVec.toNat]
cases a; simp +arith [USize.toNat, BitVec.toNat]
@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 4 := by
cases a; simp_arith [Char.toNat]
cases a; simp +arith [Char.toNat]
@[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by
cases s; simp

2
src/Init/Tactics.lean
View file

@ -1797,7 +1797,7 @@ macro_rules | `(‹$type›) => `((by assumption : $type))
by the notation `arr[i]` to prove any side conditions that arise when
constructing the term (e.g. the index is in bounds of the array).
The default behavior is to just try `trivial` (which handles the case
where `i < arr.size` is in the context) and `simp_arith` and `omega`
where `i < arr.size` is in the context) and `simp +arith` and `omega`
(for doing linear arithmetic in the index).
-/
syntax "get_elem_tactic_trivial" : tactic

2
src/Lean/Compiler/LCNF/AlphaEqv.lean
View file

@ -69,7 +69,7 @@ def eqvLetValue (e₁ e₂ : LetValue) : EqvM Bool := do
let rec @[specialize] go (i : Nat) : EqvM Bool := do
if h : i < params₁.size then
let p₁ := params₁[i]
have : i < params₂.size := by simp_all_arith
have : i < params₂.size := by simp_all +arith
let p₂ := params₂[i]
unless (← eqvType p₁.type p₂.type) do return false
withFVar p₁.fvarId p₂.fvarId do

2
src/Lean/Compiler/LCNF/PassManager.lean
View file

@ -47,7 +47,7 @@ structure Pass where
Resulting phase.
-/
phaseOut : Phase := phase
phaseInv : phaseOut ≥ phase := by simp_arith
phaseInv : phaseOut ≥ phase := by simp +arith +decide
/--
The name of the `Pass`
-/

1
src/Lean/Elab/Tactic.lean
View file

@ -50,3 +50,4 @@ import Lean.Elab.Tactic.Try
import Lean.Elab.Tactic.AsAuxLemma
import Lean.Elab.Tactic.TreeTacAttr
import Lean.Elab.Tactic.ExposeNames
import Lean.Elab.Tactic.SimpArith

53
src/Lean/Elab/Tactic/SimpArith.lean Normal file
View file

@ -0,0 +1,53 @@
/-
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Elab.Tactic.Simp
import Lean.Meta.Tactic.TryThis
namespace Lean.Elab.Tactic
private def addConfigItem (stx : Syntax) (item : Syntax) : Syntax :=
let optConfig := stx[1]
let optConfig := optConfig.modifyArg 0 fun arg => mkNullNode (#[item] ++ arg.getArgs)
stx.setArg 1 optConfig
set_option hygiene false in
private def addArith (stx : Syntax) : CoreM Syntax :=
return addConfigItem stx (← `(Lean.Parser.Tactic.configItem| +arith))
set_option hygiene false in
private def addDecide (stx : Syntax) : CoreM Syntax :=
return addConfigItem stx (← `(Lean.Parser.Tactic.configItem| +decide))
private def setKind (stx : Syntax) (str : String) (kind : SyntaxNodeKind) : Syntax :=
let stx := stx.setKind kind
stx.setArg 0 (mkAtom str)
private def addSuggestions (stx : Syntax) (tokenNew : String) (kindNew : SyntaxNodeKind) : MetaM Unit := do
let stx' := setKind stx tokenNew kindNew
let stx' := stx'.unsetTrailing
let s₁ : TSyntax `tactic := ⟨← addArith stx'⟩
let s₂ : TSyntax `tactic := ⟨← addArith (← addDecide stx')⟩
Meta.Tactic.TryThis.addSuggestions stx[0] #[s₁, s₂] (origSpan? := (← getRef))
@[builtin_tactic Lean.Parser.Tactic.simpArith] def evalSimpArith : Tactic := fun stx => do
addSuggestions stx "simp" ``Parser.Tactic.simp
throwError "`simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
@[builtin_tactic Lean.Parser.Tactic.simpArithBang] def evalSimpArithBang : Tactic := fun stx => do
addSuggestions stx "simp!" ``Parser.Tactic.simpAutoUnfold
throwError "`simp_arith!` has been deprecated. It was a shorthand for `simp! +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
@[builtin_tactic Lean.Parser.Tactic.simpAllArith] def evalSimpAllArith : Tactic := fun stx => do
addSuggestions stx "simp_all" ``Parser.Tactic.simpAll
throwError "`simp_all_arith` has been deprecated. It was a shorthand for `simp_all +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
@[builtin_tactic Lean.Parser.Tactic.simpAllArithBang] def evalSimpAllArithBang : Tactic := fun stx => do
addSuggestions stx "simp_all!" ``Parser.Tactic.simpAllAutoUnfold
throwError "`simp_all_arith!` has been deprecated. It was a shorthand for `simp_all! +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
end Lean.Elab.Tactic

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

@ -80,7 +80,7 @@ structure Context where
we don't miss simplification opportunities. For example, consider the following:
```
example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
simp_arith only
simp +arith only
...
```
If we don't set `Result.cache := false` for the first `x + x`, then we get

20
src/Std/Sat/AIG/CachedLemmas.lean
View file

@ -73,7 +73,7 @@ theorem mkAtomCached_le_size (aig : AIG α) (var : α) :
dsimp only [mkAtomCached]
split
· simp
· simp_arith
· simp +arith
instance : LawfulOperator α (fun _ => α) mkAtomCached where
le_size := mkAtomCached_le_size
@ -147,7 +147,7 @@ theorem mkConstCached_le_size (aig : AIG α) (val : Bool) :
dsimp only [mkConstCached]
split
· simp
· simp_arith
· simp +arith
instance : LawfulOperator α (fun _ => Bool) mkConstCached where
le_size := mkConstCached_le_size
@ -189,18 +189,10 @@ theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) :
dsimp only [go]
split
· simp
· split
· simp_arith [mkConstCached_le_size]
· simp_arith [mkConstCached_le_size]
· simp_arith [mkConstCached_le_size]
· simp_arith [mkConstCached_le_size]
· simp_arith
· simp_arith
· simp_arith
· simp_arith
· split
· simp_arith
· split <;> simp_arith [mkConstCached_le_size]
· split <;> try simp +arith [mkConstCached_le_size]
split
· simp +arith
· split <;> simp +arith [mkConstCached_le_size]
/--
`AIG.mkGateCached` never shrinks the underlying AIG.

6
src/Std/Sat/AIG/Lemmas.lean
View file

@ -70,7 +70,7 @@ theorem denote_projected_entry' {entry : Entrypoint α} :
-/
theorem mkGate_le_size (aig : AIG α) (input : GateInput aig) :
aig.decls.size ≤ (aig.mkGate input).aig.decls.size := by
simp_arith [mkGate]
simp +arith [mkGate]
/--
The AIG produced by `AIG.mkGate` agrees with the input AIG on all indices that are valid for both.
@ -125,7 +125,7 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
-/
theorem mkAtom_le_size (aig : AIG α) (var : α) :
aig.decls.size ≤ (aig.mkAtom var).aig.decls.size := by
simp_arith [mkAtom]
simp +arith [mkAtom]
/--
The AIG produced by `AIG.mkAtom` agrees with the input AIG on all indices that are valid for both.
@ -164,7 +164,7 @@ theorem denote_mkAtom {aig : AIG α} :
-/
theorem mkConst_le_size (aig : AIG α) (val : Bool) :
aig.decls.size ≤ (aig.mkConst val).aig.decls.size := by
simp_arith [mkConst]
simp +arith [mkConst]
/--
The AIG produced by `AIG.mkConst` agrees with the input AIG on all indices that are valid for both.

2
src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
View file

@ -43,7 +43,7 @@ theorem denote_blastShiftConcat (aig : AIG α) (target : ShiftConcatInput aig w)
intro idx hidx
unfold blastShiftConcat
have hidx_lt : idx < 1 + w := by omega
by_cases hidx_eq : idx = 0 <;> simp_arith [hidx_lt, hidx_eq, RefVec.get_append]
by_cases hidx_eq : idx = 0 <;> simp +arith [hidx_lt, hidx_eq, RefVec.get_append]
theorem denote_blastShiftConcat_eq_shiftConcat (aig : AIG α) (target : ShiftConcatInput aig w)
(x : BitVec w) (b : Bool) (assign : α → Bool)

4
tests/lean/1081.lean
View file

@ -22,10 +22,10 @@ namespace Vector'
theorem insert_at_0_eq_cons1 (a: α) (v: Vector' α n): v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v :=
rfl -- Error, it does not hold by reflexivity because the recursion is on v
example (a : α) : nil.insert a ⟨0, by simp_arith⟩ = cons a nil :=
example (a : α) : nil.insert a ⟨0, by simp +arith⟩ = cons a nil :=
rfl
example (a : α) (b : α) (bs : Vector' α n) : (cons b bs).insert a ⟨0, by simp_arith⟩ = cons a (cons b bs) :=
example (a : α) (b : α) (bs : Vector' α n) : (cons b bs).insert a ⟨0, by simp +arith⟩ = cons a (cons b bs) :=
rfl
theorem insert_at_0_eq_cons2 (a: α) (v: Vector' α n): v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v := by

4
tests/lean/allFieldForConstants.lean
View file

@ -89,13 +89,13 @@ attribute [simp] List.foldl
theorem foldl_init (s : Nat) (xs : List String) : (xs.foldl (init := s) fun sum s => sum + s.length) = s + (xs.foldl (init := 0) fun sum s => sum + s.length) := by
induction xs generalizing s with
| nil => simp
| cons x xs ih => simp_arith [ih x.length, ih (s + x.length)]
| cons x xs ih => simp +arith [ih x.length, ih (s + x.length)]
theorem listStringLen_append (xs ys : List String) : listStringLen (xs ++ ys) = listStringLen xs + listStringLen ys := by
simp [listStringLen]
induction xs with
| nil => simp
| cons x xs ih => simp_arith [foldl_init x.length, foldl_init (_ + _), ih]
| cons x xs ih => simp +arith [foldl_init x.length, foldl_init (_ + _), ih]
mutual
theorem listStringLen_flat (f : Foo) : listStringLen (flat f) = textLength f := by

2
tests/lean/run/1228.lean
View file

@ -20,7 +20,7 @@ namespace Foo
match s' with
| foo s' =>
have: Bar s' := sorry
have hterm: sizeOf s' < sizeOf s := by simp_all_arith
have hterm: sizeOf s' < sizeOf s := by simp_all +arith
exact ex₂ this
termination_by sizeOf s

2
tests/lean/run/1236.lean
View file

@ -1 +1 @@
example: x ≤ x * 2 := by simp_arith
example: x ≤ x * 2 := by simp +arith

4
tests/lean/run/1302.lean
View file

@ -3,10 +3,10 @@
example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
simp
example (a : Bool) : (a :: as).get ⟨0, by simp_arith⟩ = a := by
example (a : Bool) : (a :: as).get ⟨0, by simp +arith⟩ = a := by
simp
example (a : Bool) : (a :: as).get ⟨0, by simp_arith⟩ = a := by
example (a : Bool) : (a :: as).get ⟨0, by simp +arith⟩ = a := by
simp
example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by

4
tests/lean/run/2042.lean
View file

@ -13,7 +13,7 @@ by
funext x
simp -- unfolds `foo`
trace_state
simp_arith
simp +arith
@[simp] def boo : Nat → Nat
| a => 2 * a
@ -30,4 +30,4 @@ by
funext x
simp -- unfolds `boo`
trace_state
simp_arith
simp +arith

2
tests/lean/run/2615.lean
View file

@ -1,2 +1,2 @@
-- `simp +arith` supports integers now
theorem huh (x : Int) : x + 1 = 1 + x := by simp_arith
theorem huh (x : Int) : x + 1 = 1 + x := by simp +arith

4
tests/lean/run/addDecorationsWithoutPartial.lean
View file

@ -46,7 +46,7 @@ unsafe def replaceUnsafe (e : Expr) (f? : (e' : Expr) → sizeOf e' ≤ sizeOf e
end ReplaceImpl'
local macro "dec " h:ident : term => `(by apply Nat.le_trans _ $h; simp_arith)
local macro "dec " h:ident : term => `(by apply Nat.le_trans _ $h; simp +arith)
@[implemented_by ReplaceImpl'.replaceUnsafe]
def replace' (e0 : Expr) (f? : (e : Expr) → sizeOf e ≤ sizeOf e0 → Option Expr) : Expr :=
@ -77,4 +77,4 @@ def addDecorations (e : Expr) : Expr :=
let rest := Expr.forallE name newType newBody data
some <| mkApp2 (mkConst `SlimCheck.NamedBinder) (mkStrLit n) rest
| _ => none
decreasing_by all_goals exact Nat.le_trans (by simp_arith) h
decreasing_by all_goals exact Nat.le_trans (by simp +arith) h

2
tests/lean/run/bigop.lean
View file

@ -28,7 +28,7 @@ instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) where
def finElems (n : Nat) : List (Fin n) :=
match n with
| 0 => []
| n+1 => go (n+1) n (by simp_arith)
| n+1 => go (n+1) n (by simp +arith)
where
go (n : Nat) (i : Nat) (h : i < n) : List (Fin n) :=
match i with

4
tests/lean/run/binrec.lean
View file

@ -29,8 +29,8 @@ theorem Nat.div2_lt (h : n ≠ 0) : n / 2 < n := by
| n+4 =>
rw [div_eq, if_pos]
refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
exact @div2_lt (n+2) (by simp_arith)
simp_arith
exact @div2_lt (n+2) (by simp +arith)
simp +arith
@[specialize]
def Nat.binrec

4
tests/lean/run/caseTacInMacros.lean
View file

@ -4,7 +4,7 @@ macro "mymacro1 " h:ident : tactic =>
`(tactic| {
cases $h:ident with
| zero => decide
| succ => simp_arith [f]
| succ => simp +arith [f]
})
example : f n > 0 := by
@ -14,7 +14,7 @@ macro "mymacro2 " h:ident : tactic =>
`(tactic| {
cases $h:ident
case zero => decide
case succ => simp_arith [f]
case succ => simp +arith [f]
})
example : f n > 0 := by

12
tests/lean/run/combinatorsAndWF.lean
View file

@ -5,12 +5,12 @@ where
match cs with
| [] => a
| c :: cs =>
have : sizeOf c < sizeOf (c :: cs) := by simp_arith
have : sizeOf c < sizeOf (c :: cs) := by simp +arith
-- TODO: simplify using linarith
have h₁ : sizeOf c < sizeOf bs := Nat.lt_of_lt_of_le this h
have : sizeOf cs + (sizeOf c + 1) = sizeOf c + sizeOf cs + 1 := by simp_arith
have : sizeOf cs + (sizeOf c + 1) = sizeOf c + sizeOf cs + 1 := by simp +arith
have : sizeOf cs ≤ sizeOf c + sizeOf cs + 1 := by rw [← this]; apply Nat.le_add_right
have h₂ : sizeOf cs ≤ sizeOf bs := by simp_arith at h; apply Nat.le_trans this h
have h₂ : sizeOf cs ≤ sizeOf bs := by simp +arith at h; apply Nat.le_trans this h
go (f a c h₁) cs h₂
theorem List.foldl_wf_eq [SizeOf β] (bs : List β) (init : α) (f : α → β → α) : bs.foldl_wf init (fun a b _ => f a b) = bs.foldl f init := by
@ -56,12 +56,12 @@ where
match cs with
| [] => []
| c :: cs =>
have : sizeOf c < sizeOf (c :: cs) := by simp_arith
have : sizeOf c < sizeOf (c :: cs) := by simp +arith
-- TODO: simplify using linarith
have h₁ : sizeOf c < sizeOf as := Nat.lt_of_lt_of_le this h
have : sizeOf cs + (sizeOf c + 1) = sizeOf c + sizeOf cs + 1 := by simp_arith
have : sizeOf cs + (sizeOf c + 1) = sizeOf c + sizeOf cs + 1 := by simp +arith
have : sizeOf cs ≤ sizeOf c + sizeOf cs + 1 := by rw [← this]; apply Nat.le_add_right
have h₂ : sizeOf cs ≤ sizeOf as := by simp_arith at h; apply Nat.le_trans this h
have h₂ : sizeOf cs ≤ sizeOf as := by simp +arith at h; apply Nat.le_trans this h
f c h₁ :: go cs h₂
theorem List.map_wf_eq [SizeOf α] (as : List α) (f : α → β) : as.map_wf (fun a _ => f a) = as.map f := by

4
tests/lean/run/congrTactic.lean
View file

@ -12,11 +12,11 @@ def f (p : Prop) (a : Nat) (h : a > 0) [Decidable p] : Nat :=
else
a + 1
example (h : a = b) : f True (a + 1) (by simp_arith) = f (0 = 0) (b + 1) (by simp_arith) := by
example (h : a = b) : f True (a + 1) (by simp +arith) = f (0 = 0) (b + 1) (by simp +arith) := by
congr
decide
example (h : a = b) : f True (a + 1) (by simp_arith) = f (0 = 0) (b + 1) (by simp_arith) := by
example (h : a = b) : f True (a + 1) (by simp +arith) = f (0 = 0) (b + 1) (by simp +arith) := by
congr 1
· decide
· show a + 1 = b + 1

6
tests/lean/run/constProp.lean
View file

@ -419,11 +419,11 @@ def State.length_erase_le (σ : State) (x : Var) : (σ.erase x).length ≤ σ.le
| [] => simp
| (y, v) :: σ =>
by_cases hxy : x = y <;> simp [hxy]
next => exact Nat.le_trans (length_erase_le σ y) (by simp_arith)
next => simp_arith [length_erase_le σ x]
next => exact Nat.le_trans (length_erase_le σ y) (by simp +arith)
next => simp +arith [length_erase_le σ x]
def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.length.succ :=
Nat.lt_of_le_of_lt (length_erase_le ..) (by simp_arith)
Nat.lt_of_le_of_lt (length_erase_le ..) (by simp +arith)
@[simp] def State.join (σ₁ σ₂ : State) : State :=
match σ₁ with

4
tests/lean/run/conv2.lean
View file

@ -1,12 +1,12 @@
opaque f (a : Nat) (h : a > 0) : Nat
example (h : a = b) : f (a + 1) (by simp_arith) = f (1 + b) (by simp_arith) := by
example (h : a = b) : f (a + 1) (by simp +arith) = f (1 + b) (by simp +arith) := by
conv => lhs; congr; rw [h]
conv => lhs; congr; rw [Nat.add_comm]
opaque g (p : Prop) [Decidable p] (a : Nat) (h : a > 0) : Nat
example (h : a = b) : g True (a + 1) (by simp_arith) = g (1+1=2) (1 + b) (by simp_arith) := by
example (h : a = b) : g True (a + 1) (by simp +arith) = g (1+1=2) (1 + b) (by simp +arith) := by
conv =>
lhs
congr

6
tests/lean/run/elabAsElim.lean
View file

@ -34,10 +34,10 @@ def f3' (x : Nat) : (Nat → Nat) → Nat → Nat :=
x.casesOn
def f4 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
xs.casesOn (by intros; contradiction) (by intros; simp_arith)
xs.casesOn (by intros; contradiction) (by intros; simp +arith)
def f5 (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
xs.casesOn (by intros; contradiction) (by intros; simp_arith) h
xs.casesOn (by intros; contradiction) (by intros; simp +arith) h
def f6 (x : Nat) :=
2 * x.casesOn 0 id
@ -50,7 +50,7 @@ def f7 (xs : Vec α n) : Nat :=
xs.casesOn (a := 10) 0
def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
@List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith)
@List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp +arith)
def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h

2
tests/lean/run/grind_t1.lean
View file

@ -228,7 +228,7 @@ example (P Q : Prop) : (¬P → ¬Q) ↔ (Q → P) := by
example {α} (a b c : α) [LE α] :
¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b := by
simp_arith -- should not fail
simp +arith -- should not fail
sorry
example {α} (a b c : α) [LE α] :

2
tests/lean/run/inductionLetIssue.lean
View file

@ -13,7 +13,7 @@ def f (x? : Option Nat) (hp : P x?) : { r? : Option Nat // P r? } :=
have : x > 0 := by
cases h₂ : x with
| zero => have := aux x? hp h₁; simp [x] at h₂; simp [h₂] at this; done
| succ x' => simp_arith
| succ x' => simp +arith
⟨some x, .somePos this⟩
else
⟨none, .none⟩

6
tests/lean/run/issue5384.lean
View file

@ -3,11 +3,11 @@ def bad (n : Nat) : Nat :=
if h : n = 0 then 0 else bad (n / 2)
termination_by n
theorem foo : 2 * bad 42000 = bad 42000 + bad 42000 := by simp_arith
theorem foo : 2 * bad 42000 = bad 42000 + bad 42000 := by simp +arith
theorem foo2 (h : 2 * bad 42000 = bad 42000 + bad 42000 + 1) : False := by simp_arith at h
theorem foo2 (h : 2 * bad 42000 = bad 42000 + bad 42000 + 1) : False := by simp +arith at h
theorem foo3 (h : bad 42000 + bad 42000 = x) : (2 * bad 42000 = x) := by simp_arith at h; assumption
theorem foo3 (h : bad 42000 + bad 42000 = x) : (2 * bad 42000 = x) := by simp +arith at h; assumption
@[irreducible] def f : Nat → Nat := fun x => x

2
tests/lean/run/lazyListRotateUnfoldProof.lean
View file

@ -18,7 +18,7 @@ end LazyList
def rotate (f : LazyList τ) (r : List τ) (a : LazyList τ)
(h : f.length + 1 = r.length) : LazyList τ :=
match r with
| List.nil => False.elim (by simp_arith [LazyList.length] at h)
| List.nil => False.elim (by simp +arith [LazyList.length] at h)
| y::r' =>
match f.force with
| none => LazyList.cons y a

6
tests/lean/run/mergeSortCPDT.lean
View file

@ -30,11 +30,11 @@ theorem List.length_split_of_atLeast2 {as : List α} (h : as.atLeast2) : as.spli
| [_, _, _] => simp (config := { decide := true }) [split]
| a::b::c::d::as =>
-- TODO: simplify using linear arith and more automation
have : (c::d::as).atLeast2 := by simp_arith
have : (c::d::as).atLeast2 := by simp +arith
have ih := length_split_of_atLeast2 this
simp_arith [split] at ih |-
simp +arith [split] at ih |-
have ⟨ih₁, ih₂⟩ := ih
exact ⟨Nat.le_trans ih₁ (by simp_arith), Nat.le_trans ih₂ (by simp_arith)⟩
exact ⟨Nat.le_trans ih₁ (by simp +arith), Nat.le_trans ih₂ (by simp +arith)⟩
def List.mergeSort' (p : α → α → Bool) (as : List α) : List α :=
if h : as.atLeast2 then

4
tests/lean/run/mutualDefThms.lean
View file

@ -38,13 +38,13 @@ attribute [simp] List.foldl
theorem foldl_init (s : Nat) (xs : List String) : (xs.foldl (init := s) fun sum s => sum + s.length) = s + (xs.foldl (init := 0) fun sum s => sum + s.length) := by
induction xs generalizing s with
| nil => simp
| cons x xs ih => simp_arith [ih x.length, ih (s + x.length)]
| cons x xs ih => simp +arith [ih x.length, ih (s + x.length)]
theorem listStringLen_append (xs ys : List String) : listStringLen (xs ++ ys) = listStringLen xs + listStringLen ys := by
simp [listStringLen]
induction xs with
| nil => simp
| cons x xs ih => simp_arith [foldl_init x.length, foldl_init (_ + _), ih]
| cons x xs ih => simp +arith [foldl_init x.length, foldl_init (_ + _), ih]
mutual
theorem listStringLen_flat (f : Foo) : listStringLen (flat f) = textLength f := by

6
tests/lean/run/no_grind_constProp.lean
View file

@ -290,11 +290,11 @@ def State.length_erase_le (σ : State) (x : Var) : (σ.erase x).length ≤ σ.le
| [] => simp
| (y, v) :: σ =>
by_cases hxy : x = y <;> simp [hxy]
next => exact Nat.le_trans (length_erase_le σ y) (by simp_arith)
next => simp_arith [length_erase_le σ x]
next => exact Nat.le_trans (length_erase_le σ y) (by simp +arith)
next => simp +arith [length_erase_le σ x]
def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.length.succ :=
Nat.lt_of_le_of_lt (length_erase_le ..) (by simp_arith)
Nat.lt_of_le_of_lt (length_erase_le ..) (by simp +arith)
@[simp] def State.join (σ₁ σ₂ : State) : State :=
match σ₁ with

4
tests/lean/run/posView.lean
View file

@ -29,8 +29,8 @@ inductive PosView where
and it will be applied automatically for us. -/
theorem sizeof_lt_of_view_eq (h : Pos.view p₁ = PosView.succ p₂) : sizeOf p₂ < sizeOf p₁ := by
match p₁, p₂ with
| { pred := Nat.succ n }, { pred := Nat.succ m } => simp [Pos.view] at h; simp_arith [h]
| { pred := Nat.succ n }, { pred := 0 } => simp [Pos.view] at h; simp_arith [h]
| { pred := Nat.succ n }, { pred := Nat.succ m } => simp [Pos.view] at h; simp +arith [h]
| { pred := Nat.succ n }, { pred := 0 } => simp [Pos.view] at h; simp +arith [h]
| { pred := 0 }, _ => simp [Pos.view] at h
/-- `1` as notation for `PosView.one` -/

2
tests/lean/run/seval1.lean
View file

@ -9,7 +9,7 @@ example (h : y = 2) : f x = x + y := by
def g (x : Nat) := x + x
@[seval] theorem g_eq : g x = 2 * x := by
simp_arith [g]
simp +arith [g]
example (h : y = 2) : g x + 2 = 2 * x + y := by
fail_if_success simp

4
tests/lean/run/shrinkFn.lean
View file

@ -4,6 +4,6 @@ class Sampleable (α : Type u) [SizeOf α] where
shrink : shrinkFn α := fun _ => []
def Prod.shrink [SizeOf α] [SizeOf β] (shrA : shrinkFn α) (shrB : shrinkFn β) : shrinkFn (α × β) := fun (fst, snd) =>
let shrink1 := shrA fst |>.map fun ⟨x, _⟩ => ⟨(x, snd), by simp_all_arith⟩
let shrink2 := shrB snd |>.map fun ⟨x, _⟩ => ⟨(fst, x), by simp_all_arith⟩
let shrink1 := shrA fst |>.map fun ⟨x, _⟩ => ⟨(x, snd), by simp_all +arith⟩
let shrink2 := shrB snd |>.map fun ⟨x, _⟩ => ⟨(fst, x), by simp_all +arith⟩
shrink1 ++ shrink2

8
tests/lean/run/simpArith1.lean
View file

@ -2,18 +2,18 @@ theorem ex1 : a + b < b + 1 + a + c := by
simp (config := { arith := true })
theorem ex2 : a + b < b + 1 + a + c := by
simp_arith
simp +arith
theorem ex3 : a + (fun x => x) b < b + 1 + a + c := by
simp_arith
simp +arith
theorem ex5 (h : a + d + b > b + 1 + (a + (c + c) + d)) : False := by
simp_arith at h
simp +arith at h
#print ex5
theorem ex6 (p : Nat → Prop) (h : p (a + 1 + a + 2 + b)) : p (2*a + b + 3) := by
simp_arith at h
simp +arith at h
assumption
#print ex6

4
tests/lean/run/simpArithCacheIssue.lean
View file

@ -5,7 +5,7 @@ h : y = 0
-/
#guard_msgs in
example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
simp_arith only
simp +arith only
/-
This is a test for a `simp` cache issue where the following incorrect goal was being
produced.
@ -21,5 +21,5 @@ example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
simp [h]
example (x y : Nat) (h : y = 0) : id (x + x) = id ((x + x) + y) := by
simp_arith only
simp +arith only
simp [h]

14
tests/lean/run/simpAutoUnfold.lean
View file

@ -20,18 +20,18 @@ def g : Nat → Nat
| n+1 => n + 2
example (a : Nat) : g a > 0 := by
cases a <;> simp_arith!
cases a <;> simp! +arith
example (a : Nat) : g a > 0 := by
cases a <;> simp_arith!
cases a <;> simp! +arith
example (a : Nat) : g a > 0 := by
cases a <;> simp_arith! [-g]
simp_arith!
cases a <;> simp! +arith +decide [-g]
simp! +arith
example (a : Nat) (h : b + 2 = 2) : g a > b := by
cases a <;> simp_all_arith!
cases a <;> simp_all! +arith
example (a : Nat) (h : b + 2 = 2) : g a > b := by
cases a <;> simp_all_arith! [-g]
simp_arith!
cases a <;> simp_all! +arith +decide [-g]
simp! +arith +decide

55
tests/lean/run/simp_arith_deprecated.lean Normal file
View file

@ -0,0 +1,55 @@
/--
info: Try these:
• simp +arith
• simp +arith +decide
---
error: `simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented.
-/
#guard_msgs in
example : x + 2 = 1 + 1 + x := by
simp_arith
/--
info: Try these:
• simp +arith [h, id] at h₂
• simp +arith +decide [h, id] at h₂
---
error: `simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented.
-/
#guard_msgs in
example (h : x = y) (h₂ : y + 2 = 1 + 1 + x) : True := by
simp_arith [h, id] at h₂
/--
info: Try these:
• simp! +arith [h, id] at h₂
• simp! +arith +decide [h, id] at h₂
---
error: `simp_arith!` has been deprecated. It was a shorthand for `simp! +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented.
-/
#guard_msgs in
example (h : x = y) (h₂ : y + 2 = 1 + 1 + x) : True := by
simp_arith! [h, id] at h₂
/--
info: Try these:
• simp_all +arith
• simp_all +arith +decide
---
error: `simp_all_arith` has been deprecated. It was a shorthand for `simp_all +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented.
-/
#guard_msgs in
example (h : x = y) (h₂ : y + 2 = 1 + 1 + x) : True := by
simp_all_arith
/--
info: Try these:
• simp_all! +arith
• simp_all! +arith +decide
---
error: `simp_all_arith!` has been deprecated. It was a shorthand for `simp_all! +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented.
-/
#guard_msgs in
example (h : x = y) (h₂ : y + 2 = 1 + 1 + x) : True := by
simp_all_arith!

8
tests/lean/run/simproc1.lean
View file

@ -17,21 +17,21 @@ run_meta do
example : x + foo 2 = 12 + x := by
set_option simprocs false in fail_if_success simp
simp_arith
simp +arith
example : x + foo 2 = 12 + x := by
-- `simp only` must not use the default simproc set
fail_if_success simp only
simp_arith
simp +arith
example : x + foo 2 = 12 + x := by
-- `simp only` does not use the default simproc set, but we can provide simprocs as arguments
simp only [reduceFoo]
simp_arith
simp +arith
example : x + foo 2 = 12 + x := by
-- We can use `-` to disable `simproc`s
fail_if_success simp [-reduceFoo]
simp_arith
simp +arith
example (x : Nat) (h : x < 86) : ¬100 ≤ x + 14 := by simp; exact h

12
tests/lean/run/splitList.lean
View file

@ -15,7 +15,7 @@ def splitList : (l : List α) → ListSplit l
theorem splitList_length (as : List α) (h₁ : as.length > 1) (h₂ : as = bs) : (splitList as).left.length < bs.length ∧ (splitList as).right.length < bs.length := by
match as with
| [] => contradiction
| a :: as => simp_arith [← h₂, splitList]; simp_arith at h₁; assumption
| a :: as => simp +arith [← h₂, splitList]; simp +arith at h₁; assumption
def len : List α → Nat
| [] => 0
@ -27,10 +27,10 @@ def len : List α → Nat
| ListSplit.split fst snd =>
-- Remark: `match` refined `h₁`s type to `h₁ : fst ++ snd = a :: b :: as`
-- h₂ : HEq (splitList l) (ListSplit.split fst snd)
have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
have := splitList_length (fst ++ snd) (by simp +arith [h₁]) h₁
-- The following two proofs ase used to justify the recursive applications `len fst` and `len snd`
have dec₁ : fst.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
have dec₂ : snd.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
have dec₁ : fst.length < as.length + 2 := by subst l; simp +arith [eq_of_heq h₂] at this |- ; simp [this]
have dec₂ : snd.length < as.length + 2 := by subst l; simp +arith [eq_of_heq h₂] at this |- ; simp [this]
len fst + len snd
termination_by xs => xs.length
@ -78,9 +78,9 @@ def len : List α → Nat
termination_by xs => xs.length
decreasing_by
all_goals
have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
have := splitList_length (fst ++ snd) (by simp +arith [h₁]) h₁
subst h₂
simp_arith [eq_of_heq h₃] at this |- ; simp [this]
simp +arith [eq_of_heq h₃] at this |- ; simp [this]
-- The equational theorems are
#check @len.eq_1

4
tests/lean/run/treeNode.lean
View file

@ -9,7 +9,7 @@ def treeToList (t : TreeNode) : List String :=
let mut r := [name]
for h : child in children do
-- We will not this the following `have` in the future
have : sizeOf child < 1 + sizeOf name + sizeOf children := Nat.lt_trans (List.sizeOf_lt_of_mem h) (by simp_arith)
have : sizeOf child < 1 + sizeOf name + sizeOf children := Nat.lt_trans (List.sizeOf_lt_of_mem h) (by simp +arith)
r := r ++ treeToList child
return r
@ -28,7 +28,7 @@ end
theorem length_treeToList_eq_numNames (t : TreeNode) : (treeToList t).length = numNames t := by
match t with
| .mkLeaf .. => simp [treeToList, numNames]
| .mkNode _ cs => simp_arith [numNames, helper cs]
| .mkNode _ cs => simp +arith [numNames, helper cs]
where
helper (cs : List TreeNode) : (cs.map treeToList).flatten.length = numNamesLst cs := by
match cs with

2
tests/lean/run/unfoldMany.lean
View file

@ -4,4 +4,4 @@ def g (x : Nat) := f x + f x
example : g x > 0 := by
unfold g f
simp_arith
simp +arith

2
tests/lean/run/wfForIn.lean
View file

@ -5,5 +5,5 @@ def printFns : Term → IO Unit
| Term.app f args => do
IO.println f
for h : arg in args do
have : sizeOf arg < 1 + sizeOf f + sizeOf args := Nat.lt_trans (List.sizeOf_lt_of_mem h) (by simp_arith)
have : sizeOf arg < 1 + sizeOf f + sizeOf args := Nat.lt_trans (List.sizeOf_lt_of_mem h) (by simp +arith)
printFns arg

2
tests/lean/run/zetaDSimpIssue.lean
View file

@ -5,4 +5,4 @@ def f (x : Nat) :=
example : f x = 2*x + 2 := by
dsimp [f]
guard_target =ₛ x + 1 + (x + 1) = 2*x + 2
simp_arith
simp +arith

2
tests/lean/splitIssue.lean
View file

@ -8,7 +8,7 @@ def f (x : Nat) : Nat :=
example : f x = 2*x + 1 := by
unfold f
split
next h => simp_arith [g] at h
next h => simp +arith [g] at h
next y h =>
trace_state
-- split tactic should *not* rewrite `g x` to `Nat.succ y`

4
tests/lean/wildcardAlt.lean
View file

@ -17,10 +17,10 @@ example (x : Foo) : bla x > 0 := by
example (x : Foo) : bla x > 0 := by
cases x with
| c1 x => simp_arith [bla]
| c1 x => simp +arith [bla]
| _ => decide
example (x : Foo) : bla x > 0 := by
induction x with
| c1 x => simp_arith [bla]
| c1 x => simp +arith [bla]
| _ => decide

6
tests/pkg/user_attr/UserAttr/Tst.lean
View file

@ -26,11 +26,11 @@ def getFooAttrInfo? (declName : Name) : CoreM (Option (Nat × Bool)) :=
@[my_simp] theorem g_eq : g x = x + 1 := rfl
example : f x + g x = 2*x + 3 := by
fail_if_success simp_arith -- does not apply f_eq and g_eq
simp_arith [f, g]
fail_if_success simp +arith -- does not apply f_eq and g_eq
simp +arith [f, g]
example : f x + g x = 2*x + 3 := by
simp_arith [my_simp]
simp +arith [my_simp]
example : f x = id (x + 2) := by
simp