Add some proofs for the Lean backend (#255)

* Make progress on the proofs of the hashmap

* Make a minor modification to the hashmap

* Make progress on the hashmap

* Make progress on the proofs

* Make progress on the proofs

* Make progress on the proof of the hashmap

* Progress on the proofs of the hashmap

* Update a proof

* Update the Charon pin

* Make minor modifications to the hashmap

* Regenerate the tests

* Regenerate the hashmap

* Add lemmas to the Lean backend

* Make progress on the proofs of the hashmap

* Make a minor fix

* Finish the proof about the hashmap

* Update scalar_tac

* Make a minor modification in the hashmap

* Update the proofs of the hashmap

---------

Co-authored-by: Son Ho <sonho@Sons-MacBook-Pro.local>
Co-authored-by: Son Ho <sonho@Sons-MBP.lan>

1 files changed, 21 insertions, 2 deletions

diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 96843f55..ab71daed 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -43,6 +43,9 @@ def index [Inhabited α] (ls : List α) (i : Int) : α :=
 
 @[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 index_zero_lt_cons [Inhabited α] (hne : 0 < i) : index ((x :: tl) : List α) i = index tl (i - 1) := by
+  have : i ≠ 0 := by scalar_tac
+  simp [*, index]
 
 theorem indexOpt_bounds (ls : List α) (i : Int) :
   ls.indexOpt i = none ↔ i < 0 ∨ ls.len ≤ i :=
@@ -453,16 +456,18 @@ theorem index_update_eq
         simp at *
         apply index_update_eq <;> scalar_tac
 
-theorem update_map_eq {α : Type u} {β : Type v} (ls : List α) (i : Int) (x : α) (f : α → β) :
+@[simp]
+theorem map_update_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
+      have hi := map_update_eq tl (i - 1) x f
       by simp [*]
 
+@[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 :=
@@ -476,6 +481,20 @@ theorem len_flatten_update_eq {α : Type u} (ls : List (List α)) (i : Int) (x :
       simp [*]
       int_tac
 
+theorem len_index_le_len_flatten (ls : List (List α)) :
+  forall (i : Int), (ls.index i).len ≤ ls.flatten.len := by
+  induction ls <;> intro i <;> simp_all
+  . rw [List.index]
+    simp [default]
+  . rename ∀ _, _ => ih
+    if hi: i = 0 then
+      simp_all
+      int_tac
+    else
+      replace ih := ih (i - 1)
+      simp_all
+      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) :