diff options
| author | Son HO | 2024-06-13 22:56:37 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-13 22:56:37 +0200 |
| commit | 8e3fe11c1b31eafe14806bb513b51530c6eb99ec (patch) | |
| tree | c101e6bffaf474da394229fa4bda3147409577a0 /backends/lean/Base/Arith/Base.lean | |
| parent | 234fa36da87b672397f96098bcf832d869f2cfbb (diff) | |
| parent | d5cf75a0f8209298ad85f46249f14d5c3a24faf6 (diff) | |
Merge pull request #243 from AeneasVerif/son/update-lean
Update Lean to v4.9.0-rc1
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Arith/Base.lean | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean index 8ada4171..fb6b12e5 100644 --- a/backends/lean/Base/Arith/Base.lean +++ b/backends/lean/Base/Arith/Base.lean @@ -1,6 +1,5 @@ import Lean -import Std.Data.Int.Lemmas -import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Linarith -- Introduces a lot of useful lemmas namespace Arith @@ -21,12 +20,12 @@ theorem ne_is_lt_or_gt {x y : Int} (hne : x ≠ y) : x < y ∨ x > y := by have hne : x - y ≠ 0 := by simp intro h - have: x = y := by linarith + have: x = y := by omega simp_all have h := ne_zero_is_lt_or_gt hne match h with - | .inl _ => left; linarith - | .inr _ => right; linarith + | .inl _ => left; omega + | .inr _ => right; omega -- TODO: move? theorem add_one_le_iff_le_ne (n m : Nat) (h1 : m ≤ n) (h2 : m ≠ n) : m + 1 ≤ n := by @@ -66,7 +65,7 @@ theorem to_int_to_nat_lt (x y : ℤ) (h0 : 0 ≤ x) (h1 : x < y) : theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ) (h0 : ↑x' ≤ x) (h1 : x - ↑x' < y) : ↑(x.toNat - x') < y := by - have : 0 ≤ x := by linarith + have : 0 ≤ x := by omega simp [Int.toNat_sub_of_le, *] end Arith |