chore(data/array, data/buffer): Array and buffer cleanup (#277)

data/array/lemmas.lean

@@ -3,86 +3,159 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-import data.list.basic data.buffer category.traversable.equiv data.vector2
+import data.list.basic category.traversable.equiv data.vector2
 
 universes u w
 
 namespace d_array
-variables {n : nat} {α : fin n → Type u} {β : Type w}
+variables {n : ℕ} {α : fin n → Type u}
 
 instance [∀ i, inhabited (α i)] : inhabited (d_array n α) :=
 ⟨⟨λ _, default _⟩⟩
 
 end d_array
 
 namespace array
-variables {n m : nat} {α : Type u} {β : Type w}
 
-instance [inhabited α] : inhabited (array n α) := d_array.inhabited
+instance {n α} [inhabited α] : inhabited (array n α) :=
+d_array.inhabited
 
-theorem rev_list_foldr_aux (a : array n α) (b : β) (f : α → β → β) :
-  Π (i : nat) (h : i ≤ n), (d_array.iterate_aux a (λ _ v l, v :: l) i h []).foldr f b = d_array.iterate_aux a (λ _, f) i h b
-| 0     h := rfl
-| (j+1) h := congr_arg (f (read a ⟨j, h⟩)) (rev_list_foldr_aux j _)
+theorem to_list_of_heq {n₁ n₂ α} {a₁ : array n₁ α} {a₂ : array n₂ α}
+  (hn : n₁ = n₂) (ha : a₁ == a₂) : a₁.to_list = a₂.to_list :=
+by congr; assumption
 
-theorem rev_list_foldr (a : array n α) (b : β) (f : α → β → β) : a.rev_list.foldr f b = a.foldl b f :=
-rev_list_foldr_aux a b f _ _
+/- rev_list -/
 
-theorem mem.def (v : α) (a : array n α) :
-  v ∈ a ↔ ∃ i : fin n, read a i = v := iff.rfl
+section rev_list
+variables {n : ℕ} {α : Type u} {a : array n α}
 
-theorem rev_list_reverse_core (a : array n α) : Π i (h : i ≤ n) (t : list α),
-  (a.iterate_aux (λ _ v l, v :: l) i h []).reverse_core t = a.rev_iterate_aux (λ _ v l, v :: l) i h t
+theorem rev_list_reverse_aux : ∀ i (h : i ≤ n) (t : list α),
+  (a.iterate_aux (λ _, (::)) i h []).reverse_core t = a.rev_iterate_aux (λ _, (::)) i h t
 | 0     h t := rfl
-| (i+1) h t := rev_list_reverse_core i _ _
+| (i+1) h t := rev_list_reverse_aux i _ _
+
+@[simp] theorem rev_list_reverse : a.rev_list.reverse = a.to_list :=
+rev_list_reverse_aux _ _ _
+
+@[simp] theorem to_list_reverse : a.to_list.reverse = a.rev_list :=
+by rw [←rev_list_reverse, list.reverse_reverse]
+
+end rev_list
+
+/- mem -/
+
+section mem
+variables {n : ℕ} {α : Type u} {v : α} {a : array n α}
+
+theorem mem.def : v ∈ a ↔ ∃ i, a.read i = v :=
+iff.rfl
+
+theorem mem_rev_list_aux : ∀ {i} (h : i ≤ n),
+  (∃ (j : fin n), j.1 < i ∧ read a j = v) ↔ v ∈ a.iterate_aux (λ _, (::)) i h []
+| 0     _ := ⟨λ ⟨i, n, _⟩, absurd n i.val.not_lt_zero, false.elim⟩
+| (i+1) h := let IH := mem_rev_list_aux (le_of_lt h) in
+  ⟨λ ⟨j, ji1, e⟩, or.elim (lt_or_eq_of_le $ nat.le_of_succ_le_succ ji1)
+    (λ ji, list.mem_cons_of_mem _ $ IH.1 ⟨j, ji, e⟩)
+    (λ je, by simp [d_array.iterate_aux]; apply or.inl; unfold read at e;
+          have H : j = ⟨i, h⟩ := fin.eq_of_veq je; rwa [←H, e]),
+  λ m, begin
+    simp [d_array.iterate_aux, list.mem] at m,
+    cases m with e m',
+    exact ⟨⟨i, h⟩, nat.lt_succ_self _, eq.symm e⟩,
+    exact let ⟨j, ji, e⟩ := IH.2 m' in
+    ⟨j, nat.le_succ_of_le ji, e⟩
+  end⟩
+
+@[simp] theorem mem_rev_list : v ∈ a.rev_list ↔ v ∈ a :=
+iff.symm $ iff.trans
+  (exists_congr $ λ j, iff.symm $
+    show j.1 < n ∧ read a j = v ↔ read a j = v,
+    from and_iff_right j.2)
+  (mem_rev_list_aux _)
+
+@[simp] theorem mem_to_list : v ∈ a.to_list ↔ v ∈ a :=
+by rw ←rev_list_reverse; exact list.mem_reverse.trans mem_rev_list
+
+end mem
+
+/- foldr -/
+
+section foldr
+variables {n : ℕ} {α : Type u} {β : Type w} {b : β} {f : α → β → β} {a : array n α}
+
+theorem rev_list_foldr_aux : ∀ {i} (h : i ≤ n),
+  (d_array.iterate_aux a (λ _, (::)) i h []).foldr f b = d_array.iterate_aux a (λ _, f) i h b
+| 0     h := rfl
+| (j+1) h := congr_arg (f (read a ⟨j, h⟩)) (rev_list_foldr_aux _)
+
+theorem rev_list_foldr : a.rev_list.foldr f b = a.foldl b f :=
+rev_list_foldr_aux _
+
+end foldr
+
+/- foldl -/
+
+section foldl
+variables {n : ℕ} {α : Type u} {β : Type w} {b : β} {f : β → α → β} {a : array n α}
+
+theorem to_list_foldl : a.to_list.foldl f b = a.foldl b (function.swap f) :=
+by rw [←rev_list_reverse, list.foldl_reverse, rev_list_foldr]
+
+end foldl
 
-@[simp] theorem rev_list_reverse (a : array n α) : a.rev_list.reverse = a.to_list :=
-rev_list_reverse_core a _ _ _
+/- length -/
 
-@[simp] theorem to_list_reverse (a : array n α) : a.to_list.reverse = a.rev_list :=
-by rw [← rev_list_reverse, list.reverse_reverse]
+section length
+variables {n : ℕ} {α : Type u}
 
-theorem rev_list_length_aux (a : array n α) (i h) : (a.iterate_aux (λ _ v l, v :: l) i h []).length = i :=
+theorem rev_list_length_aux (a : array n α) (i h) :
+  (a.iterate_aux (λ _, (::)) i h []).length = i :=
 by induction i; simp [*, d_array.iterate_aux]
 
 @[simp] theorem rev_list_length (a : array n α) : a.rev_list.length = n :=
 rev_list_length_aux a _ _
 
 @[simp] theorem to_list_length (a : array n α) : a.to_list.length = n :=
-by rw[← rev_list_reverse, list.length_reverse, rev_list_length]
+by rw[←rev_list_reverse, list.length_reverse, rev_list_length]
 
-theorem to_list_nth_le_core (a : array n α) (i : ℕ) (ih : i < n) : Π (j) {jh t h'},
-  (∀k tl, j + k = i → list.nth_le t k tl = a.read ⟨i, ih⟩) → (a.rev_iterate_aux (λ _ v l, v :: l) j jh t).nth_le i h' = a.read ⟨i, ih⟩
+end length
+
+/- nth -/
+
+section nth
+variables {n : ℕ} {α : Type u} {a : array n α}
+
+theorem to_list_nth_le_aux (i : ℕ) (ih : i < n) : ∀ j {jh t h'},
+  (∀ k tl, j + k = i → list.nth_le t k tl = a.read ⟨i, ih⟩) →
+  (a.rev_iterate_aux (λ _, (::)) j jh t).nth_le i h' = a.read ⟨i, ih⟩
 | 0     _  _ _  al := al i _ $ zero_add _
-| (j+1) jh t h' al := to_list_nth_le_core j $ λk tl hjk,
+| (j+1) jh t h' al := to_list_nth_le_aux j $ λ k tl hjk,
   show list.nth_le (a.read ⟨j, jh⟩ :: t) k tl = a.read ⟨i, ih⟩, from
   match k, hjk, tl with
   | 0,    e, tl := match i, e, ih with ._, rfl, _ := rfl end
   | k'+1, _, tl := by simp[list.nth_le]; exact al _ _ (by simp [*])
   end
 
-theorem to_list_nth_le (a : array n α) (i : ℕ) (h h') : list.nth_le a.to_list i h' = a.read ⟨i, h⟩ :=
-to_list_nth_le_core _ _ _ _ (λk tl, absurd tl $ nat.not_lt_zero _)
+theorem to_list_nth_le (i : ℕ) (h h') : list.nth_le a.to_list i h' = a.read ⟨i, h⟩ :=
+to_list_nth_le_aux _ _ _ (λ k tl, absurd tl k.not_lt_zero)
 
-@[simp] theorem to_list_nth_le' (a : array n α) (i : fin n) (h') : list.nth_le a.to_list i.1 h' = a.read i :=
+@[simp] theorem to_list_nth_le' (a : array n α) (i : fin n) (h') :
+  list.nth_le a.to_list i.1 h' = a.read i :=
 by cases i; apply to_list_nth_le
 
-theorem to_list_nth {a : array n α} {i : ℕ} {v} : list.nth a.to_list i = some v ↔ ∃ h, a.read ⟨i, h⟩ = v :=
+theorem to_list_nth {i v} : list.nth a.to_list i = some v ↔ ∃ h, a.read ⟨i, h⟩ = v :=
 begin
   rw list.nth_eq_some,
   have ll := to_list_length a,
   split; intro h; cases h with h e; subst v,
-  { exact ⟨ll ▸ h, (to_list_nth_le _ _ _ _).symm⟩ },
-  { exact ⟨ll.symm ▸ h, to_list_nth_le _ _ _ _⟩ }
+  { exact ⟨ll ▸ h, (to_list_nth_le _ _ _).symm⟩ },
+  { exact ⟨ll.symm ▸ h, to_list_nth_le _ _ _⟩ }
 end
 
-theorem to_list_foldl (a : array n α) (b : β) (f : β → α → β) : a.to_list.foldl f b = a.foldl b (function.swap f) :=
-by rw [← rev_list_reverse, list.foldl_reverse, rev_list_foldr]
-
-theorem write_to_list {a : array n α} {i v} : (a.write i v).to_list = a.to_list.update_nth i.1 v :=
+theorem write_to_list {i v} : (a.write i v).to_list = a.to_list.update_nth i.1 v :=
 list.ext_le (by simp) $ λ j h₁ h₂, begin
   have h₃ : j < n, {simpa using h₁},
-  rw [to_list_nth_le _ _ h₃],
+  rw [to_list_nth_le _ h₃],
   refine let ⟨_, e⟩ := list.nth_eq_some.1 _ in e.symm,
   by_cases ij : i.1 = j,
   { subst j, rw [show fin.mk i.val h₃ = i, from fin.eq_of_veq rfl,
@@ -93,79 +166,71 @@ list.ext_le (by simp) $ λ j h₁ h₂, begin
     exact fin.ne_of_vne ij }
 end
 
-theorem mem_rev_list_core (a : array n α) (v : α) : Π i (h : i ≤ n),
-  (∃ (j : fin n), j.1 < i ∧ read a j = v) ↔ v ∈ a.iterate_aux (λ _ v l, v :: l) i h []
-| 0     _ := ⟨λ⟨_, n, _⟩, absurd n $ nat.not_lt_zero _, false.elim⟩
-| (i+1) h := let IH := mem_rev_list_core i (le_of_lt h) in
-  ⟨λ⟨j, ji1, e⟩, or.elim (lt_or_eq_of_le $ nat.le_of_succ_le_succ ji1)
-    (λji, list.mem_cons_of_mem _ $ IH.1 ⟨j, ji, e⟩)
-    (λje, by simp [d_array.iterate_aux]; apply or.inl; unfold read at e;
-          have H : j = ⟨i, h⟩ := fin.eq_of_veq je; rwa [← H, e]),
-  λm, begin
-    simp [d_array.iterate_aux, list.mem] at m,
-    cases m with e m',
-    exact ⟨⟨i, h⟩, nat.lt_succ_self _, eq.symm e⟩,
-    exact let ⟨j, ji, e⟩ := IH.2 m' in
-    ⟨j, nat.le_succ_of_le ji, e⟩
-  end⟩
+end nth
 
-@[simp] theorem mem_rev_list (a : array n α) (v : α) : v ∈ a.rev_list ↔ v ∈ a :=
-iff.symm $ iff.trans
-  (exists_congr $ λj, iff.symm $ show j.1 < n ∧ read a j = v ↔ read a j = v, from and_iff_right j.2)
-  (mem_rev_list_core a v _ _)
+/- enum -/
 
-@[simp] theorem mem_to_list (a : array n α) (v : α) : v ∈ a.to_list ↔ v ∈ a :=
-by rw ← rev_list_reverse; simp [-rev_list_reverse]
+section enum
+variables {n : ℕ} {α : Type u} {a : array n α}
 
-theorem mem_to_list_enum (a : array n α) {i v} :
-  (i, v) ∈ a.to_list.enum ↔ ∃ h, a.read ⟨i, h⟩ = v :=
+theorem mem_to_list_enum {i v} : (i, v) ∈ a.to_list.enum ↔ ∃ h, a.read ⟨i, h⟩ = v :=
 by simp [list.mem_iff_nth, to_list_nth, and.comm, and.assoc, and.left_comm]
 
+end enum
+
+/- to_array -/
+
+section to_array
+variables {n : ℕ} {α : Type u}
+
 @[simp] theorem to_list_to_array (a : array n α) : a.to_list.to_array == a :=
 heq_of_heq_of_eq
-  (@@eq.drec_on (λ m (e : a.to_list.length = m), (d_array.mk (λv, a.to_list.nth_le v.1 v.2)) ==
-    (@d_array.mk m (λ_, α) $ λv, a.to_list.nth_le v.1 $ e.symm ▸ v.2)) a.to_list_length heq.rfl) $
-  d_array.ext $ λ⟨i, h⟩, to_list_nth_le _ i h _
+  (@@eq.drec_on (λ m (e : a.to_list.length = m), (d_array.mk (λ v, a.to_list.nth_le v.1 v.2)) ==
+    (@d_array.mk m (λ _, α) $ λ v, a.to_list.nth_le v.1 $ e.symm ▸ v.2)) a.to_list_length heq.rfl) $
+  d_array.ext $ λ ⟨i, h⟩, to_list_nth_le i h _
 
 @[simp] theorem to_array_to_list (l : list α) : l.to_array.to_list = l :=
-list.ext_le (to_list_length _) $ λn h1 h2, to_list_nth_le _ _ _ _
+list.ext_le (to_list_length _) $ λ n h1 h2, to_list_nth_le _ _ _
 
-theorem to_list_of_heq {a₀ : array n α} {a₁ : array m α}
-  (h  : n = m)
-  (h' : a₀ == a₁) :
-  a₀.to_list = a₁.to_list :=
-by congr; assumption
+end to_array
 
-lemma push_back_rev_list_core (a : array n α) (v : α) :
-  ∀ i h h',
-    d_array.iterate_aux (a.push_back v) (λ_, list.cons) i h [] =
-    d_array.iterate_aux a (λ_, list.cons) i h' []
+/- push_back -/
+
+section push_back
+variables {n : ℕ} {α : Type u} {v : α} {a : array n α}
+
+lemma push_back_rev_list_aux : ∀ i h h',
+  d_array.iterate_aux (a.push_back v) (λ _, (::)) i h [] = d_array.iterate_aux a (λ _, (::)) i h' []
 | 0 h h' := rfl
 | (i+1) h h' := begin
   simp [d_array.iterate_aux],
-  refine ⟨_, push_back_rev_list_core _ _ _⟩,
+  refine ⟨_, push_back_rev_list_aux _ _ _⟩,
   dsimp [read, d_array.read, push_back],
   rw [dif_neg], refl,
   exact ne_of_lt h',
 end
 
-@[simp] theorem push_back_rev_list (a : array n α) (v : α) :
-  (a.push_back v).rev_list = v :: a.rev_list :=
+@[simp] theorem push_back_rev_list : (a.push_back v).rev_list = v :: a.rev_list :=
 begin
   unfold push_back rev_list foldl iterate d_array.iterate,
   dsimp [d_array.iterate_aux, read, d_array.read, push_back],
-  rw [dif_pos (eq.refl n)], apply congr_arg,
-  apply push_back_rev_list_core
+  rw [dif_pos (eq.refl n)],
+  apply congr_arg,
+  apply push_back_rev_list_aux
 end
 
-@[simp] theorem push_back_to_list (a : array n α) (v : α) :
-  (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] 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]
+
+end push_back
+
+/- foreach -/
 
-theorem read_foreach_aux (f : fin n → α → α) (ai : array n α) :
-  ∀ i h (a : array n α) (j : fin n), j.1 < i →
-    (d_array.iterate_aux ai (λ i v a', write a' i (f i v)) i h a).read j = f j (ai.read j)
+section foreach
+variables {n : ℕ} {α : Type u} {i : fin n} {f : fin n → α → α} {a : array n α}
+
+theorem read_foreach_aux : ∀ i h (b : array n α) (j : fin n), j.1 < i →
+  (d_array.iterate_aux a (λ i v a', write a' i (f i v)) i h b).read j = f j (a.read j)
 | 0     hi a ⟨j, hj⟩ ji := absurd ji (nat.not_lt_zero _)
 | (i+1) hi a ⟨j, hj⟩ ji := begin
   dsimp [d_array.iterate_aux], dsimp at ji,
@@ -176,26 +241,36 @@ theorem read_foreach_aux (f : fin n → α → α) (ai : array n α) :
       (ne.symm $ mt (@fin.eq_of_veq _ ⟨i, hi⟩ ⟨j, hj⟩) e) }
 end
 
-theorem read_foreach (a : array n α) (f : fin n → α → α) (i : fin n) :
-  (foreach a f).read i = f i (a.read i) :=
-read_foreach_aux _ _ _ _ _ _ i.2
+theorem read_foreach : (foreach a f).read i = f i (a.read i) :=
+read_foreach_aux _ _ _ _ i.2
 
-theorem read_map (f : α → α) (a : array n α) (i : fin n) :
-  (map f a).read i = f (a.read i) :=
-read_foreach _ _ _
+end foreach
 
-theorem read_map₂ (f : α → α → α) (a b : array n α) (i : fin n) :
-  (map₂ f a b).read i = f (a.read i) (b.read i) :=
-read_foreach _ _ _
+/- map -/
 
-end array
+section map
+variables {n : ℕ} {α : Type u} {i : fin n} {f : α → α} {a : array n α}
+
+theorem read_map : (map f a).read i = f (a.read i) :=
+read_foreach
 
-instance (α) [decidable_eq α] : decidable_eq (buffer α) :=
-by tactic.mk_dec_eq_instance
+end map
+
+/- map₂ -/
+
+section map₂
+variables {n : ℕ} {α : Type u} {i : fin n} {f : α → α → α} {a₁ a₂ : array n α}
+
+theorem read_map₂ : (map₂ f a₁ a₂).read i = f (a₁.read i) (a₂.read i) :=
+read_foreach
+
+end map₂
+
+end array
 
 namespace equiv
 
-def d_array_equiv_fin {n : ℕ} (α : fin n → Type*) : d_array n α ≃ (Π i, α i) :=
+def d_array_equiv_fin {n : ℕ} (α : fin n → Type*) : d_array n α ≃ (∀ i, α i) :=
 ⟨d_array.read, d_array.mk, λ ⟨f⟩, rfl, λ f, rfl⟩
 
 def array_equiv_fin (n : ℕ) (α : Type*) : array n α ≃ (fin n → α) :=
@@ -211,13 +286,12 @@ end equiv
 
 namespace array
 open function
-
 variable {n : ℕ}
 
-instance : traversable.{u} (array n) :=
+instance : traversable (array n) :=
 @equiv.traversable (flip vector n) _ (λ α, equiv.vector_equiv_array α n) _
 
-instance : is_lawful_traversable.{u} (array n) :=
+instance : is_lawful_traversable (array n) :=
 @equiv.is_lawful_traversable (flip vector n) _ (λ α, equiv.vector_equiv_array α n) _ _
 
 end array