chore(library): add auxiliary lemmas for hoare state monad experiment

library/data/buffer.lean

@@ -44,6 +44,12 @@ def read' [inhabited α] : buffer α → nat → α
 def write' : buffer α → nat → α → buffer α
 | ⟨n, a⟩ i v := ⟨n, a.write' i v⟩
 
+lemma read_eq_read' [inhabited α] (b : buffer α) (i : nat) (h : i < b.size) : read b ⟨i, h⟩ = read' b i :=
+by cases b; unfold read read'; simp [array.read_eq_read']
+
+lemma write_eq_write' (b : buffer α) (i : nat) (h : i < b.size) (v : α) : write b ⟨i, h⟩ v = write' b i v :=
+by cases b; unfold write write'; simp [array.write_eq_write']
+
 def to_list (b : buffer α) : list α :=
 b.to_array.to_list
 

library/init/data/array.lean

@@ -22,12 +22,18 @@ a.data i
 def read' [inhabited α] (a : array α n) (i : nat) : α :=
 if h : i < n then a.read ⟨i,h⟩ else default α
 
+lemma read_eq_read' [inhabited α] (a : array α n) (i : nat) (h : i < n) : read a ⟨i, h⟩ = read' a i :=
+by unfold read'; rw [dif_pos h]
+
 def write (a : array α n) (i : fin n) (v : α) : array α n :=
 {data := λ j, if i = j then v else a.read j}
 
 def write' (a : array α n) (i : nat) (v : α) : array α n :=
 if h : i < n then a.write ⟨i, h⟩ v else a
 
+lemma write_eq_write' (a : array α n) (i : nat) (h : i < n) (v : α) : write a ⟨i, h⟩ v = write' a i v :=
+by unfold write'; rw [dif_pos h]
+
 lemma push_back_idx {j n} : j < n + 1 → j ≠ n → j < n :=
 λ h₁ h₂, nat.lt_of_le_and_ne (nat.le_of_lt_succ h₁) h₂