From 1259db13a154b0d5f101d2f874ae017b81ed4e72 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Feb 2024 22:54:52 +0100
Subject: Fix more proofs

---
 backends/lean/Base/IList/IList.lean           | 25 ++++++++++++++-----------
 backends/lean/Base/Primitives/ArraySlice.lean |  2 +-
 backends/lean/Base/Primitives/Vec.lean        |  2 +-
 3 files changed, 16 insertions(+), 13 deletions(-)

(limited to 'backends')

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
-- 
cgit v1.2.3