diff options
author | Son Ho | 2024-06-17 06:16:43 +0200 |
---|---|---|
committer | Son Ho | 2024-06-17 06:16:43 +0200 |
commit | e57e6f08e5cc34bf4e9237650f5ecbab440b9ea2 (patch) | |
tree | 1e48b2d23719d72f39282213a1806591cc35c3b8 /backends/lean/Base/Arith/Base.lean | |
parent | f3b22b5cca9bc1154f55a81c9a82dc491074067d (diff) | |
parent | 85098d7caf5e3196c2e8f92411efd2814bfed1ea (diff) |
Merge branch 'son/update-lean' into has-int-pred
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 |