From f7c09787c4a7457568d3d79d38b45caac4af8772 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Aug 2023 18:19:37 +0200
Subject: Start adding support for Arrays/Slices in the Lean library

---
 backends/lean/Base/Arith/Int.lean         |  31 ++-
 backends/lean/Base/Arith/Scalar.lean      |   4 +
 backends/lean/Base/IList/IList.lean       | 238 +++++++++++++++++-
 backends/lean/Base/Primitives.lean        |   1 +
 backends/lean/Base/Primitives/Array.lean  | 398 ++++++++++++++++++++++++++++++
 backends/lean/Base/Primitives/Range.lean  |  19 ++
 backends/lean/Base/Primitives/Scalar.lean |  11 +-
 backends/lean/Base/Primitives/Vec.lean    |  17 +-
 8 files changed, 680 insertions(+), 39 deletions(-)
 create mode 100644 backends/lean/Base/Primitives/Array.lean
 create mode 100644 backends/lean/Base/Primitives/Range.lean

(limited to 'backends/lean')

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 7a5bbe98..531ec94f 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -53,13 +53,21 @@ open Lean Lean.Elab Lean.Meta
 -- Explore a term by decomposing the applications (we explore the applied
 -- functions and their arguments, but ignore lambdas, forall, etc. -
 -- should we go inside?).
+-- Remark: we pretend projections are applications, and explore the projected
+-- terms.
 partial def foldTermApps (k : α → Expr → MetaM α) (s : α) (e : Expr) : MetaM α := do
-  -- We do it in a very simpler manner: we deconstruct applications,
-  -- and recursively explore the sub-expressions. Note that we do
-  -- not go inside foralls and abstractions (should we?).
-  e.withApp fun f args => do
-    let s ← k s f
-    args.foldlM (foldTermApps k) s
+  -- Explore the current expression
+  let e := e.consumeMData
+  let s ← k s e
+  -- Recurse
+  match e with
+  | .proj _ _ e' =>
+    foldTermApps k s e'
+  | .app .. =>
+    e.withApp fun f args => do
+      let s ← k s f
+      args.foldlM (foldTermApps k) s
+  | _ => pure s
 
 -- Provided a function `k` which lookups type class instances on an expression,
 -- collect all the instances lookuped by applying `k` on the sub-expressions of `e`.
@@ -83,15 +91,18 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
   let hs := HashSet.empty
   -- Explore the declarations
   let decls ← ctx.getDecls
-  decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs
+  let hs ← decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs
+  -- Also explore the goal
+  collectInstances k hs (← Tactic.getMainTarget)
 
 -- Helper
 def lookupProp (fName : String) (className : Name) (e : Expr) : MetaM (Option Expr) := do
   trace[Arith] fName
   -- TODO: do we need Lean.observing?
   -- This actually eliminates the error messages
+  trace[Arith] m!"{fName}: {e}"
   Lean.observing? do
-    trace[Arith] m!"{fName}: observing"
+    trace[Arith] m!"{fName}: observing: {e}"
     let ty ← Lean.Meta.inferType e
     let hasProp ← mkAppM className #[ty]
     let hasPropInst ← trySynthInstance hasProp
@@ -112,11 +123,11 @@ def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
 
 -- Return an instance of `PropHasImp` for `e` if it has some
 def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do
-  trace[Arith] "lookupPropHasImp"
+  trace[Arith] m!"lookupPropHasImp: {e}"
   -- TODO: do we need Lean.observing?
   -- This actually eliminates the error messages
   Lean.observing? do
-    trace[Arith] "lookupPropHasImp: observing"
+    trace[Arith] "lookupPropHasImp: observing: {e}"
     let ty ← Lean.Meta.inferType e
     trace[Arith] "lookupPropHasImp: ty: {ty}"
     let cl ← mkAppM ``PropHasImp #[ty]
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index b792ff21..db672489 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -46,4 +46,8 @@ example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
 example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   scalar_tac
 
+-- Checking that we explore the goal *and* projectors correctly
+example (x : U32 × U32) : 0 ≤ x.fst.val := by
+  scalar_tac
+
 end Arith
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 93047a1b..0b483e90 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -3,6 +3,7 @@
 
 import Std.Data.Int.Lemmas
 import Base.Arith
+import Base.Utils
 
 namespace List
 
@@ -87,6 +88,28 @@ def idrop (i : Int) (ls : List α) : List α :=
   | [] => []
   | x :: tl => if i = 0 then x :: tl else idrop (i - 1) tl
 
+def itake (i : Int) (ls : List α) : List α :=
+  match ls with
+  | [] => []
+  | hd :: tl => if i = 0 then [] else hd :: itake (i - 1) tl
+
+def slice (start end_ : Int) (ls : List α) : List α :=
+  (ls.idrop start).itake (end_ - start)
+
+def replace_slice (start end_ : Int) (l nl : List α) : List α :=
+  let l_beg := l.itake start
+  let l_end := l.idrop end_
+  l_beg ++ nl ++ l_end
+
+def allP {α : Type u} (l : List α) (p: α → Prop) : Prop :=
+  foldr (fun a r => p a ∧ r) True l
+
+def pairwise_rel
+  {α : Type u} (rel : α → α → Prop) (l: List α) : Prop
+  := match l with
+  | [] => True
+  | hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl
+
 section Lemmas
 
 variable {α : Type u} 
@@ -99,6 +122,28 @@ variable {α : Type u}
 @[simp] theorem idrop_zero : idrop 0 (ls : List α) = ls := by cases ls <;> simp [idrop]
 @[simp] theorem idrop_nzero_cons (hne : i ≠ 0) : idrop i ((x :: tl) : List α) = idrop (i - 1) tl := by simp [*, idrop]
 
+@[simp] theorem itake_nil : itake i ([] : List α) = [] := by simp [itake]
+@[simp] theorem itake_zero : itake 0 (ls : List α) = [] := by cases ls <;> simp [itake]
+@[simp] theorem itake_nzero_cons (hne : i ≠ 0) : itake i ((x :: tl) : List α) = x :: itake (i - 1) tl := by simp [*, itake]
+
+@[simp] theorem slice_nil : slice i j ([] : List α) = [] := by simp [slice]
+@[simp] theorem slice_zero : slice 0 0 (ls : List α) = [] := by cases ls <;> simp [slice]
+
+@[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 :=
+  match tl with
+  | [] => by simp [slice]; simp [*]
+  | hd :: tl =>
+    if h: i - 1 = 0 then by
+      have : i = 1 := by int_tac
+      simp [*, slice]
+    else
+      have := slice_nzero_cons (i - 1) (j - 1) hd tl h
+      by
+        conv => lhs; simp [slice, *]
+        conv at this => lhs; simp [slice, *]
+        simp [*, slice]
+
 theorem len_eq_length (ls : List α) : ls.len = ls.length := by
   induction ls
   . rfl
@@ -158,8 +203,33 @@ theorem right_len_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.len = l2'.len
   apply right_length_eq_append_eq
   assumption
 
+@[simp]
+theorem index_append_beg [Inhabited α] (i : Int) (l0 l1 : List α)
+  (_ : 0 ≤ i) (_ : i < l0.len) :
+  (l0 ++ l1).index i = l0.index i :=
+  match l0 with
+  | [] => by simp_all; int_tac
+  | hd :: tl =>
+    if hi : i = 0 then by simp_all
+    else by
+      have := index_append_beg (i - 1) tl l1 (by int_tac) (by simp_all; int_tac)
+      simp_all
+
+@[simp]
+theorem index_append_end [Inhabited α] (i : Int) (l0 l1 : List α)
+  (_ : l0.len ≤ i) (_ : i < l0.len + l1.len) :
+  (l0 ++ l1).index i = l1.index (i - l0.len) :=
+  match l0 with
+  | [] => by simp_all
+  | hd :: tl =>
+    have : ¬ i = 0 := by simp_all; int_tac
+    have := index_append_end (i - 1) tl l1 (by simp_all; int_tac) (by simp_all; int_tac)
+    -- TODO: canonize arith expressions
+    have : i - 1 - len tl = i - (1 + len tl) := by int_tac
+    by simp_all
+
 open Arith in
-theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by
+@[simp] theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by
   revert i
   induction ls <;> simp [*]
   rename_i hd tl hi
@@ -175,6 +245,136 @@ theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by
     apply hi
     linarith
 
+theorem idrop_len_le (i : Int) (ls : List α) : (ls.idrop i).len ≤ ls.len :=
+  match ls with
+  | [] => by simp
+  | hd :: tl =>
+    if h: i = 0 then by simp [*]
+    else
+      have := idrop_len_le (i - 1) tl
+      by simp [*]; linarith
+
+@[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
+  | hd :: tl =>
+    if h: i = 0 then by simp [*]
+    else
+      have := idrop_len (i - 1) tl (by int_tac) (by simp at *; int_tac)
+      by simp [*] at *; int_tac
+
+theorem itake_len_le (i : Int) (ls : List α) : (ls.itake i).len ≤ ls.len :=
+  match ls with
+  | [] => by simp
+  | hd :: tl =>
+    if h: i = 0 then by simp [*]; int_tac
+    else
+      have := itake_len_le (i - 1) tl
+      by simp [*]
+
+@[simp]
+theorem itake_len (i : Int) (ls : List α) (_ : 0 ≤ i) (_ : i ≤ ls.len) : (ls.itake i).len = i :=
+  match ls with
+  | [] => by simp_all; int_tac
+  | hd :: tl =>
+    if h: i = 0 then by simp [*]
+    else
+      have := itake_len (i - 1) tl (by int_tac) (by simp at *; int_tac)
+      by simp [*]
+
+theorem slice_len_le (i j : Int) (ls : List α) : (ls.slice i j).len ≤ ls.len := by
+  simp [slice]
+  have := ls.idrop_len_le i
+  have := (ls.idrop i).itake_len_le (j - i)
+  int_tac
+
+@[simp]
+theorem index_idrop [Inhabited α] (i : Int) (j : Int) (ls : List α)
+  (_ : 0 ≤ i) (_ : 0 ≤ j) (_ : i + j < ls.len) :
+  (ls.idrop i).index j = ls.index (i + j) :=
+  match ls with
+  | [] => by simp at *; int_tac
+  | hd :: tl =>
+    if h: i = 0 then by simp [*]
+    else by
+      have : ¬ i + j = 0 := by int_tac
+      simp [*]
+      -- TODO: rewriting rule: ¬ i = 0 → 0 ≤ i → 0 < i ?
+      have := index_idrop (i - 1) j tl (by int_tac) (by simp at *; int_tac) (by simp at *; int_tac)
+      -- TODO: canonize add/subs?
+      have : i - 1 + j = i + j - 1 := by int_tac
+      simp [*]
+
+@[simp]
+theorem index_itake [Inhabited α] (i : Int) (j : Int) (ls : List α)
+  (_ : 0 ≤ j) (_ : j < i) (_ : j < ls.len) :
+  (ls.itake i).index j = ls.index j :=
+  match ls with
+  | [] => by simp at *
+  | hd :: tl =>
+    have : ¬ 0 = i := by int_tac -- TODO: this is slightly annoying
+    if h: j = 0 then by simp [*] at *
+    else by
+      simp [*]
+      -- TODO: rewriting rule: ¬ i = 0 → 0 ≤ i → 0 < i ?
+      have := index_itake (i - 1) (j - 1) tl (by simp at *; int_tac) (by simp at *; int_tac) (by simp at *; int_tac)
+      simp [*]
+
+@[simp]
+theorem index_slice [Inhabited α] (i j k : Int) (ls : List α)
+  (_ : 0 ≤ i) (_ : j ≤ ls.len) (_ : 0 ≤ k) (_ : i + k < j) :
+  (ls.slice i j).index k = ls.index (i + k) :=
+  match ls with
+  | [] => by simp at *; int_tac
+  | hd :: tl =>
+    if h: i = 0 then by
+      simp [*, slice] at *
+      apply index_itake <;> simp_all
+      int_tac
+    else by
+      have : ¬ i + k = 0 := by int_tac
+      simp [*]
+      -- TODO: tactics simp_int_tac/simp_scalar_tac?
+      have := index_slice (i - 1) (j - 1) k tl (by simp at *; int_tac) (by simp at *; int_tac)
+                (by simp at *; int_tac) (by simp at *; int_tac)
+      have : (i - 1 + k) = (i + k - 1) := by int_tac -- TODO: canonize add/sub
+      simp [*]
+
+@[simp]
+theorem index_itake_append_beg [Inhabited α] (i j : Int) (l0 l1 : List α)
+  (_ : 0 ≤ j) (_ : j < i) (_ : i ≤ l0.len) :
+  ((l0 ++ l1).itake i).index j = l0.index j :=
+  match l0 with
+  | [] => by
+    simp at *
+    int_tac
+  | hd :: tl =>
+    have : ¬ i = 0 := by simp at *; int_tac
+    if hj : j = 0 then by simp [*]
+    else by
+      have := index_itake_append_beg (i - 1) (j - 1) tl l1 (by simp_all; int_tac) (by simp_all) (by simp_all; int_tac)
+      simp [*]
+
+@[simp]
+theorem index_itake_append_end [Inhabited α] (i j : Int) (l0 l1 : List α)
+  (_ : l0.len ≤ j) (_ : j < i) (_ : i ≤ l0.len + l1.len) :
+  ((l0 ++ l1).itake i).index j = l1.index (j - l0.len) :=
+  match l0 with
+  | [] => by
+    simp at *
+    have := index_itake i j l1 (by simp_all) (by simp_all) (by simp_all; int_tac)
+    simp [*]
+  | hd :: tl =>
+    have : ¬ i = 0 := by simp at *; int_tac
+    if hj : j = 0 then by simp_all; int_tac -- Contradiction
+    else by
+      have := index_itake_append_end (i - 1) (j - 1) tl l1 (by simp_all; int_tac) (by simp_all) (by simp_all; int_tac)
+      -- TODO: normalization of add/sub
+      have : j - 1 - len tl = j - (1 + len tl) := by int_tac
+      simp_all
+
 @[simp]
 theorem index_ne
   {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (j: ℤ) (x: α) :
@@ -251,8 +451,34 @@ theorem index_map_eq {α : Type u} {β : Type v} [Inhabited α] [Inhabited β] (
       by
         simp [*]
 
-def allP {α : Type u} (l : List α) (p: α → Prop) : Prop :=
-  foldr (fun a r => p a ∧ r) True l
+theorem replace_slice_index [Inhabited α] (start end_ : Int) (l nl : List α)
+  (_ : 0 ≤ start) (_ : start < end_) (_ : end_ ≤ l.len) (_ : nl.len = end_ - start) :
+  let l1 := l.replace_slice start end_ nl
+  (∀ i, 0 ≤ i → i < start → l1.index i = l.index i) ∧
+  (∀ i, start ≤ i → i < end_ → l1.index i = nl.index (i - start)) ∧
+  (∀ i, end_ ≤ i → i < l.len → l1.index i = l.index i)
+  := by
+  -- let s_end := s.val ++ a.val.idrop r.end_.val
+  -- We need those assumptions everywhere
+  -- have : 0 ≤ start := by scalar_tac
+  have : start ≤ l.len := by int_tac
+  simp only [replace_slice]
+  split_conjs
+  . intro i _ _
+    -- Introducing exactly the assumptions we need to make the rewriting work
+    have : i < l.len := by int_tac
+    simp_all
+  . intro i _ _
+    have : (List.itake start l).len ≤ i := by simp_all
+    have : i < (List.itake start l).len + (nl ++ List.idrop end_ l).len := by
+      simp_all; int_tac
+    simp_all
+  . intro i _ _
+    have : 0 ≤ end_ := by scalar_tac
+    have : end_ ≤ l.len := by int_tac
+    have : (List.itake start l).len ≤ i := by simp_all; int_tac
+    have : i < (List.itake start l).len + (nl ++ List.idrop end_ l).len := by simp_all
+    simp_all
 
 @[simp]
 theorem allP_nil {α : Type u} (p: α → Prop) : allP [] p :=
@@ -263,12 +489,6 @@ theorem allP_cons {α : Type u} (hd: α) (tl : List α) (p: α → Prop) :
   allP (hd :: tl) p ↔ p hd ∧ allP tl p
   := by simp [allP, foldr]
 
-def pairwise_rel
-  {α : Type u} (rel : α → α → Prop) (l: List α) : Prop
-  := match l with
-  | [] => True
-  | hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl
-
 @[simp]
 theorem pairwise_rel_nil {α : Type u} (rel : α → α → Prop) :
   pairwise_rel rel []
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 91823cb6..6b7b0792 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -1,3 +1,4 @@
 import Base.Primitives.Base
 import Base.Primitives.Scalar
+import Base.Primitives.Array
 import Base.Primitives.Vec
diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean
new file mode 100644
index 00000000..d19e9144
--- /dev/null
+++ b/backends/lean/Base/Primitives/Array.lean
@@ -0,0 +1,398 @@
+/- Arrays/slices -/
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
+import Mathlib.Tactic.Linarith
+import Base.IList
+import Base.Primitives.Scalar
+import Base.Primitives.Range
+import Base.Arith
+import Base.Progress.Base
+
+namespace Primitives
+
+open Result Error
+
+abbrev Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val }
+
+instance (a : Type u) (n : Usize) : Arith.HasIntProp (Array a n) where
+  prop_ty := λ v => v.val.len = n.val
+  prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
+
+instance {α : Type u} {n : Usize} (p : Array α n → Prop) : Arith.HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
+@[simp]
+abbrev Array.length {α : Type u} {n : Usize} (v : Array α n) : Int := v.val.len
+
+@[simp]
+abbrev Array.v {α : Type u} {n : Usize} (v : Array α n) : List α := v.val
+
+example {α: Type u} {n : Usize} (v : Array α n) : v.length ≤ Scalar.max ScalarTy.Usize := by
+  scalar_tac
+
+def Array.mk (α : Type u) (n : Usize) (init : List α) (hl : init.len = n.val := by decide) :
+  Array α n := ⟨ init, by simp [← List.len_eq_length]; apply hl ⟩
+
+example : Array Int (Usize.ofInt 2) := Array.mk Int (Usize.ofInt 2) [0, 1]
+
+-- Remark: not used yet, but could be used if explicit calls to Len are used in Rust
+-- TODO: very annoying that the α and the n are explicit parameters
+def Array.len (α : Type u) (n : Usize) (v : Array α n) : Usize :=
+  Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac)
+
+@[simp]
+theorem Array.len_val {α : Type u} {n : Usize} (v : Array α n) : (Array.len α n v).val = v.length :=
+  by rfl
+
+@[simp]
+abbrev Array.index {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Int) : α :=
+  v.val.index i
+
+@[simp]
+abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i j : Int) : List α :=
+  v.val.slice i j
+
+def Array.index_shared (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
+
+/- In the theorems below: we don't always need the `∃ ..`, but we use one
+   so that `progress` introduces an opaque variable and an equality. This
+   helps control the context.
+ -/
+
+@[pspec]
+theorem Array.index_shared_spec {α : Type u} {n : Usize}[Inhabited α] (v: Array α n) (i: Usize)
+  (hbound : i.val < v.length) :
+  ∃ x, v.index_shared α n i = ret x ∧ x = v.val.index i.val := by
+  simp only [index_shared]
+  -- TODO: dependent rewrite
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
+  simp [*]
+
+-- This shouldn't be used
+def Array.index_shared_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (_: α) : Result Unit :=
+  if i.val < List.length v.val then
+    .ret ()
+  else
+    .fail arrayOutOfBounds
+
+def Array.index_mut (α : Type u) (v: Array α n) (i: Usize) : Result α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
+
+@[pspec]
+theorem Array.index_mut_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
+  (hbound : i.val < v.length) :
+  ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by
+  simp only [index_mut]
+  -- TODO: dependent rewrite
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
+  simp [*]
+
+def Array.index_mut_back (α : Type u) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some _ =>
+    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+
+@[pspec]
+theorem Array.index_mut_back_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
+  (hbound : i.val < v.length) :
+  ∃ nv, v.index_mut_back α i x = ret nv ∧
+  nv.val = v.val.update i.val x
+  := by
+  simp only [index_mut_back]
+  have h := List.indexOpt_bounds v.val i.val
+  split
+  . simp_all [length]; cases h <;> scalar_tac
+  . simp_all
+
+def Slice (α : Type u) := { l : List α // l.length ≤ Usize.max }
+
+instance (a : Type u) : Arith.HasIntProp (Slice a) where
+  prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
+  prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
+
+instance {α : Type u} (p : Slice α → Prop) : Arith.HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
+@[simp]
+abbrev Slice.length {α : Type u} (v : Slice α) : Int := v.val.len
+
+@[simp]
+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 ⟩
+
+-- TODO: very annoying that the α is an explicit parameter
+def Slice.len (α : Type u) (v : Slice α) : Usize :=
+  Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac)
+
+@[simp]
+theorem Slice.len_val {α : Type u} (v : Slice α) : (Slice.len α v).val = v.length :=
+  by rfl
+
+@[simp]
+abbrev Slice.index {α : Type u} [Inhabited α] (v: Slice α) (i: Int) : α :=
+  v.val.index i
+
+@[simp]
+abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : List α :=
+  s.val.slice i j
+
+def Slice.index_shared (α : Type u) (v: Slice α) (i: Usize) : Result α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
+
+/- In the theorems below: we don't always need the `∃ ..`, but we use one
+   so that `progress` introduces an opaque variable and an equality. This
+   helps control the context.
+ -/
+
+@[pspec]
+theorem Slice.index_shared_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
+  (hbound : i.val < v.length) :
+  ∃ x, v.index_shared α i = ret x ∧ x = v.val.index i.val := by
+  simp only [index_shared]
+  -- TODO: dependent rewrite
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
+  simp [*]
+
+-- This shouldn't be used
+def Slice.index_shared_back (α : Type u) (v: Slice α) (i: Usize) (_: α) : Result Unit :=
+  if i.val < List.length v.val then
+    .ret ()
+  else
+    .fail arrayOutOfBounds
+
+def Slice.index_mut (α : Type u) (v: Slice α) (i: Usize) : Result α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
+
+@[pspec]
+theorem Slice.index_mut_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
+  (hbound : i.val < v.length) :
+  ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by
+  simp only [index_mut]
+  -- TODO: dependent rewrite
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
+  simp [*]
+
+def Slice.index_mut_back (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (Slice α) :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some _ =>
+    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+
+@[pspec]
+theorem Slice.index_mut_back_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
+  (hbound : i.val < v.length) :
+  ∃ nv, v.index_mut_back α i x = ret nv ∧
+  nv.val = v.val.update i.val x
+  := by
+  simp only [index_mut_back]
+  have h := List.indexOpt_bounds v.val i.val
+  split
+  . simp_all [length]; cases h <;> scalar_tac
+  . simp_all
+
+/- Array to slice/subslices -/
+def Array.to_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
+  ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
+
+@[pspec]
+theorem Array.to_slice_spec {α : Type u} {n : Usize} (v : Array α n) :
+  ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice]
+
+def Array.to_mut_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
+  to_slice α n v
+
+@[pspec]
+theorem Array.to_mut_slice_spec {α : Type u} {n : Usize} (v : Array α n) :
+  ∃ s, Array.to_slice α n v = ret s ∧ v.val = s.val := to_slice_spec v
+
+def Array.to_mut_slice_back (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
+  if h: s.val.len = n.val then
+    ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
+  else fail panic
+
+@[pspec]
+theorem Array.to_mut_slice_back_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
+  ∃ na, to_mut_slice_back α n a ns = ret na ∧ na.val = ns.val
+  := by simp [to_mut_slice_back, *]
+
+def Array.shared_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
+  -- TODO: not completely sure here
+  if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then
+    ret ⟨ a.val.slice r.start.val r.end_.val,
+          by
+            simp [← List.len_eq_length]
+            have := a.val.slice_len_le r.start.val r.end_.val
+            scalar_tac ⟩
+  else
+    fail panic
+
+@[pspec]
+theorem Array.shared_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
+  (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
+  ∃ s, shared_subslice α n a r = ret s ∧
+  s.val = a.val.slice r.start.val r.end_.val ∧
+  (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
+  := by
+  simp [shared_subslice, *]
+  intro i _ _
+  have := List.index_slice r.start.val r.end_.val i a.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
+  simp [*]
+
+def Array.mut_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
+  Array.shared_subslice α n a r
+
+@[pspec]
+theorem Array.mut_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
+  (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
+  ∃ s, mut_subslice α n a r = ret s ∧
+  s.val = a.slice r.start.val r.end_.val ∧
+  (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
+  := shared_subslice_spec a r h0 h1
+
+def Array.mut_subslice_back (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) :=
+  -- TODO: not completely sure here
+  if h: r.start.val < r.end_.val ∧ r.end_.val ≤ a.length ∧ s.val.len = r.end_.val - r.start.val then
+    let s_beg := a.val.itake r.start.val
+    let s_end := a.val.idrop r.end_.val
+    have : s_beg.len = r.start.val := by
+      apply List.itake_len
+      . simp_all; scalar_tac
+      . scalar_tac
+    have : s_end.len = a.val.len - r.end_.val := by
+      apply List.idrop_len
+      . scalar_tac
+      . scalar_tac
+    let na := s_beg.append (s.val.append s_end)
+    have : na.len = a.val.len := by simp [*]
+    ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+  else
+    fail panic
+
+-- TODO: it is annoying to write `.val` everywhere. We could leverage coercions,
+-- but: some symbols like `+` are already overloaded to be notations for monadic
+-- operations/
+-- We should introduce special symbols for the monadic arithmetic operations
+-- (the use will never write those symbols directly).
+@[pspec]
+theorem Array.mut_subslice_back_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
+  (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) :
+  ∃ na, mut_subslice_back α n a r s = ret na ∧
+  (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧
+  (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = s.index (i - r.start.val)) ∧
+  (∀ i, r.end_.val ≤ i → i < n.val → na.index i = a.index i) := by
+  simp [mut_subslice_back, *]
+  have h := List.replace_slice_index r.start.val r.end_.val a.val s.val
+    (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac)
+  simp [List.replace_slice] at h
+  have ⟨ h0, h1, h2 ⟩ := h
+  clear h
+  split_conjs
+  . intro i _ _
+    have := h0 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    have := h1 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    have := h2 i (by int_tac) (by int_tac)
+    simp [*]
+
+def Slice.shared_subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
+  -- TODO: not completely sure here
+  if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then
+    ret ⟨ s.val.slice r.start.val r.end_.val,
+          by
+            simp [← List.len_eq_length]
+            have := s.val.slice_len_le r.start.val r.end_.val
+            scalar_tac ⟩
+  else
+    fail panic
+
+@[pspec]
+theorem Slice.shared_subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
+  (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
+  ∃ ns, shared_subslice α s r = ret ns ∧
+  ns.val = s.slice r.start.val r.end_.val ∧
+  (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i))
+  := by
+  simp [shared_subslice, *]
+  intro i _ _
+  have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
+  simp [*]
+
+def Slice.mut_subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
+  Slice.shared_subslice α s r
+
+@[pspec]
+theorem Slice.mut_subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
+  (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
+  ∃ ns, mut_subslice α s r = ret ns ∧
+  ns.val = s.slice r.start.val r.end_.val ∧
+  (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i))
+  := shared_subslice_spec s r h0 h1
+
+attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing
+set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse)
+
+def Slice.mut_subslice_back (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) :=
+  -- TODO: not completely sure here
+  if h: r.start.val < r.end_.val ∧ r.end_.val ≤ s.length ∧ ss.val.len = r.end_.val - r.start.val then
+    let s_beg := s.val.itake r.start.val
+    let s_end := s.val.idrop r.end_.val
+    have : s_beg.len = r.start.val := by
+      apply List.itake_len
+      . simp_all; scalar_tac
+      . scalar_tac
+    have : s_end.len = s.val.len - r.end_.val := by
+      apply List.idrop_len
+      . scalar_tac
+      . scalar_tac
+    let ns := s_beg.append (ss.val.append s_end)
+    have : ns.len = s.val.len := by simp [*]
+    ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+  else
+    fail panic
+
+@[pspec]
+theorem Slice.mut_subslice_back_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α)
+  (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) :
+  ∃ na, mut_subslice_back α a r ss = ret na ∧
+  (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧
+  (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = ss.index (i - r.start.val)) ∧
+  (∀ i, r.end_.val ≤ i → i < a.length → na.index i = a.index i) := by
+  simp [mut_subslice_back, *]
+  have h := List.replace_slice_index r.start.val r.end_.val a.val ss.val
+    (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac)
+  simp [List.replace_slice, *] at h
+  have ⟨ h0, h1, h2 ⟩ := h
+  clear h
+  split_conjs
+  . intro i _ _
+    have := h0 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    have := h1 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    have := h2 i (by int_tac) (by int_tac)
+    simp [*]
+
+end Primitives
diff --git a/backends/lean/Base/Primitives/Range.lean b/backends/lean/Base/Primitives/Range.lean
new file mode 100644
index 00000000..26cbee42
--- /dev/null
+++ b/backends/lean/Base/Primitives/Range.lean
@@ -0,0 +1,19 @@
+/- Arrays/slices -/
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
+import Mathlib.Tactic.Linarith
+import Base.IList
+import Base.Primitives.Scalar
+import Base.Arith
+import Base.Progress.Base
+
+namespace Primitives
+
+structure Range (α : Type u) where
+  mk ::
+  start: α
+  end_: α
+
+end Primitives
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 2e5be8bf..ffc969f3 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -787,15 +787,8 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
     | isTrue h  => isTrue (Scalar.eq_of_val_eq h)
     | isFalse h => isFalse (Scalar.ne_of_val_ne h)
 
-/- Remark: we can't write the following instance because of restrictions about
-   the type class parameters (`ty` doesn't appear in the return type, which is
-   forbidden):
-
-   ```
-   instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val
-   ```
- -/
-def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val
+instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where
+  coe := λ v => v.val
 
 -- -- We now define a type class that subsumes the various machine integer types, so
 -- -- as to write a concise definition for scalar_cast, rather than exhaustively
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index a09d6ac2..d37fb5fd 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -1,3 +1,4 @@
+/- Vectors -/
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
@@ -5,6 +6,7 @@ import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
+import Base.Primitives.Array
 import Base.Arith
 import Base.Progress.Base
 
@@ -12,19 +14,16 @@ namespace Primitives
 
 open Result Error
 
--------------
--- VECTORS --
--------------
-
 def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max }
 
--- TODO: do we really need it? It should be with Subtype by default
-instance Vec.cast (a : Type u): Coe (Vec a) (List a)  where coe := λ v => v.val
-
 instance (a : Type u) : Arith.HasIntProp (Vec a) where
   prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
   prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
 
+instance {α : Type u} (p : Vec α → Prop) : Arith.HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
 @[simp]
 abbrev Vec.length {α : Type u} (v : Vec α) : Int := v.val.len
 
@@ -120,10 +119,6 @@ theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
   simp [*]
 
-instance {α : Type u} (p : Vec α → Prop) : Arith.HasIntProp (Subtype p) where
-  prop_ty := λ x => p x
-  prop := λ x => x.property
-
 def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
-- 
cgit v1.2.3