Init.Data.Array.DecidableEq

Array.isEqv_iff_rel theorem

 {xs ys : Array α} {r} :
  Array.isEqv xs ys r ↔ ∃ h : xs.size = ys.size, ∀ (i : Nat) (h' : i < xs.size), r (xs[i]) (ys[i]'(h ▸ h'))

Full source

theorem isEqv_iff_rel {xs ys : Array α} {r} :
    Array.isEqvArray.isEqv xs ys r ↔ ∃ h : xs.size = ys.size, ∀ (i : Nat) (h' : i < xs.size), r (xs[i]) (ys[i]'(h ▸ h')) :=
  ⟨rel_of_isEqv, fun ⟨h, w⟩ => by
    simp only [isEqv, ← h, ↓reduceDIte]
    exact isEqvAux_of_rel h (by simp [h]) w⟩

Element-wise Array Equivalence Condition

Informal description

For any arrays `xs` and `ys` of type `Array α` and a relation `r` on `α`, the arrays are element-wise equivalent under `r` if and only if they have the same size and for every index `i` less than the size of `xs`, the relation `r` holds between the `i`-th elements of `xs` and `ys`.

Array.isEqv_eq_decide theorem

 (xs ys : Array α) (r) :
  Array.isEqv xs ys r =
    if h : xs.size = ys.size then decide (∀ (i : Nat) (h' : i < xs.size), r (xs[i]) (ys[i]'(h ▸ h'))) else false

Full source

theorem isEqv_eq_decide (xs ys : Array α) (r) :
    Array.isEqv xs ys r =
      if h : xs.size = ys.size then decide (∀ (i : Nat) (h' : i < xs.size), r (xs[i]) (ys[i]'(h ▸ h'))) else false := by
  by_cases h : Array.isEqv xs ys r
  · simp only [h, Bool.true_eq]
    simp only [isEqv_iff_rel] at h
    obtain ⟨h, w⟩ := h
    simp [h, w]
  · let h' := h
    simp only [Bool.not_eq_true] at h
    simp only [h, Bool.false_eq, dite_eq_right_iff, decide_eq_false_iff_not, Classical.not_forall,
      Bool.not_eq_true]
    simpa [isEqv_iff_rel] using h'

Equivalence Check for Arrays via Size and Pointwise Relation

Informal description

For any two arrays `xs` and `ys` of type `Array α` and a relation `r`, the equivalence check `Array.isEqv xs ys r` evaluates to the boolean result of deciding whether `xs` and `ys` have the same size and satisfy `r(xs[i], ys[i])` for all valid indices `i`. If the sizes are unequal, the result is `false`.

Array.isEqv_toList theorem

[BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r)

Full source

@[simp] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
  simp [isEqv_eq_decide, List.isEqv_eq_decide]

Equivalence of Array and List Representations under Relation $r$

Informal description

For any arrays `xs` and `ys` of type `Array α` with a boolean equality relation `BEq α`, the equivalence check between their list representations `xs.toList` and `ys.toList` under relation `r` is equal to the equivalence check between the arrays themselves under the same relation `r`.

Array.isEqv_self_beq theorem

[BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs (· == ·) = true

Full source

theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs (· == ·) = true := by
  simp [isEqv, isEqvAux_self]

Reflexivity of Array Boolean Equality Check: `isEqv xs xs (· == ·) = true`

Informal description

For any type $\alpha$ with a reflexive boolean equality relation `==`, and for any array `xs` of elements of type $\alpha$, the boolean equality check `Array.isEqv xs xs (· == ·)` evaluates to `true`.

Array.isEqv_self theorem

[DecidableEq α] (xs : Array α) : Array.isEqv xs xs (· = ·) = true

Full source

theorem isEqv_self [DecidableEq α] (xs : Array α) : Array.isEqv xs xs (· = ·) = true := by
  simp [isEqv, isEqvAux_self]

Reflexivity of Array Equivalence Check: $\text{isEqv}(xs, xs, \cdot = \cdot) = \text{true}$

Informal description

For any type $\alpha$ with decidable equality and any array `xs` of type `Array α`, the reflexive equivalence check `Array.isEqv xs xs (· = ·)` evaluates to `true`.

Array.instDecidableEq instance

[DecidableEq α] : DecidableEq (Array α)

Full source

instance [DecidableEq α] : DecidableEq (Array α) :=
  fun xs ys =>
    match h:isEqv xs ys (fun a b => a = b) with
    | true  => isTrue (eq_of_isEqv xs ys h)
    | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction

Decidable Equality for Arrays

Informal description

For any type $\alpha$ with decidable equality, the type `Array α` of dynamic arrays over $\alpha$ also has decidable equality. That is, for any two arrays `xs` and `ys` of type `Array α`, the equality `xs = ys` is decidable.

Array.beq_eq_decide theorem

 [BEq α] (xs ys : Array α) :
  (xs == ys) = if h : xs.size = ys.size then decide (∀ (i : Nat) (h' : i < xs.size), xs[i] == ys[i]'(h ▸ h')) else false

Full source

theorem beq_eq_decide [BEq α] (xs ys : Array α) :
    (xs == ys) = if h : xs.size = ys.size then
      decide (∀ (i : Nat) (h' : i < xs.size), xs[i] == ys[i]'(h ▸ h')) else false := by
  simp [BEq.beq, isEqv_eq_decide]

Boolean Equality of Arrays via Size and Element-wise Comparison

Informal description

For any type $\alpha$ with a boolean equality relation `==`, and for any two arrays `xs` and `ys` of type `Array α`, the boolean equality `xs == ys` evaluates to the result of the following decision procedure: if the sizes of `xs` and `ys` are equal, then check whether all corresponding elements `xs[i]` and `ys[i]` are equal under `==` for every valid index `i`; otherwise, the result is `false`.

Array.beq_toList theorem

[BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys)

Full source

@[simp] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
  simp [beq_eq_decide, List.beq_eq_decide]

Equality of Array-to-List Conversions Preserves Boolean Equality

Informal description

For any type $\alpha$ with a boolean equality relation `==`, and for any two arrays `xs` and `ys` of type `Array α`, the boolean equality of their list representations `xs.toList == ys.toList` is equal to the boolean equality of the arrays themselves `xs == ys`.

List.isEqv_toArray theorem

[BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r)

Full source

@[simp] theorem isEqv_toArray [BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r) := by
  simp [isEqv_eq_decide, Array.isEqv_eq_decide]

Equivalence of List and Array Equivalence Checks under Conversion

Informal description

For any two lists `as` and `bs` of type `List α` with a boolean equality relation `BEq α`, the equivalence check `as.toArray.isEqv bs.toArray r` (after converting the lists to arrays) is equal to the equivalence check `as.isEqv bs r` on the original lists.

List.beq_toArray theorem

[BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs)

Full source

@[simp] theorem beq_toArray [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs) := by
  simp [beq_eq_decide, Array.beq_eq_decide]

Preservation of Boolean Equality under List-to-Array Conversion

Informal description

For any type $\alpha$ with a boolean equality relation `==`, and for any two lists `as` and `bs` of type `List \alpha`, the boolean equality of their array conversions `as.toArray == bs.toArray` is equal to the boolean equality of the original lists `as == bs`.

Array.instLawfulBEq instance

[BEq α] [LawfulBEq α] : LawfulBEq (Array α)

Full source

instance [BEq α] [LawfulBEq α] : LawfulBEq (Array α) where
  rfl := by simp [BEq.beq, isEqv_self_beq]
  eq_of_beq := by
    rintro ⟨_⟩ ⟨_⟩ h
    simpa using h

Lawful Boolean Equality for Arrays

Informal description

For any type $\alpha$ with a lawful boolean equality relation `==`, the boolean equality relation on arrays of $\alpha$ is also lawful. This means that for any two arrays `xs` and `ys` of type `Array α`, the boolean equality `xs == ys` holds if and only if the arrays are element-wise equal according to the underlying equality on $\alpha$.