feat: theorems about == on Vector (#6376)

This PR adds theorems about `==` on `Vector`, reproducing those already on `List` and `Array`.
2024-12-13 13:07:12 +11:00 · 2024-12-13 13:07:12 +11:00 · bac34c7767
commit bac34c7767
parent db354d2cde
5 changed files with 222 additions and 85 deletions
--- a/src/Init/Data/Array/Find.lean
+++ b/src/Init/Data/Array/Find.lean
@ -99,7 +99,7 @@ theorem back?_flatten {L : Array (Array α)} :
  simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def]

 theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
-  simp [mkArray_eq_toArray_replicate, List.findSome?_replicate]
+  simp [← List.toArray_replicate, List.findSome?_replicate]

@[simp] theorem findSome?_mkArray_of_pos (h : 0 < n) : findSome? f (mkArray n a) = f a := by
  simp [findSome?_mkArray, Nat.ne_of_gt h]
@ -246,7 +246,7 @@ theorem find?_flatMap_eq_none {xs : Array α} {f : α → Array β} {p : β →

 theorem find?_mkArray :
    find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by
-  simp [mkArray_eq_toArray_replicate, List.find?_replicate]
+  simp [← List.toArray_replicate, List.find?_replicate]

@[simp] theorem find?_mkArray_of_length_pos (h : 0 < n) :
    find? p (mkArray n a) = if p a then some a else none := by
@ -262,15 +262,15 @@ theorem find?_mkArray :
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
 theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α → Bool} :
    (mkArray n a).find? p = none ↔ n = 0 ∨ !p a := by
-  simp [mkArray_eq_toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]
+  simp [← List.toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]

@[simp] theorem find?_mkArray_eq_some {n : Nat} {a b : α} {p : α → Bool} :
    (mkArray n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
-  simp [mkArray_eq_toArray_replicate]
+  simp [← List.toArray_replicate]

@[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α → Bool) (h) :
    ((mkArray n a).find? p).get h = a := by
-  simp [mkArray_eq_toArray_replicate]
+  simp [← List.toArray_replicate]

 theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
    (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@ -25,8 +25,8 @@ namespace Array

 /-! ### toList -/

-theorem toList_inj {a b : Array α} (h : a.toList = b.toList) : a = b := by
-  cases a; cases b; simpa using h
+theorem toList_inj {a b : Array α} : a.toList = b.toList ↔ a = b := by
+  cases a; cases b; simp

@[simp] theorem toList_eq_nil_iff (l : Array α) : l.toList = [] ↔ l = #[] := by
  cases l <;> simp
@ -143,6 +143,34 @@ theorem exists_push_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
    ∃ (ys : Array α) (a : α), xs = ys.push a :=
  exists_push_of_size_pos (by simp [h])

+theorem singleton_inj : #[a] = #[b] ↔ a = b := by
+  simp
+
+/-! ### mkArray -/
+
+@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
+  List.length_replicate ..
+
+@[simp] theorem toList_mkArray : (mkArray n a).toList = List.replicate n a := by
+  simp only [mkArray]
+
+@[simp] theorem mkArray_zero : mkArray 0 a = #[] := rfl
+
+theorem mkArray_succ : mkArray (n + 1) a = (mkArray n a).push a := by
+  apply toList_inj.1
+  simp [List.replicate_succ']
+
+theorem mkArray_inj : mkArray n a = mkArray m b ↔ n = m ∧ (n = 0 ∨ a = b) := by
+  rw [← List.replicate_inj, ← toList_inj]
+  simp
+
+@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
+    (mkArray n v)[i] = v := by simp [← getElem_toList]
+
+theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
+    (mkArray n v)[i]? = if i < n then some v else none := by
+  simp [getElem?_def]
+
 /-! ## L[i] and L[i]? -/

@[simp] theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i := by
@ -894,11 +922,60 @@ theorem mem_or_eq_of_mem_setIfInBounds
  · simp
  · simp [List.set_eq_of_length_le (by simpa using h)]

-/-! Content below this point has not yet been aligned with `List`. -/
+/-! ### BEq -/

-theorem singleton_inj : #[a] = #[b] ↔ a = b := by
+@[simp] theorem push_beq_push [BEq α] {a b : α} {v : Array α} {w : Array α} :
+    (v.push a == w.push b) = (v == w && a == b) := by
+  cases v
+  cases w
  simp

+@[simp] theorem mkArray_beq_mkArray [BEq α] {a b : α} {n : Nat} :
+    (mkArray n a == mkArray n b) = (n == 0 || a == b) := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    rw [mkArray_succ, mkArray_succ, push_beq_push, mkArray_beq_mkArray]
+    rw [Bool.eq_iff_iff]
+    simp +contextual
+
+@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ↔ ReflBEq α := by
+  constructor
+  · intro h
+    constructor
+    intro a
+    suffices (#[a] == #[a]) = true by
+      simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
+    simp
+  · intro h
+    constructor
+    apply Array.isEqv_self_beq
+
+@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (Array α) ↔ LawfulBEq α := by
+  constructor
+  · intro h
+    constructor
+    · intro a b h
+      apply singleton_inj.1
+      apply eq_of_beq
+      simp only [instBEq, isEqv, isEqvAux]
+      simpa
+    · intro a
+      suffices (#[a] == #[a]) = true by
+        simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
+      simp
+  · intro h
+    constructor
+    · intro a b h
+      obtain ⟨hs, hi⟩ := rel_of_isEqv h
+      ext i h₁ h₂
+      · exact hs
+      · simpa using hi _ h₁
+    · intro a
+      apply Array.isEqv_self_beq
+
+/-! Content below this point has not yet been aligned with `List`. -/
+
 theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl

@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
@ -1083,22 +1160,6 @@ theorem ofFn_succ (f : Fin (n+1) → α) :
      simp at h₁ h₂
      omega

-/-! # mkArray -/
-
-@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
-  List.length_replicate ..
-
-@[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
-
-theorem mkArray_eq_toArray_replicate (n : Nat) (v : α) : mkArray n v = (List.replicate n v).toArray := rfl
-
-@[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
-    (mkArray n v)[i] = v := by simp [← getElem_toList]
-
-theorem getElem?_mkArray (n : Nat) (v : α) (i : Nat) :
-    (mkArray n v)[i]? = if i < n then some v else none := by
-  simp [getElem?_def]
-
 /-! # mem -/

@[simp] theorem mem_toList {a : α} {l : Array α} : a ∈ l.toList ↔ a ∈ l := mem_def.symm
@ -1310,43 +1371,6 @@ theorem getElem_range {n : Nat} {x : Nat} (h : x < (Array.range n).size) : (Arra
        true_and, Nat.not_lt] at h
      rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (a.toList.length_reverse ▸ ‹_›)]

-/-! ### BEq -/
-
-@[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ↔ ReflBEq α := by
-  constructor
-  · intro h
-    constructor
-    intro a
-    suffices (#[a] == #[a]) = true by
-      simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
-    simp
-  · intro h
-    constructor
-    apply Array.isEqv_self_beq
-
-@[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (Array α) ↔ LawfulBEq α := by
-  constructor
-  · intro h
-    constructor
-    · intro a b h
-      apply singleton_inj.1
-      apply eq_of_beq
-      simp only [instBEq, isEqv, isEqvAux]
-      simpa
-    · intro a
-      suffices (#[a] == #[a]) = true by
-        simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
-      simp
-  · intro h
-    constructor
-    · intro a b h
-      obtain ⟨hs, hi⟩ := rel_of_isEqv h
-      ext i h₁ h₂
-      · exact hs
-      · simpa using hi _ h₁
-    · intro a
-      apply Array.isEqv_self_beq
-
 /-! ### take -/

@[simp] theorem size_take_loop (a : Array α) (n : Nat) : (take.loop n a).size = a.size - n := by
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@ -154,6 +154,9 @@ theorem ne_nil_iff_exists_cons {l : List α} : l ≠ [] ↔ ∃ b L, l = b :: L
 theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b := by
  simp

+@[simp] theorem concat_ne_nil (a : α) (l : List α) : l ++ [a] ≠ [] := by
+  cases l <;> simp
+
 /-! ## L[i] and L[i]? -/

 /-! ### `get` and `get?`.
@ -717,6 +720,15 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.s
@[simp] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
    (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl

+@[simp] theorem concat_beq_concat [BEq α] {a b : α} {l₁ l₂ : List α} :
+    (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b) := by
+  induction l₁ generalizing l₂ with
+  | nil => cases l₂ <;> simp
+  | cons x l₁ ih =>
+    cases l₂ with
+    | nil => simp
+    | cons y l₂ => simp [ih, Bool.and_assoc]
+
 theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l₁.length = l₂.length :=
  match l₁, l₂ with
  | [], [] => rfl
@ -2074,8 +2086,6 @@ theorem concat_inj_right {l : List α} {a a' : α} : concat l a = concat l a'

@[deprecated concat_inj (since := "2024-09-05")] abbrev concat_eq_concat := @concat_inj

-theorem concat_ne_nil (a : α) (l : List α) : concat l a ≠ [] := by cases l <;> simp
-
 theorem concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l₁ ++ a :: l₂ := by simp

 theorem append_concat (a : α) (l₁ l₂ : List α) : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a := by simp
@ -2328,6 +2338,10 @@ theorem flatMap_eq_foldl (f : α → List β) (l : List α) :

@[simp] theorem replicate_one : replicate 1 a = [a] := rfl

+/-- Variant of `replicate_succ` that concatenates `a` to the end of the list. -/
+theorem replicate_succ' : replicate (n + 1) a = replicate n a ++ [a] := by
+  induction n <;> simp_all [replicate_succ, ← cons_append]
+
@[simp] theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
  | 0 => by simp
  | n+1 => by simp [replicate_succ, mem_replicate, Nat.succ_ne_zero]
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@ -371,4 +371,9 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
  · simp
  · simp_all [List.set_eq_of_length_le]

+@[simp] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = mkArray n v := rfl
+
+@[deprecated toArray_replicate (since := "2024-12-13")]
+abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate
+
 end List
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@ -22,6 +22,7 @@ end Array

 namespace Vector

+
 /-! ### mk lemmas -/

 theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a := rfl
@ -49,6 +50,10 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
@[simp] theorem pop_mk {data : Array α} {size : data.size = n} :
    (Vector.mk data size).pop = Vector.mk data.pop (by simp [size]) := rfl

+@[simp] theorem mk_beq_mk [BEq α] {a b : Array α} {h : a.size = n} {h' : b.size = n} :
+    (Vector.mk a h == Vector.mk b h') = (a == b) := by
+  simp [instBEq, isEqv, Array.instBEq, Array.isEqv, h, h']
+
@[simp] theorem allDiff_mk [BEq α] (a : Array α) (h : a.size = n) :
    (Vector.mk a h).allDiff = a.allDiff := rfl

@ -181,6 +186,10 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a

@[simp] theorem toArray_push (a : Vector α n) (x) : (a.push x).toArray = a.toArray.push x := rfl

+@[simp] theorem toArray_beq_toArray [BEq α] (a : Vector α n) (b : Vector α n) :
+    (a.toArray == b.toArray) = (a == b) := by
+  simp [instBEq, isEqv, Array.instBEq, Array.isEqv, a.2, b.2]
+
@[simp] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl

@[simp] theorem toArray_reverse (a : Vector α n) : a.reverse.toArray = a.toArray.reverse := rfl
@ -236,8 +245,25 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
  cases v
  simp

-theorem toArray_inj : ∀ {v w : Vector α n}, v.toArray = w.toArray → v = w
-  | {..}, {..}, rfl => rfl
+@[simp] theorem toArray_mkVector : (mkVector n a).toArray = mkArray n a := rfl
+
+theorem toArray_inj {v w : Vector α n} : v.toArray = w.toArray ↔ v = w := by
+  cases v
+  cases w
+  simp
+
+/--
+`Vector.ext` is an extensionality theorem.
+Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
+-/
+@[ext]
+protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i] = b[i]) : a = b := by
+  apply Vector.toArray_inj.1
+  apply Array.ext
+  · rw [a.size_toArray, b.size_toArray]
+  · intro i hi _
+    rw [a.size_toArray] at hi
+    exact h i hi

@[simp] theorem toArray_eq_empty_iff (v : Vector α n) : v.toArray = #[] ↔ n = 0 := by
  rcases v with ⟨v, h⟩
@ -293,6 +319,10 @@ theorem toList_pop (a : Vector α n) : a.pop.toList = a.toList.dropLast := rfl

 theorem toList_push (a : Vector α n) (x) : (a.push x).toList = a.toList ++ [x] := by simp

+@[simp] theorem toList_beq_toList [BEq α] (a : Vector α n) (b : Vector α n) :
+    (a.toList == b.toList) = (a == b) := by
+  simp [instBEq, isEqv, Array.instBEq, Array.isEqv, a.2, b.2]
+
 theorem toList_range : (Vector.range n).toList = List.range n := by simp

 theorem toList_reverse (a : Vector α n) : a.reverse.toList = a.toList.reverse := by simp
@ -335,8 +365,12 @@ theorem toList_swap (a : Vector α n) (i j) (hi hj) :
  cases v
  simp

-theorem toList_inj : ∀ {v w : Vector α n}, v.toList = w.toList → v = w
-  | {..}, {..}, rfl => rfl
+@[simp] theorem toList_mkVector : (mkVector n a).toList = List.replicate n a := rfl
+
+theorem toList_inj {v w : Vector α n} : v.toList = w.toList ↔ v = w := by
+  cases v
+  cases w
+  simp [Array.toList_inj]

@[simp] theorem toList_eq_empty_iff (v : Vector α n) : v.toList = [] ↔ n = 0 := by
  rcases v with ⟨v, h⟩
@ -356,7 +390,7 @@ theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by sim

 /-- A vector of length `0` is the empty vector. -/
 protected theorem eq_empty (v : Vector α 0) : v = #v[] := by
-  apply Vector.toArray_inj
+  apply Vector.toArray_inj.1
  apply Array.eq_empty_of_size_eq_zero v.2


@ -364,7 +398,7 @@ protected theorem eq_empty (v : Vector α 0) : v = #v[] := by

 theorem eq_empty_of_size_eq_zero (xs : Vector α n) (h : n = 0) : xs = #v[].cast h.symm := by
  rcases xs with ⟨xs, rfl⟩
-  apply toArray_inj
+  apply toArray_inj.1
  simp only [List.length_eq_zero, Array.toList_eq_nil_iff] at h
  simp [h]

@ -405,7 +439,20 @@ theorem exists_push {xs : Vector α (n + 1)} :
    ∃ (ys : Vector α n) (a : α), xs = ys.push a := by
  rcases xs with ⟨xs, w⟩
  obtain ⟨ys, a, h⟩ := Array.exists_push_of_size_eq_add_one w
-  exact ⟨⟨ys, by simp_all⟩, a, toArray_inj h⟩
+  exact ⟨⟨ys, by simp_all⟩, a, toArray_inj.1 h⟩
+
+theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by
+  simp
+
+/-! ### mkVector -/
+
+@[simp] theorem mkVector_zero : mkVector 0 a = #v[] := rfl
+
+theorem mkVector_succ : mkVector (n + 1) a = (mkVector n a).push a := by
+  simp [mkVector, Array.mkArray_succ]
+
+theorem mkVector_inj : mkVector n a = mkVector n b ↔ n = 0 ∨ a = b := by
+  simp [← toArray_inj, toArray_mkVector, Array.mkArray_inj]

 /-! ## L[i] and L[i]? -/

@ -908,6 +955,67 @@ theorem mem_setIfInBounds (v : Vector α n) (i : Nat) (hi : i < n) (a : α) :
  simp [mem_iff_getElem]
  exact ⟨i, (by simpa using hi), by simp⟩

+/-! ### BEq -/
+
+@[simp] theorem push_beq_push [BEq α] {a b : α} {n : Nat} {v : Vector α n} {w : Vector α n} :
+    (v.push a == w.push b) = (v == w && a == b) := by
+  cases v
+  cases w
+  simp
+
+@[simp] theorem mkVector_beq_mkVector [BEq α] {a b : α} {n : Nat} :
+    (mkVector n a == mkVector n b) = (n == 0 || a == b) := by
+  cases n with
+  | zero => simp
+  | succ n =>
+    rw [mkVector_succ, mkVector_succ, push_beq_push, mkVector_beq_mkVector]
+    rw [Bool.eq_iff_iff]
+    simp +contextual
+
+@[simp] theorem reflBEq_iff [BEq α] [NeZero n] : ReflBEq (Vector α n) ↔ ReflBEq α := by
+  match n, NeZero.ne n with
+  | n + 1, _ =>
+    constructor
+    · intro h
+      constructor
+      intro a
+      suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
+        rw [mkVector_succ, push_beq_push, Bool.and_eq_true] at this
+        exact this.2
+      simp
+    · intro h
+      constructor
+      rintro ⟨v, h⟩
+      simpa using Array.isEqv_self_beq ..
+
+@[simp] theorem lawfulBEq_iff [BEq α] [NeZero n] : LawfulBEq (Vector α n) ↔ LawfulBEq α := by
+  match n, NeZero.ne n with
+  | n + 1, _ =>
+    constructor
+    · intro h
+      constructor
+      · intro a b h
+        have := mkVector_inj (n := n+1) (a := a) (b := b)
+        simp only [Nat.add_one_ne_zero, false_or] at this
+        rw [← this]
+        apply eq_of_beq
+        rw [mkVector_beq_mkVector]
+        simpa
+      · intro a
+        suffices (mkVector (n + 1) a == mkVector (n + 1) a) = true by
+          rw [mkVector_beq_mkVector] at this
+          simpa
+        simp
+    · intro h
+      constructor
+      · rintro ⟨a, ha⟩ ⟨b, hb⟩ h
+        simp at h
+        obtain ⟨hs, hi⟩ := Array.rel_of_isEqv h
+        ext i h
+        · simpa using hi _ (by omega)
+      · rintro ⟨a, ha⟩
+        simpa using Array.isEqv_self_beq ..
+
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/

@[simp] theorem getElem_ofFn {α n} (f : Fin n → α) (i : Nat) (h : i < n) :
@ -920,20 +1028,6 @@ theorem map_empty (f : α → β) : map f #v[] = #v[] := by
  rw [map, mk.injEq]
  exact Array.map_empty f

-
-/--
-`Vector.ext` is an extensionality theorem.
-Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
-/
-@[ext]
-protected theorem ext {a b : Vector α n} (h : (i : Nat) → (_ : i < n) → a[i] = b[i]) : a = b := by
-  apply Vector.toArray_inj
-  apply Array.ext
-  · rw [a.size_toArray, b.size_toArray]
-  · intro i hi _
-    rw [a.size_toArray] at hi
-    exact h i hi
-
@[simp] theorem getElem_push_last {v : Vector α n} {x : α} : (v.push x)[n] = x := by
  rcases v with ⟨data, rfl⟩
  simp