summaryrefslogtreecommitdiff
path: root/backends/lean/Base/IList
diff options
context:
space:
mode:
authorSon Ho2023-07-25 19:06:05 +0200
committerSon Ho2023-07-25 19:06:05 +0200
commit0cc3c78137434d848188eee2a66b1e2cacfd102e (patch)
tree43c9cee6a846f634ecd9f144c3c3f51934c7f81e /backends/lean/Base/IList
parent1854c631a6a7a3f8d45ad18e05547f9d3782c3ee (diff)
Make progress on the proofs of the hashmap
Diffstat (limited to 'backends/lean/Base/IList')
-rw-r--r--backends/lean/Base/IList/IList.lean41
1 files changed, 41 insertions, 0 deletions
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