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/IList | |
parent | f3b22b5cca9bc1154f55a81c9a82dc491074067d (diff) | |
parent | 85098d7caf5e3196c2e8f92411efd2814bfed1ea (diff) |
Merge branch 'son/update-lean' into has-int-pred
Diffstat (limited to 'backends/lean/Base/IList')
-rw-r--r-- | backends/lean/Base/IList/IList.lean | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean index 9fe2297f..96843f55 100644 --- a/backends/lean/Base/IList/IList.lean +++ b/backends/lean/Base/IList/IList.lean @@ -1,7 +1,6 @@ /- Complementary list functions and lemmas which operate on integers rather than natural numbers. -/ -import Std.Data.Int.Lemmas import Base.Arith import Base.Utils @@ -17,7 +16,7 @@ def len (ls : List α) : Int := theorem len_pos : 0 ≤ (ls : List α).len := by induction ls <;> simp [*] - linarith + omega instance (l: List a) : Arith.HasIntPred (l.len) where concl := 0 ≤ l.len @@ -171,6 +170,7 @@ theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : have hl : l.toNat = .succ (l.toNat - 1) := by cases hl: l.toNat <;> simp_all conv => rhs; rw[hl] + rfl termination_by l.toNat decreasing_by int_decr_tac @@ -279,12 +279,12 @@ open Arith in if heq: i = 0 then simp [*] at * have := tl.len_pos - linarith + omega else have : 0 < i := by int_tac simp [*] apply hi - linarith + omega theorem idrop_len_le (i : Int) (ls : List α) : (ls.idrop i).len ≤ ls.len := match ls with @@ -293,13 +293,13 @@ theorem idrop_len_le (i : Int) (ls : List α) : (ls.idrop i).len ≤ ls.len := if h: i = 0 then by simp [*] else have := idrop_len_le (i - 1) tl - by simp [*]; linarith + by simp [*]; omega @[simp] theorem idrop_len (i : Int) (ls : List α) (_ : 0 ≤ i) (_ : i ≤ ls.len) : (ls.idrop i).len = ls.len - i := match ls with - | [] => by simp_all; linarith + | [] => by simp_all; omega | hd :: tl => if h: i = 0 then by simp [*] else |