From 00705bba68fed61d3b0bcde2c5fe0ecc83880870 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 18:37:07 +0100
Subject: Update the failing proofs

---
 backends/lean/Base/Primitives/Vec.lean    | 26 ++++++++++++++++++++++----
 backends/lean/Base/Progress/Progress.lean |  2 +-
 2 files changed, 23 insertions(+), 5 deletions(-)

(limited to 'backends/lean')

diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index e1b7e87b..bbed6082 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -81,7 +81,7 @@ theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
   ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
   simp [insert, *]
 
-def Vec.index_usize (α : Type u) (v: Vec α) (i: Usize) : Result α :=
+def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some x => ret x
@@ -94,13 +94,13 @@ def Vec.index_usize (α : Type u) (v: Vec α) (i: Usize) : Result α :=
 @[pspec]
 theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by
+  ∃ x, v.index_usize i = ret x ∧ x = v.val.index i.val := by
   simp only [index_usize]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
   simp [*]
 
-def Vec.update_usize (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+def Vec.update_usize {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
@@ -109,7 +109,7 @@ def Vec.update_usize (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec
 @[pspec]
 theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.update_usize α i x = ret nv ∧
+  ∃ nv, v.update_usize i x = ret nv ∧
   nv.val = v.val.update i.val x
   := by
   simp only [update_usize]
@@ -151,6 +151,24 @@ def Vec.coreopsindexIndexMutInst (T I : Type)
   index_mut_back := Vec.index_mut_back T I inst
 }
 
+@[simp]
+theorem Vec.index_slice_index {α : Type} (v : Vec α) (i : Usize) :
+  Vec.index α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i =
+  Vec.index_usize v i :=
+  sorry
+
+@[simp]
+theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) :
+  Vec.index_mut α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i =
+  Vec.index_usize v i :=
+  sorry
+
+@[simp]
+theorem Vec.index_mut_back_slice_index {α : Type} (v : Vec α) (i : Usize) (x : α) :
+  Vec.index_mut_back α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i x =
+  Vec.update_usize v i x :=
+  sorry
+
 end alloc.vec
 
 end Primitives
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 24c6f912..ba63f09d 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -409,7 +409,7 @@ namespace Test
      `α : Type u` where u is quantified, while here we use `α : Type 0` -/
   example {α : Type} (v: Vec α) (i: Usize) (x : α)
     (hbounds : i.val < v.length) :
-    ∃ nv, v.update_usize α i x = ret nv ∧
+    ∃ nv, v.update_usize i x = ret nv ∧
     nv.val = v.val.update i.val x := by
     progress
     simp [*]
-- 
cgit v1.2.3