summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2024-02-02 22:54:52 +0100
committerSon Ho2024-02-02 22:54:52 +0100
commit1259db13a154b0d5f101d2f874ae017b81ed4e72 (patch)
tree7a1b445132a423125493d86f0703675e7c54fa53 /backends
parentdd262ccc9ea7a8528959659881060ddbb3bffcd5 (diff)
Fix more proofs
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/IList/IList.lean25
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean2
-rw-r--r--backends/lean/Base/Primitives/Vec.lean2
3 files changed, 16 insertions, 13 deletions
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index e90d1e0d..51457c20 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -66,13 +66,15 @@ theorem indexOpt_eq_index [Inhabited α] (ls : List α) (i : Int) :
i < ls.len →
ls.indexOpt i = some (ls.index i) :=
match ls with
- | [] => by simp; intros; linarith
+ | [] => by simp
| hd :: tl =>
if h: i = 0 then
by simp [*]
- else
+ else by
have hi := indexOpt_eq_index tl (i - 1)
- by simp [*]; intros; apply hi <;> int_tac
+ simp [*]; intros
+ -- TODO: there seems to be syntax errors if we don't put the parentheses below??
+ apply hi <;> (int_tac)
-- Remark: the list is unchanged if the index is not in bounds (in particular
-- if it is < 0)
@@ -83,7 +85,7 @@ def update (ls : List α) (i : Int) (y : α) : List α :=
-- Remark: the whole list is dropped if the index is not in bounds (in particular
-- if it is < 0)
-def idrop (i : Int) (ls : List α) : List α :=
+def idrop {α : Type u} (i : Int) (ls : List α) : List α :=
match ls with
| [] => []
| x :: tl => if i = 0 then x :: tl else idrop (i - 1) tl
@@ -117,7 +119,7 @@ variable {α : Type u}
def ireplicate {α : Type u} (i : ℤ) (x : α) : List α :=
if i ≤ 0 then []
else x :: ireplicate (i - 1) x
-termination_by ireplicate i x => i.toNat
+termination_by i.toNat
decreasing_by int_decr_tac
@[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update]
@@ -137,7 +139,7 @@ decreasing_by int_decr_tac
@[simp] theorem ireplicate_zero : ireplicate 0 x = [] := by rw [ireplicate]; simp
@[simp] theorem ireplicate_nzero_cons (hne : 0 < i) : ireplicate i x = x :: ireplicate (i - 1) x := by
- rw [ireplicate]; simp [*]; intro; linarith
+ rw [ireplicate]; simp [*]
@[simp]
theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : slice i j ((x :: tl) : List α) = slice (i - 1) (j - 1) tl :=
@@ -148,11 +150,12 @@ theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : s
have : i = 1 := by int_tac
simp [*, slice]
else
- have := slice_nzero_cons (i - 1) (j - 1) hd tl h
+ have hi := slice_nzero_cons (i - 1) (j - 1) hd tl h
by
conv => lhs; simp [slice, *]
- conv at this => lhs; simp [slice, *]
- simp [*, slice]
+ conv at hi => lhs; simp [slice, *]
+ simp [slice]
+ simp [*]
@[simp]
theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) :
@@ -166,7 +169,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]
-termination_by ireplicate_replicate l x h => l.toNat
+termination_by l.toNat
decreasing_by int_decr_tac
@[simp]
@@ -178,7 +181,7 @@ theorem ireplicate_len {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) :
have : 0 < l := by int_tac
have hr := ireplicate_len (l - 1) x (by int_tac)
simp [*]
-termination_by ireplicate_len l x h => l.toNat
+termination_by l.toNat
decreasing_by int_decr_tac
theorem len_eq_length (ls : List α) : ls.len = ls.length := by
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 5057fb01..c90a85b8 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -127,7 +127,7 @@ abbrev Slice.v {α : Type u} (v : Slice α) : List α := v.val
example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by
scalar_tac
-def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
+def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp; decide ⟩
-- TODO: very annoying that the α is an explicit parameter
def Slice.len (α : Type u) (v : Slice α) : Usize :=
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 12733a34..b03de15b 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -35,7 +35,7 @@ abbrev Vec.v {α : Type u} (v : Vec α) : List α := v.val
example {a: Type u} (v : Vec a) : v.length ≤ Scalar.max ScalarTy.Usize := by
scalar_tac
-def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
+def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp; decide ⟩
instance (α : Type u) : Inhabited (Vec α) := by
constructor