diff options
Diffstat (limited to 'backends/lean/Base/IList')
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 23 |
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) : |