feat(data/buffer/basic): read and to_buffer lemmas (#6048)

src/data/array/lemmas.lean

@@ -223,6 +223,20 @@ end
 @[simp] theorem push_back_to_list : (a.push_back v).to_list = a.to_list ++ [v] :=
 by rw [←rev_list_reverse, ←rev_list_reverse, push_back_rev_list, list.reverse_cons]
 
+@[simp] lemma read_push_back_left (i : fin n) : (a.push_back v).read i.cast_succ = a.read i :=
+begin
+  cases i with i hi,
+  have : ¬ i = n := ne_of_lt hi,
+  simp [push_back, this, fin.cast_succ, fin.cast_add, fin.cast_le, fin.cast_lt, read, d_array.read]
+end
+
+@[simp] lemma read_push_back_right : (a.push_back v).read (fin.last _) = v :=
+begin
+  cases hn : fin.last n with k hk,
+  have : k = n := by simpa [fin.eq_iff_veq ] using hn.symm,
+  simp [push_back, this, fin.cast_succ, fin.cast_add, fin.cast_le, fin.cast_lt, read, d_array.read]
+end
+
 end push_back
 
 /- foreach -/

src/data/buffer/basic.lean

@@ -42,18 +42,128 @@ lemma append_list_mk_buffer  :
 by ext x : 1; simp [array.to_buffer,to_list,to_list_append_list];
    induction xs; [refl,skip]; simp [to_array]; refl
 
+@[simp] lemma to_buffer_to_list (b : buffer α) : b.to_list.to_buffer = b :=
+begin
+  cases b,
+  rw [to_list, to_array, list.to_buffer, append_list_mk_buffer],
+  congr,
+  { simpa },
+  { apply array.to_list_to_array }
+end
+
+@[simp] lemma to_list_to_buffer (l : list α) : l.to_buffer.to_list = l :=
+begin
+  cases l,
+  { refl },
+  { rw [list.to_buffer, to_list_append_list],
+    refl }
+end
+
+@[simp] lemma append_list_nil (b : buffer α) : b.append_list [] = b := rfl
+
+lemma to_buffer_cons (c : α) (l : list α) :
+  (c :: l).to_buffer = [c].to_buffer.append_list l :=
+begin
+  induction l with hd tl hl,
+  { simp },
+  { apply ext,
+    simp [hl] }
+end
+
+@[simp] lemma size_push_back (b : buffer α) (a : α) : (b.push_back a).size = b.size + 1 :=
+by { cases b, simp [size, push_back] }
+
+@[simp] lemma size_append_list (b : buffer α) (l : list α) :
+  (b.append_list l).size = b.size + l.length :=
+begin
+  induction l with hd tl hl generalizing b,
+  { simp },
+  { simp [append_list, hl, add_comm, add_assoc] }
+end
+
+@[simp] lemma size_to_buffer (l : list α) : l.to_buffer.size = l.length :=
+begin
+  induction l with hd tl hl,
+  { simpa },
+  { rw [to_buffer_cons],
+    have : [hd].to_buffer.size = 1 := rfl,
+    simp [add_comm, this] }
+end
+
+@[simp] lemma length_to_list (b : buffer α) : b.to_list.length = b.size :=
+by rw [←to_buffer_to_list b, to_list_to_buffer, size_to_buffer]
+
+lemma size_singleton (a : α) : [a].to_buffer.size = 1 := rfl
+
+lemma read_push_back_left (b : buffer α) (a : α) {i : ℕ} (h : i < b.size) :
+  (b.push_back a).read ⟨i, by { convert nat.lt_succ_of_lt h, simp }⟩ = b.read ⟨i, h⟩ :=
+by { cases b, convert array.read_push_back_left _, simp }
+
+@[simp] lemma read_push_back_right (b : buffer α) (a : α) :
+  (b.push_back a).read ⟨b.size, by simp⟩ = a :=
+by { cases b, convert array.read_push_back_right }
+
+lemma read_append_list_left' (b : buffer α) (l : list α) {i : ℕ}
+  (h : i < (b.append_list l).size) (h' : i < b.size) :
+  (b.append_list l).read ⟨i, h⟩ = b.read ⟨i, h'⟩ :=
+begin
+  induction l with hd tl hl generalizing b,
+  { refl },
+  { have hb : i < ((b.push_back hd).append_list tl).size := by convert h using 1,
+    have hb' : i < (b.push_back hd).size := by { convert nat.lt_succ_of_lt h', simp },
+    have : (append_list b (hd :: tl)).read ⟨i, h⟩ =
+      read ((push_back b hd).append_list tl) ⟨i, hb⟩ := rfl,
+    simp [this, hl _ hb hb', read_push_back_left _ _ h'] }
+end
+
+lemma read_append_list_left (b : buffer α) (l : list α) {i : ℕ} (h : i < b.size) :
+  (b.append_list l).read ⟨i, by simpa using nat.lt_add_right _ _ _ h⟩ = b.read ⟨i, h⟩ :=
+read_append_list_left' b l _ h
+
+@[simp] lemma read_append_list_right (b : buffer α) (l : list α) {i : ℕ} (h : i < l.length) :
+  (b.append_list l).read ⟨b.size + i, by simp [h]⟩ = l.nth_le i h :=
+begin
+  induction l with hd tl hl generalizing b i,
+  { exact absurd i.zero_le (not_le_of_lt h) },
+  { convert_to ((b.push_back hd).append_list tl).read _ = _,
+    cases i,
+    { convert read_append_list_left _ _ _;
+      simp },
+    { rw [list.length, nat.succ_lt_succ_iff] at h,
+      have : b.size + i.succ = (b.push_back hd).size + i,
+        { simp [add_comm, add_left_comm, nat.succ_eq_add_one] },
+      convert hl (b.push_back hd) h using 1,
+      simpa [nat.add_succ, nat.succ_add] } }
+end
+
+lemma read_to_buffer' (l : list α) {i : ℕ} (h : i < l.to_buffer.size) (h' : i < l.length) :
+  l.to_buffer.read ⟨i, h⟩ = l.nth_le i h' :=
+begin
+  cases l with hd tl,
+  { simpa using h' },
+  { have hi : i < ([hd].to_buffer.append_list tl).size := by simpa [add_comm] using h,
+    convert_to ([hd].to_buffer.append_list tl).read ⟨i, hi⟩ = _,
+    cases i,
+    { convert read_append_list_left _ _ _,
+      simp },
+    { rw list.nth_le,
+      convert read_append_list_right _ _ _,
+      simp [nat.succ_eq_add_one, add_comm] } }
+end
+
+@[simp] lemma read_to_buffer (l : list α) (i) :
+  l.to_buffer.read i = l.nth_le i (by { convert i.property, simp }) :=
+by { convert read_to_buffer' _ _ _, { simp }, { simpa using i.property } }
+
+lemma read_singleton (c : α) : [c].to_buffer.read ⟨0, by simp⟩ = c :=
+by simp
+
 /-- The natural equivalence between lists and buffers, using
 `list.to_buffer` and `buffer.to_list`. -/
 def list_equiv_buffer (α : Type*) : list α ≃ buffer α :=
 begin
   refine { to_fun := list.to_buffer, inv_fun := buffer.to_list, .. };
-  simp [left_inverse,function.right_inverse],
-  { intro x, induction x, refl,
-    simp [list.to_buffer,append_list],
-    rw ← x_ih, refl },
-  { intro x, cases x,
-    simp [to_list,to_array,list.to_buffer],
-    congr, simp, refl, apply array.to_list_to_array }
+  simp [left_inverse,function.right_inverse]
 end
 
 instance : traversable buffer :=