From 3e8060b5501ec83940a4309389a68898df26ebd0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jul 2023 23:37:31 +0200
Subject: Reorganize the Lean backend

---
 backends/lean/Base/IList/IList.lean | 142 ++++++++++++++++++++++++++++++++++++
 1 file changed, 142 insertions(+)
 create mode 100644 backends/lean/Base/IList/IList.lean

(limited to 'backends/lean/Base/IList/IList.lean')

diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
new file mode 100644
index 00000000..2a335cac
--- /dev/null
+++ b/backends/lean/Base/IList/IList.lean
@@ -0,0 +1,142 @@
+/- Complementary list functions and lemmas which operate on integers rather
+   than natural numbers. -/
+
+import Std.Data.Int.Lemmas
+import Base.Arith
+
+namespace List
+
+def len (ls : List α) : Int :=
+  match ls with
+  | [] => 0
+  | _ :: tl => 1 + len tl
+
+-- 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)
+
+-- Remark: if i < 0, then the result is the defaul element
+def index [Inhabited α] (ls : List α) (i : Int) : α :=
+  match ls with
+  | [] => Inhabited.default
+  | x :: tl =>
+    if i = 0 then x else index tl (i - 1)
+
+-- 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 α :=
+  match ls with
+  | [] => []
+  | x :: tl => if i = 0 then y :: tl else x :: update tl (i - 1) y
+
+-- Remark: the whole list is dropped if the index is not in bounds (in particular
+-- if it is < 0)
+def idrop (i : Int) (ls : List α) : List α :=
+  match ls with
+  | [] => []
+  | x :: tl => if i = 0 then x :: tl else idrop (i - 1) tl
+
+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]
+
+@[simp] theorem idrop_nil : idrop i ([] : List α) = [] := by simp [idrop]
+@[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]
+
+theorem len_eq_length (ls : List α) : ls.len = ls.length := by
+  induction ls
+  . rfl
+  . simp [*, Int.ofNat_succ, Int.add_comm]
+
+@[simp] theorem len_append (l1 l2 : List α) : (l1 ++ l2).len = l1.len + l2.len := by
+  -- Remark: simp loops here because of the following rewritings:
+  -- @Nat.cast_add: ↑(List.length l1 + List.length l2) ==> ↑(List.length l1) + ↑(List.length l2)
+  -- Int.ofNat_add_ofNat: ↑(List.length l1) + ↑(List.length l2) ==> ↑(List.length l1 + List.length l2)
+  -- TODO: post an issue?
+  simp only [len_eq_length]
+  simp only [length_append]
+  simp only [Int.ofNat_add]
+
+@[simp]
+theorem length_update (ls : List α) (i : Int) (x : α) : (ls.update i x).length = ls.length := by
+  revert i
+  induction ls <;> simp_all [length, update]
+  intro; split <;> simp [*]
+
+@[simp]
+theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.len := by
+  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'
+  induction l1
+  . intro l1'; cases l1' <;> simp [*]
+  . intro l1'; cases l1' <;> simp_all; tauto
+
+theorem right_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.length = l2'.length) :
+  l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
+  have := left_length_eq_append_eq l1 l2 l1' l2'
+  constructor <;> intro heq2 <;>
+  have : l1.length + l2.length = l1'.length + l2'.length := by
+    have : (l1 ++ l2).length = (l1' ++ l2').length := by simp [*]
+    simp only [length_append] at this
+    apply this
+  . simp [heq] at this
+    tauto
+  . tauto
+
+theorem left_len_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.len = l1'.len) :
+  l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
+  simp [len_eq_length] at heq
+  apply left_length_eq_append_eq
+  assumption
+
+theorem right_len_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.len = l2'.len) :
+  l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
+  simp [len_eq_length] at heq
+  apply right_length_eq_append_eq
+  assumption
+
+open Arith in
+theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by
+  revert i
+  induction ls <;> simp [*]
+  rename_i hd tl hi
+  intro i hineq
+  if heq: i = 0 then
+    simp [*] at *
+    have := tl.len_pos
+    linarith
+  else
+    simp at hineq
+    have : 0 < i := by int_tac
+    simp [*]
+    apply hi
+    linarith
+
+end Lemmas
+
+end List
-- 
cgit v1.2.3


From 2fa3cb8ee04dd7ff4184e3e1000fdc025abc50a4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jul 2023 23:37:48 +0200
Subject: Start proving theorems for primitive definitions

---
 backends/lean/Base/IList/IList.lean | 66 +++++++++++++++++++++++++++++--------
 1 file changed, 52 insertions(+), 14 deletions(-)

(limited to 'backends/lean/Base/IList/IList.lean')

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'
-- 
cgit v1.2.3


From 6ef1d360b89fd9f9383e63609888bf925a6a16ab Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 12:08:09 +0200
Subject: Improve progress further and move some lemmas

---
 backends/lean/Base/IList/IList.lean | 67 +++++++++++++++++++++++++++++++++++++
 1 file changed, 67 insertions(+)

(limited to 'backends/lean/Base/IList/IList.lean')

diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index ddb10236..1773e593 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -175,6 +175,73 @@ theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by
     apply hi
     linarith
 
+@[simp]
+theorem index_ne
+  {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (j: ℤ) (x: α) :
+   0 ≤ i → i < l.len → 0 ≤ j → j < l.len → j ≠ i →
+    (l.update i x).index j = l.index j
+  :=
+  λ _ _ _ _ _ => match l with
+  | [] => by simp at *
+  | hd :: tl =>
+    if h: i = 0 then
+      have : j ≠ 0 := by scalar_tac
+      by simp [*]
+    else if h : j = 0 then
+      have : i ≠ 0 := by scalar_tac
+      by simp [*]
+    else
+      by
+        simp [*]
+        simp at *
+        apply index_ne <;> scalar_tac
+
+@[simp]
+theorem index_eq
+  {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (x: α) :
+   0 ≤ i → i < l.len →
+    (l.update i x).index i = x
+  :=
+  fun _ _ => match l with
+  | [] => by simp at *; exfalso; scalar_tac -- TODO: exfalso needed. Son FIXME
+  | hd :: tl =>
+    if h: i = 0 then
+      by
+        simp [*]
+    else
+      by
+        simp [*]
+        simp at *
+        apply index_eq <;> scalar_tac
+
+def allP {α : Type u} (l : List α) (p: α → Prop) : Prop :=
+  foldr (fun a r => p a ∧ r) True l
+
+@[simp]
+theorem allP_nil {α : Type u} (p: α → Prop) : allP [] p :=
+  by simp [allP, foldr]
+
+@[simp]
+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 []
+  := by simp [pairwise_rel]
+
+@[simp]
+theorem pairwise_rel_cons {α : Type u} (rel : α → α → Prop) (hd: α) (tl: List α) :
+  pairwise_rel rel (hd :: tl) ↔ allP tl (rel hd) ∧ pairwise_rel rel tl
+  := by simp [pairwise_rel]
+
 end Lemmas
 
 end List
-- 
cgit v1.2.3


From 876137dff361620d8ade1a4ee94fa9274df0bdc6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 14:08:44 +0200
Subject: Improve int_tac and scalar_tac

---
 backends/lean/Base/IList/IList.lean | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

(limited to 'backends/lean/Base/IList/IList.lean')

diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 1773e593..2443b1a6 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -46,21 +46,18 @@ 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)
+    have : ¬ (i < 0) → 0 ≤ i := by 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
+        int_tac
     else by
       simp [*]
       constructor <;> intros <;>
-      -- TODO: tactic to split all disjunctions
-      rename_i hor <;> cases hor <;>
+      casesm* _ ∨ _ <;> -- splits all the disjunctions
       first | left; int_tac | right; int_tac
 
 theorem indexOpt_eq_index [Inhabited α] (ls : List α) (i : Int) :
@@ -126,7 +123,6 @@ theorem length_update (ls : List α) (i : Int) (x : α) : (ls.update i x).length
 theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.len := by
   simp [len_eq_length]
 
-
 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'
@@ -203,7 +199,7 @@ theorem index_eq
     (l.update i x).index i = x
   :=
   fun _ _ => match l with
-  | [] => by simp at *; exfalso; scalar_tac -- TODO: exfalso needed. Son FIXME
+  | [] => by simp at *; scalar_tac
   | hd :: tl =>
     if h: i = 0 then
       by
-- 
cgit v1.2.3


From 0cc3c78137434d848188eee2a66b1e2cacfd102e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 19:06:05 +0200
Subject: Make progress on the proofs of the hashmap

---
 backends/lean/Base/IList/IList.lean | 41 +++++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)

(limited to 'backends/lean/Base/IList/IList.lean')

diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 2443b1a6..93047a1b 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -123,6 +123,10 @@ theorem length_update (ls : List α) (i : Int) (x : α) : (ls.update i x).length
 theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.len := by
   simp [len_eq_length]
 
+@[simp]
+theorem len_map (ls : List α) (f : α → β) : (ls.map f).len = ls.len := by
+  simp [len_eq_length]
+
 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'
@@ -210,6 +214,43 @@ theorem index_eq
         simp at *
         apply index_eq <;> scalar_tac
 
+theorem update_map_eq {α : Type u} {β : Type v} (ls : List α) (i : Int) (x : α) (f : α → β) :
+  (ls.update i x).map f = (ls.map f).update i (f x) :=
+  match ls with
+  | [] => by simp
+  | hd :: tl =>
+    if h : i = 0 then by simp [*]
+    else
+      have hi := update_map_eq tl (i - 1) x f
+      by simp [*]
+
+theorem len_flatten_update_eq {α : Type u} (ls : List (List α)) (i : Int) (x : List α)
+  (h0 : 0 ≤ i) (h1 : i < ls.len) :
+  (ls.update i x).flatten.len = ls.flatten.len + x.len - (ls.index i).len :=
+  match ls with
+  | [] => by simp at h1; int_tac
+  | hd :: tl => by
+    simp at h1
+    if h : i = 0 then simp [*]; int_tac
+    else
+      have hi := len_flatten_update_eq tl (i - 1) x (by int_tac) (by int_tac)
+      simp [*]
+      int_tac
+
+@[simp]
+theorem index_map_eq {α : Type u} {β : Type v} [Inhabited α] [Inhabited β] (ls : List α) (i : Int) (f : α → β)
+  (h0 : 0 ≤ i) (h1 : i < ls.len) :
+  (ls.map f).index i = f (ls.index i) :=
+  match ls with
+  | [] => by simp at h1; int_tac
+  | hd :: tl =>
+    if h : i = 0 then by
+      simp [*]
+    else
+      have hi := index_map_eq tl (i - 1) f (by int_tac) (by simp at h1; int_tac)
+      by
+        simp [*]
+
 def allP {α : Type u} (l : List α) (p: α → Prop) : Prop :=
   foldr (fun a r => p a ∧ r) True l
 
-- 
cgit v1.2.3