Start adding support for Arrays/Slices in the Lean library

1 files changed, 229 insertions, 9 deletions

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 []