Init.Data.List.Nat.BEq

List.isEqv_eq_decide theorem

 {as bs : List α} {r : α → α → Bool} :
  isEqv as bs r =
    if h : as.length = bs.length then decide (∀ (i : Nat) (h' : i < as.length), r (as[i]'(h ▸ h')) (bs[i]'(h ▸ h')))
    else false

Full source

theorem isEqv_eq_decide {as bs : List α} {r : α → α → Bool} :
    isEqv as bs r = if h : as.length = bs.length then
      decide (∀ (i : Nat) (h' : i < as.length), r (as[i]'(h ▸ h')) (bs[i]'(h ▸ h'))) else false := by
  induction as generalizing bs with
  | nil =>
    cases bs <;> simp
  | cons a as ih =>
    cases bs with
    | nil => simp
    | cons b bs =>
      simp only [isEqv, ih, length_cons, Nat.add_right_cancel_iff]
      split <;> simp [Nat.forall_lt_succ_left']

Equivalence of Lists under Pairwise Relation via Decidable Check

Informal description

For any two lists `as` and `bs` of type `List α` and a binary relation `r : α → α → Bool`, the equivalence check `isEqv as bs r` evaluates to `true` if and only if the lists have the same length and for every index `i` less than the length of `as`, the relation `r` holds between the corresponding elements `as[i]` and `bs[i]`. Otherwise, it evaluates to `false`.

List.beq_eq_isEqv theorem

[BEq α] {as bs : List α} : as.beq bs = isEqv as bs (· == ·)

Full source

theorem beq_eq_isEqv [BEq α] {as bs : List α} : as.beq bs = isEqv as bs (· == ·) := by
  induction as generalizing bs with
  | nil =>
    cases bs <;> simp
  | cons a as ih =>
    cases bs with
    | nil => simp
    | cons b bs =>
      simp only [beq_cons₂, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff,
        Nat.forall_lt_succ_left', getElem_cons_zero, getElem_cons_succ, Bool.decide_and,
        Bool.decide_eq_true]
      split <;> simp

Boolean Equality of Lists Coincides with Pairwise Element Equality Check

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 check `as.beq bs` is equal to the equivalence check `isEqv as bs (· == ·)`, where `isEqv` tests whether the lists have the same length and all corresponding elements are equal according to the `==` relation.

List.beq_eq_decide theorem

 [BEq α] {as bs : List α} :
  (as == bs) =
    if h : as.length = bs.length then decide (∀ (i : Nat) (h' : i < as.length), as[i] == bs[i]'(h ▸ h')) else false

Full source

theorem beq_eq_decide [BEq α] {as bs : List α} :
    (as == bs) = if h : as.length = bs.length then
      decide (∀ (i : Nat) (h' : i < as.length), as[i] == bs[i]'(h ▸ h')) else false := by
  simp [BEq.beq, beq_eq_isEqv, isEqv_eq_decide]

Boolean Equality of Lists via Pairwise Element Comparison

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 check `as == bs` evaluates to `true` if and only if the lists have the same length and for every index `i` less than the length of `as`, the corresponding elements `as[i]` and `bs[i]` are equal according to the `==` relation. Otherwise, it evaluates to `false`.