3 files changed, 168 insertions, 25 deletions
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index a940da25..79de93d5 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -112,7 +112,19 @@ def pairwise_rel
 
 section Lemmas
 
-variable {α : Type u} 
+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
+decreasing_by
+  simp_wf
+  -- TODO: simplify this kind of proofs
+  simp at *
+  have : 0 ≤ i := by linarith
+  have : 1 ≤ i := by linarith
+  simp [Int.toNat_sub_of_le, *]
 
 @[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update]
 @[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update]
@@ -129,6 +141,10 @@ variable {α : Type u}
 @[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 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
+
 @[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
@@ -144,6 +160,45 @@ theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : s
         conv at this => lhs; simp [slice, *]
         simp [*, slice]
 
+@[simp]
+theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) :
+  ireplicate l x = replicate l.toNat x :=
+  if hz: l = 0 then by
+    simp [*]
+  else by
+    have : 0 < l := by int_tac
+    have hr := ireplicate_replicate (l - 1) x (by int_tac)
+    simp [*]
+    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
+decreasing_by
+  simp_wf
+  -- TODO: simplify this kind of proofs
+  simp at *
+  have : 0 ≤ l := by linarith
+  have : 1 ≤ l := by linarith
+  simp [Int.toNat_sub_of_le, *]  
+
+@[simp]
+theorem ireplicate_len {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) :
+  (ireplicate l x).len = l :=
+  if hz: l = 0 then by
+    simp [*]
+  else by
+    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
+decreasing_by
+  simp_wf
+  -- TODO: simplify this kind of proofs
+  simp at *
+  have : 0 ≤ l := by linarith
+  have : 1 ≤ l := by linarith
+  simp [Int.toNat_sub_of_le, *]
+
 theorem len_eq_length (ls : List α) : ls.len = ls.length := by
   induction ls
   . rfl
diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean
index 6c95fd78..49c84bee 100644
--- a/backends/lean/Base/Primitives/Array.lean
+++ b/backends/lean/Base/Primitives/Array.lean
@@ -51,6 +51,15 @@ def Array.index_shared (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Re
   | none => fail .arrayOutOfBounds
   | some x => ret x
 
+-- For initialization
+def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n :=
+  ⟨ List.ireplicate n.val x, by have h := n.hmin; simp_all [Scalar.min] ⟩
+
+@[pspec]
+theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) :
+  ∃ a, Array.repeat α n x = a ∧ a.val = List.ireplicate n.val x := by
+  simp [Array.repeat]
+
 /- 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.
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 55227a9f..ec9665a5 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -230,6 +230,20 @@ def Scalar.cMax (ty : ScalarTy) : Int :=
   | .Usize => Scalar.max .U32
   | _ => Scalar.max ty
 
+theorem Scalar.min_lt_max (ty : ScalarTy) : Scalar.min ty < Scalar.max ty := by
+  cases ty <;> simp [Scalar.min, Scalar.max]
+  . simp [Isize.min, Isize.max]
+    have h1 := Isize.refined_min.property
+    have h2 := Isize.refined_max.property
+    cases h1 <;> cases h2 <;> simp [*]
+  . simp [Usize.max]
+    have h := Usize.refined_max.property
+    cases h <;> simp [*]
+
+theorem Scalar.min_le_max (ty : ScalarTy) : Scalar.min ty ≤ Scalar.max ty := by
+  have := Scalar.min_lt_max ty
+  int_tac
+
 theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by
   cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at *
   have h := Isize.refined_min.property
@@ -395,6 +409,34 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re
 @[reducible] def U64   := Scalar .U64
 @[reducible] def U128  := Scalar .U128
 
+-- TODO: reducible?
+@[reducible] def core_isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
+@[reducible] def core_isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
+@[reducible] def core_i8_min : I8 := Scalar.ofInt I8.min
+@[reducible] def core_i8_max : I8 := Scalar.ofInt I8.max
+@[reducible] def core_i16_min : I16 := Scalar.ofInt I16.min
+@[reducible] def core_i16_max : I16 := Scalar.ofInt I16.max
+@[reducible] def core_i32_min : I32 := Scalar.ofInt I32.min
+@[reducible] def core_i32_max : I32 := Scalar.ofInt I32.max
+@[reducible] def core_i64_min : I64 := Scalar.ofInt I64.min
+@[reducible] def core_i64_max : I64 := Scalar.ofInt I64.max
+@[reducible] def core_i128_min : I128 := Scalar.ofInt I128.min
+@[reducible] def core_i128_max : I128 := Scalar.ofInt I128.max
+
+-- TODO: reducible?
+@[reducible] def core_usize_min : Usize := Scalar.ofInt Usize.min
+@[reducible] def core_usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize))
+@[reducible] def core_u8_min : U8 := Scalar.ofInt U8.min
+@[reducible] def core_u8_max : U8 := Scalar.ofInt U8.max
+@[reducible] def core_u16_min : U16 := Scalar.ofInt U16.min
+@[reducible] def core_u16_max : U16 := Scalar.ofInt U16.max
+@[reducible] def core_u32_min : U32 := Scalar.ofInt U32.min
+@[reducible] def core_u32_max : U32 := Scalar.ofInt U32.max
+@[reducible] def core_u64_min : U64 := Scalar.ofInt U64.min
+@[reducible] def core_u64_max : U64 := Scalar.ofInt U64.max
+@[reducible] def core_u128_min : U128 := Scalar.ofInt U128.min
+@[reducible] def core_u128_max : U128 := Scalar.ofInt U128.max
+
 -- TODO: below: not sure this is the best way.
 -- Should we rather overload operations like +, -, etc.?
 -- Also, it is possible to automate the generation of those definitions
@@ -861,33 +903,33 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
 
 -- ofIntCore
 -- TODO: typeclass?
-@[reducible] def Isize.ofIntCore := @Scalar.ofIntCore .Isize
-@[reducible] def I8.ofIntCore    := @Scalar.ofIntCore .I8
-@[reducible] def I16.ofIntCore   := @Scalar.ofIntCore .I16
-@[reducible] def I32.ofIntCore   := @Scalar.ofIntCore .I32
-@[reducible] def I64.ofIntCore   := @Scalar.ofIntCore .I64
-@[reducible] def I128.ofIntCore  := @Scalar.ofIntCore .I128
-@[reducible] def Usize.ofIntCore := @Scalar.ofIntCore .Usize
-@[reducible] def U8.ofIntCore    := @Scalar.ofIntCore .U8
-@[reducible] def U16.ofIntCore   := @Scalar.ofIntCore .U16
-@[reducible] def U32.ofIntCore   := @Scalar.ofIntCore .U32
-@[reducible] def U64.ofIntCore   := @Scalar.ofIntCore .U64
-@[reducible] def U128.ofIntCore  := @Scalar.ofIntCore .U128
+def Isize.ofIntCore := @Scalar.ofIntCore .Isize
+def I8.ofIntCore    := @Scalar.ofIntCore .I8
+def I16.ofIntCore   := @Scalar.ofIntCore .I16
+def I32.ofIntCore   := @Scalar.ofIntCore .I32
+def I64.ofIntCore   := @Scalar.ofIntCore .I64
+def I128.ofIntCore  := @Scalar.ofIntCore .I128
+def Usize.ofIntCore := @Scalar.ofIntCore .Usize
+def U8.ofIntCore    := @Scalar.ofIntCore .U8
+def U16.ofIntCore   := @Scalar.ofIntCore .U16
+def U32.ofIntCore   := @Scalar.ofIntCore .U32
+def U64.ofIntCore   := @Scalar.ofIntCore .U64
+def U128.ofIntCore  := @Scalar.ofIntCore .U128
 
 --  ofInt
 -- TODO: typeclass?
-@[reducible] def Isize.ofInt := @Scalar.ofInt .Isize
-@[reducible] def I8.ofInt    := @Scalar.ofInt .I8
-@[reducible] def I16.ofInt   := @Scalar.ofInt .I16
-@[reducible] def I32.ofInt   := @Scalar.ofInt .I32
-@[reducible] def I64.ofInt   := @Scalar.ofInt .I64
-@[reducible] def I128.ofInt  := @Scalar.ofInt .I128
-@[reducible] def Usize.ofInt := @Scalar.ofInt .Usize
-@[reducible] def U8.ofInt    := @Scalar.ofInt .U8
-@[reducible] def U16.ofInt   := @Scalar.ofInt .U16
-@[reducible] def U32.ofInt   := @Scalar.ofInt .U32
-@[reducible] def U64.ofInt   := @Scalar.ofInt .U64
-@[reducible] def U128.ofInt  := @Scalar.ofInt .U128
+abbrev Isize.ofInt := @Scalar.ofInt .Isize
+abbrev I8.ofInt    := @Scalar.ofInt .I8
+abbrev I16.ofInt   := @Scalar.ofInt .I16
+abbrev I32.ofInt   := @Scalar.ofInt .I32
+abbrev I64.ofInt   := @Scalar.ofInt .I64
+abbrev I128.ofInt  := @Scalar.ofInt .I128
+abbrev Usize.ofInt := @Scalar.ofInt .Usize
+abbrev U8.ofInt    := @Scalar.ofInt .U8
+abbrev U16.ofInt   := @Scalar.ofInt .U16
+abbrev U32.ofInt   := @Scalar.ofInt .U32
+abbrev U64.ofInt   := @Scalar.ofInt .U64
+abbrev U128.ofInt  := @Scalar.ofInt .U128
 
 postfix:max "#isize" => Isize.ofInt
 postfix:max "#i8"    => I8.ofInt
@@ -905,9 +947,46 @@ postfix:max "#u128"  => U128.ofInt
 -- Testing the notations
 example : Result Usize := 0#usize + 1#usize
 
+-- TODO: factor those lemmas out
 @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofInt x h).val = x := by
   simp [Scalar.ofInt, Scalar.ofIntCore]
 
+@[simp] theorem Isize.ofInt_val_eq (h : Scalar.min ScalarTy.Isize ≤ x ∧ x ≤ Scalar.max ScalarTy.Isize) : (Isize.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I8.ofInt_val_eq (h : Scalar.min ScalarTy.I8 ≤ x ∧ x ≤ Scalar.max ScalarTy.I8) : (I8.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I16.ofInt_val_eq (h : Scalar.min ScalarTy.I16 ≤ x ∧ x ≤ Scalar.max ScalarTy.I16) : (I16.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I32.ofInt_val_eq (h : Scalar.min ScalarTy.I32 ≤ x ∧ x ≤ Scalar.max ScalarTy.I32) : (I32.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I64.ofInt_val_eq (h : Scalar.min ScalarTy.I64 ≤ x ∧ x ≤ Scalar.max ScalarTy.I64) : (I64.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I128.ofInt_val_eq (h : Scalar.min ScalarTy.I128 ≤ x ∧ x ≤ Scalar.max ScalarTy.I128) : (I128.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem Usize.ofInt_val_eq (h : Scalar.min ScalarTy.Usize ≤ x ∧ x ≤ Scalar.max ScalarTy.Usize) : (Usize.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U8.ofInt_val_eq (h : Scalar.min ScalarTy.U8 ≤ x ∧ x ≤ Scalar.max ScalarTy.U8) : (U8.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U16.ofInt_val_eq (h : Scalar.min ScalarTy.U16 ≤ x ∧ x ≤ Scalar.max ScalarTy.U16) : (U16.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U32.ofInt_val_eq (h : Scalar.min ScalarTy.U32 ≤ x ∧ x ≤ Scalar.max ScalarTy.U32) : (U32.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U64.ofInt_val_eq (h : Scalar.min ScalarTy.U64 ≤ x ∧ x ≤ Scalar.max ScalarTy.U64) : (U64.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U128.ofInt_val_eq (h : Scalar.min ScalarTy.U128 ≤ x ∧ x ≤ Scalar.max ScalarTy.U128) : (U128.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
 -- Comparisons
 instance {ty} : LT (Scalar ty) where
   lt a b := LT.lt a.val b.val