Start proving theorems for primitive definitions

6 files changed, 116 insertions, 50 deletions

diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 0a9ea4c4..4ff1d923 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -3,8 +3,7 @@ import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
 import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
-
-import Base.Primitives
+import Base.Primitives.Base
 
 /- TODO: this is very useful, but is there more? -/
 set_option profiler true
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 2a335cac..ddb10236 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -11,12 +11,27 @@ def len (ls : List α) : Int :=
   | [] => 0
   | _ :: tl => 1 + len tl
 
+@[simp] theorem len_nil : len ([] : List α) = 0 := by simp [len]
+@[simp] theorem len_cons : len ((x :: tl) : List α) = 1 + len tl := by simp [len]
+
+theorem len_pos : 0 ≤ (ls : List α).len := by
+  induction ls <;> simp [*]
+  linarith
+
+instance (a : Type u) : Arith.HasIntProp (List a) where
+  prop_ty := λ ls => 0 ≤ ls.len
+  prop := λ ls => ls.len_pos
+
 -- Remark: if i < 0, then the result is none
 def indexOpt (ls : List α) (i : Int) : Option α :=
   match ls with
   | [] => none
   | hd :: tl => if i = 0 then some hd else indexOpt tl (i - 1)
 
+@[simp] theorem indexOpt_nil : indexOpt ([] : List α) i = none := by simp [indexOpt]
+@[simp] theorem indexOpt_zero_cons : indexOpt ((x :: tl) : List α) 0 = some x := by simp [indexOpt]
+@[simp] theorem indexOpt_nzero_cons (hne : i ≠ 0) : indexOpt ((x :: tl) : List α) i = indexOpt tl (i - 1) := by simp [*, indexOpt]
+
 -- Remark: if i < 0, then the result is the defaul element
 def index [Inhabited α] (ls : List α) (i : Int) : α :=
   match ls with
@@ -24,6 +39,43 @@ def index [Inhabited α] (ls : List α) (i : Int) : α :=
   | x :: tl =>
     if i = 0 then x else index tl (i - 1)
 
+@[simp] theorem index_zero_cons [Inhabited α] : index ((x :: tl) : List α) 0 = x := by simp [index]
+@[simp] theorem index_nzero_cons [Inhabited α] (hne : i ≠ 0) : index ((x :: tl) : List α) i = index tl (i - 1) := by simp [*, index]
+
+theorem indexOpt_bounds (ls : List α) (i : Int) :
+  ls.indexOpt i = none ↔ i < 0 ∨ ls.len ≤ i :=
+  match ls with
+  | [] =>
+    have : ¬ (i < 0) → 0 ≤ i := by intro; linarith -- TODO: simplify (we could boost int_tac)
+    by simp; tauto
+  | _ :: tl =>
+    have := indexOpt_bounds tl (i - 1)
+    if h: i = 0 then
+      by
+        simp [*];
+        -- TODO: int_tac/scalar_tac should also explore the goal!
+        have := tl.len_pos
+        linarith
+    else by
+      simp [*]
+      constructor <;> intros <;>
+      -- TODO: tactic to split all disjunctions
+      rename_i hor <;> cases hor <;>
+      first | left; int_tac | right; int_tac
+
+theorem indexOpt_eq_index [Inhabited α] (ls : List α) (i : Int) :
+  0 ≤ i →
+  i < ls.len →
+  ls.indexOpt i = some (ls.index i) :=
+  match ls with
+  | [] => by simp; intros; linarith
+  | hd :: tl =>
+    if h: i = 0 then
+      by simp [*]
+    else
+      have hi := indexOpt_eq_index tl (i - 1)
+      by simp [*]; intros;  apply hi <;> int_tac
+
 -- Remark: the list is unchanged if the index is not in bounds (in particular
 -- if it is < 0)
 def update (ls : List α) (i : Int) (y : α) : List α :=
@@ -42,12 +94,6 @@ section Lemmas
 
 variable {α : Type u} 
 
-@[simp] theorem len_nil : len ([] : List α) = 0 := by simp [len]
-@[simp] theorem len_cons : len ((x :: tl) : List α) = 1 + len tl := by simp [len]
-
-@[simp] theorem index_zero_cons [Inhabited α] : index ((x :: tl) : List α) 0 = x := by simp [index]
-@[simp] theorem index_nzero_cons [Inhabited α] (hne : i ≠ 0) : index ((x :: tl) : List α) i = index tl (i - 1) := by simp [*, index]
-
 @[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]
 @[simp] theorem update_nzero_cons (hne : i ≠ 0) : update ((x :: tl) : List α) i y = x :: update tl (i - 1) y := by simp [*, update]
@@ -81,14 +127,6 @@ theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.
   simp [len_eq_length]
 
 
-theorem len_pos : 0 ≤ (ls : List α).len := by
-  induction ls <;> simp [*]
-  linarith
-
-instance (a : Type u) : Arith.HasIntProp (List a) where
-  prop_ty := λ ls => 0 ≤ ls.len
-  prop := λ ls => ls.len_pos
-
 theorem left_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.length = l1'.length) :
   l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
   revert l1'
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 241dfa07..3f88caa2 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -2,6 +2,7 @@ import Lean
 import Lean.Meta.Tactic.Simp
 import Mathlib.Tactic.Linarith
 import Base.Primitives.Base
+import Base.Diverge.Base
 
 namespace Primitives
 
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 7851a232..4ecfa28f 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -6,6 +6,7 @@ import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
 import Base.Arith
+import Base.Progress.Base
 
 namespace Primitives
 
@@ -56,58 +57,80 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
     fail maximumSizeExceeded
 
 -- This shouldn't be used
-def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit :=
-  if i.val < List.length v.val then
+def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
+  if i.val < v.length then
     .ret ()
   else
     .fail arrayOutOfBounds
 
 -- This is actually the backward function
-def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) :=
-  if i.val < List.length v.val then
-    -- TODO: maybe we should redefine a list library which uses integers
-    -- (instead of natural numbers)
+def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+  if i.val < v.length then
     .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
   else
     .fail arrayOutOfBounds
 
--- TODO: remove
-def Vec.index_to_fin {α : Type u} {v: Vec α} {i: Usize} (h : i.val < List.length v.val) :
-  Fin (List.length v.val) :=
-  let j := i.val.toNat
-  let h: j < List.length v.val := by
-    have heq := @Int.toNat_lt (List.length v.val) i.val i.hmin
-    apply heq.mpr
-    assumption
-  ⟨j, h⟩
-
-def Vec.index (α : Type u) (v: Vec α) (i: Usize): Result α :=
+@[pspec]
+theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α) :
+  i.val < v.length →
+  ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
+  intro h
+  simp [insert, *]
+
+def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some x => ret x
 
+@[pspec]
+theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
+  i.val < v.length →
+  v.index α i = ret (v.val.index i.val) := by
+  intro
+  simp only [index]
+  -- TODO: dependent rewrite
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp[length] at *; simp [*])
+  simp only [*]
+
 -- This shouldn't be used
-def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit :=
+def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
   if i.val < List.length v.val then
     .ret ()
   else
     .fail arrayOutOfBounds
 
-def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize): Result α :=
-  if h: i.val < List.length v.val then
-    let i := Vec.index_to_fin h
-    .ret (List.get v.val i)
-  else
-    .fail arrayOutOfBounds
+def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
 
-def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) :=
-  if h: i.val < List.length v.val then
-    let i := Vec.index_to_fin h
-    .ret ⟨ List.set v.val i x, by
-      have h: List.length v.val ≤ Usize.max := v.property
-      simp [*] at *
-    ⟩
-  else
-    .fail arrayOutOfBounds
+@[pspec]
+theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
+  i.val < v.length →
+  v.index_mut α i = ret (v.val.index i.val) := by
+  intro
+  simp only [index_mut]
+  -- TODO: dependent rewrite
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp[length] at *; simp [*])
+  simp only [*]
+
+def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+  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 Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α) :
+  i.val < v.length →
+  ∃ nv, v.index_mut_back α i x = ret nv ∧
+  nv.val = v.val.update i.val x
+  := by
+  intro
+  simp only [index_mut_back]
+  have h := List.indexOpt_bounds v.val i.val
+  split
+  . simp_all [length]; cases h <;> scalar_tac
+  . simp_all
 
 end Primitives
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index a288d889..00b0a478 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -1,6 +1,7 @@
 import Lean
+import Std.Lean.HashSet
 import Base.Utils
-import Base.Primitives
+import Base.Primitives.Base
 
 namespace Progress
 
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index af7b426a..001967e5 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -7,6 +7,7 @@ namespace Progress
 open Lean Elab Term Meta Tactic
 open Utils
 
+/-
 -- TODO: remove
 namespace Test
   open Primitives
@@ -20,6 +21,7 @@ namespace Test
 
   #eval pspecAttr.find? ``Primitives.Vec.index
 end Test
+-/
 
 inductive TheoremOrLocal where
 | Theorem (thName : Name)
@@ -200,6 +202,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
 
+/-
 -- TODO: remove
 namespace Test
   open Primitives
@@ -215,5 +218,6 @@ namespace Test
   set_option trace.Progress false
 
 end Test
+-/
 
 end Progress