Mathlib.Data.List.Forall2

List.Forall₂.imp theorem

(H : ∀ a b, R a b → S a b) {l₁ l₂} (h : Forall₂ R l₁ l₂) : Forall₂ S l₁ l₂

Full source

theorem Forall₂.imp (H : ∀ a b, R a b → S a b) {l₁ l₂} (h : Forall₂ R l₁ l₂) : Forall₂ S l₁ l₂ := by
  induction h <;> constructor <;> solve_by_elim

Preservation of List Elementwise Relation Under Implication

Informal description

Let $R$ and $S$ be binary relations on types $\alpha$ and $\beta$ such that for all $a \in \alpha$ and $b \in \beta$, $R(a,b)$ implies $S(a,b)$. Then for any two lists $l_1$ of elements in $\alpha$ and $l_2$ of elements in $\beta$, if $\text{Forall}_2(R, l_1, l_2)$ holds (meaning $l_1$ and $l_2$ have the same length and $R$ relates their corresponding elements), then $\text{Forall}_2(S, l_1, l_2)$ also holds.

List.Forall₂.mp theorem

 {Q : α → β → Prop} (h : ∀ a b, Q a b → R a b → S a b) : ∀ {l₁ l₂}, Forall₂ Q l₁ l₂ → Forall₂ R l₁ l₂ → Forall₂ S l₁ l₂

Full source

theorem Forall₂.mp {Q : α → β → Prop} (h : ∀ a b, Q a b → R a b → S a b) :
    ∀ {l₁ l₂}, Forall₂ Q l₁ l₂ → Forall₂ R l₁ l₂ → Forall₂ S l₁ l₂
  | [], [], Forall₂.nil, Forall₂.nil => Forall₂.nil
  | a :: _, b :: _, Forall₂.cons hr hrs, Forall₂.cons hq hqs =>
    Forall₂.cons (h a b hr hq) (Forall₂.mp h hrs hqs)

Pairwise List Relation Implication: $Q \land R \Rightarrow S$ implies $\text{Forall}_2(Q) \land \text{Forall}_2(R) \Rightarrow \text{Forall}_2(S)$

Informal description

Let $Q, R, S$ be binary relations on types $\alpha$ and $\beta$. Suppose that for all $a \in \alpha$ and $b \in \beta$, whenever $Q(a,b)$ and $R(a,b)$ hold, then $S(a,b)$ holds. Then for any two lists $l_1$ of $\alpha$ and $l_2$ of $\beta$, if $l_1$ and $l_2$ satisfy $\text{Forall}_2(Q)$ and $\text{Forall}_2(R)$, they also satisfy $\text{Forall}_2(S)$. Here $\text{Forall}_2(R)$ means the lists have the same length and the relation $R$ holds pairwise for corresponding elements.

List.Forall₂.flip theorem

: ∀ {a b}, Forall₂ (flip R) b a → Forall₂ R a b

Full source

theorem Forall₂.flip : ∀ {a b}, Forall₂ (flip R) b a → Forall₂ R a b
  | _, _, Forall₂.nil => Forall₂.nil
  | _ :: _, _ :: _, Forall₂.cons h₁ h₂ => Forall₂.cons h₁ h₂.flip

Flipped Double Universal Quantification Implies Original

Informal description

For any lists `a` and `b`, if the relation `R` holds in flipped order between corresponding elements of `b` and `a` (i.e., `Forall₂ (flip R) b a`), then the relation `R` holds between corresponding elements of `a` and `b` (i.e., `Forall₂ R a b`).

List.forall₂_same theorem

: ∀ {l : List α}, Forall₂ Rₐ l l ↔ ∀ x ∈ l, Rₐ x x

Full source

@[simp]
theorem forall₂_same : ∀ {l : List α}, Forall₂Forall₂ Rₐ l l ↔ ∀ x ∈ l, Rₐ x x
  | [] => by simp
  | a :: l => by simp [@forall₂_same l]

Reflexive Pairwise List Relation Equivalence: $\text{Forall}_2(R_\alpha)(l,l) \leftrightarrow \forall x \in l, R_\alpha(x,x)$

Informal description

For any list $l$ of elements of type $\alpha$, the relation $\text{Forall}_2(R_\alpha)$ holds between $l$ and itself if and only if for every element $x$ in $l$, the relation $R_\alpha(x, x)$ holds. Here $\text{Forall}_2(R_\alpha)$ means that the two lists have the same length and the relation $R_\alpha$ holds pairwise for corresponding elements.

List.forall₂_refl theorem

[IsRefl α Rₐ] (l : List α) : Forall₂ Rₐ l l

Full source

theorem forall₂_refl [IsRefl α Rₐ] (l : List α) : Forall₂ Rₐ l l :=
  forall₂_same.2 fun _ _ => refl _

Reflexivity of Double Universal Quantification on Lists

Informal description

For any reflexive binary relation $R_\alpha$ on a type $\alpha$ and any list $l$ of elements of type $\alpha$, the relation $\text{Forall}_2(R_\alpha)$ holds between $l$ and itself. Here $\text{Forall}_2(R_\alpha)$ means that the two lists have the same length and the relation $R_\alpha$ holds pairwise for corresponding elements.

List.forall₂_eq_eq_eq theorem

: Forall₂ ((· = ·) : α → α → Prop) = Eq

Full source

@[simp]
theorem forall₂_eq_eq_eq : Forall₂ ((· = ·) : α → α → Prop) = Eq := by
  funext a b; apply propext
  constructor
  · intro h
    induction h
    · rfl
    simp only [*]
  · rintro rfl
    exact forall₂_refl _

$\text{Forall}_2$ with Equality is List Equality

Informal description

For any type $\alpha$, the relation $\text{Forall}_2$ with the equality relation on $\alpha$ is equivalent to the equality relation on lists of $\alpha$. In other words, $\text{Forall}_2(\lambda x y, x = y) = \text{Eq}$.

List.forall₂_nil_left_iff theorem

{l} : Forall₂ R nil l ↔ l = nil

Full source

@[simp]
theorem forall₂_nil_left_iff {l} : Forall₂Forall₂ R nil l ↔ l = nil :=
  ⟨fun H => by cases H; rfl, by rintro rfl; exact Forall₂.nil⟩

Empty List Left Condition for Double Universal Quantification

Informal description

For any relation $R$ and any list $l$, the statement $\text{Forall}_2(R, \text{nil}, l)$ holds if and only if $l$ is the empty list (i.e., $l = \text{nil}$).

List.forall₂_nil_right_iff theorem

{l} : Forall₂ R l nil ↔ l = nil

Full source

@[simp]
theorem forall₂_nil_right_iff {l} : Forall₂Forall₂ R l nil ↔ l = nil :=
  ⟨fun H => by cases H; rfl, by rintro rfl; exact Forall₂.nil⟩

Empty List Right Case for Double Universal Quantification on Lists

Informal description

For any list `l` and binary relation `R`, the predicate `Forall₂ R l nil` holds if and only if `l` is the empty list. In other words, the only list that satisfies `Forall₂ R` with the empty list is the empty list itself.

List.forall₂_cons_left_iff theorem

{a l u} : Forall₂ R (a :: l) u ↔ ∃ b u', R a b ∧ Forall₂ R l u' ∧ u = b :: u'

Full source

theorem forall₂_cons_left_iff {a l u} :
    Forall₂Forall₂ R (a :: l) u ↔ ∃ b u', R a b ∧ Forall₂ R l u' ∧ u = b :: u' :=
  Iff.intro
    (fun h =>
      match u, h with
      | b :: u', Forall₂.cons h₁ h₂ => ⟨b, u', h₁, h₂, rfl⟩)
    fun h =>
    match u, h with
    | _, ⟨_, _, h₁, h₂, rfl⟩ => Forall₂.cons h₁ h₂

Characterization of $\text{Forall}_2$ for Cons on the Left

Informal description

For any relation $R$, element $a$, and lists $l$ and $u$, the relation $\text{Forall}_2 R (a :: l) u$ holds if and only if there exists an element $b$ and a list $u'$ such that $R a b$ holds, $\text{Forall}_2 R l u'$ holds, and $u = b :: u'$.

List.forall₂_cons_right_iff theorem

{b l u} : Forall₂ R u (b :: l) ↔ ∃ a u', R a b ∧ Forall₂ R u' l ∧ u = a :: u'

Full source

theorem forall₂_cons_right_iff {b l u} :
    Forall₂Forall₂ R u (b :: l) ↔ ∃ a u', R a b ∧ Forall₂ R u' l ∧ u = a :: u' :=
  Iff.intro
    (fun h =>
      match u, h with
      | b :: u', Forall₂.cons h₁ h₂ => ⟨b, u', h₁, h₂, rfl⟩)
    fun h =>
    match u, h with
    | _, ⟨_, _, h₁, h₂, rfl⟩ => Forall₂.cons h₁ h₂

Characterization of $\text{Forall₂}$ for a Cons Right List

Informal description

For any relation $R$, list $u$, and element $b$ with tail list $l$, the statement $\text{Forall₂}\ R\ u\ (b :: l)$ holds if and only if there exists an element $a$ and a list $u'$ such that $R\ a\ b$ holds, $\text{Forall₂}\ R\ u'\ l$ holds, and $u$ is equal to $a :: u'$.

List.forall₂_and_left theorem

{p : α → Prop} : ∀ l u, Forall₂ (fun a b => p a ∧ R a b) l u ↔ (∀ a ∈ l, p a) ∧ Forall₂ R l u

Full source

theorem forall₂_and_left {p : α → Prop} :
    ∀ l u, Forall₂Forall₂ (fun a b => p a ∧ R a b) l u ↔ (∀ a ∈ l, p a) ∧ Forall₂ R l u
  | [], u => by
    simp only [forall₂_nil_left_iff, forall_prop_of_false not_mem_nil, imp_true_iff, true_and]
  | a :: l, u => by
    simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons, and_assoc,
      @and_comm _ (p a), @and_left_comm _ (p a), exists_and_left]
    simp only [and_comm, and_assoc, and_left_comm, ← exists_and_right]

$\mathrm{Forall}_2$ with Left Predicate is Equivalent to Pointwise Predicate and $\mathrm{Forall}_2$ Relation

Informal description

For any predicate $p : \alpha \to \mathrm{Prop}$ and lists $l$ and $u$, the relation $\mathrm{Forall}_2 (\lambda a b, p(a) \land R(a, b))$ holds between $l$ and $u$ if and only if $p(a)$ holds for every element $a$ in $l$ and $\mathrm{Forall}_2 R$ holds between $l$ and $u$.

List.forall₂_map_left_iff theorem

{f : γ → α} : ∀ {l u}, Forall₂ R (map f l) u ↔ Forall₂ (fun c b => R (f c) b) l u

Full source

@[simp]
theorem forall₂_map_left_iff {f : γ → α} :
    ∀ {l u}, Forall₂Forall₂ R (map f l) u ↔ Forall₂ (fun c b => R (f c) b) l u
  | [], _ => by simp only [map, forall₂_nil_left_iff]
  | a :: l, _ => by simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]

Mapping Preserves Pairwise Relation on Lists: $\text{Forall₂}\,R\,(\text{map}\,f\,l)\,u \leftrightarrow \text{Forall₂}\,(\lambda c\,b, R\,(f\,c)\,b)\,l\,u$

Informal description

For any function $f : \gamma \to \alpha$ and any lists $l$ (of type $\gamma$) and $u$ (of type $\beta$), the following are equivalent: 1. The lists $\text{map}\,f\,l$ and $u$ satisfy $\text{Forall₂}\,R$ (i.e., they have the same length and $R$ holds pairwise for their elements). 2. The lists $l$ and $u$ satisfy $\text{Forall₂}\,(\lambda c\,b, R\,(f\,c)\,b)$ (i.e., they have the same length and $R$ holds pairwise after applying $f$ to elements of $l$).

List.forall₂_map_right_iff theorem

{f : γ → β} : ∀ {l u}, Forall₂ R l (map f u) ↔ Forall₂ (fun a c => R a (f c)) l u

Full source

@[simp]
theorem forall₂_map_right_iff {f : γ → β} :
    ∀ {l u}, Forall₂Forall₂ R l (map f u) ↔ Forall₂ (fun a c => R a (f c)) l u
  | _, [] => by simp only [map, forall₂_nil_right_iff]
  | _, b :: u => by simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]

Mapping Right List Preserves Forall₂ Relation

Informal description

For any function $f : \gamma \to \beta$ and any lists $l$ and $u$, the relation `Forall₂ R l (map f u)` holds if and only if `Forall₂ (fun a c => R a (f c)) l u` holds. In other words, the relation `Forall₂ R` holds between a list $l$ and the mapped list `map f u` precisely when the relation `R` holds between each element of $l$ and the corresponding element of $u$ after applying $f$.

List.left_unique_forall₂' theorem

(hr : LeftUnique R) : ∀ {a b c}, Forall₂ R a c → Forall₂ R b c → a = b

Full source

theorem left_unique_forall₂' (hr : LeftUnique R) : ∀ {a b c}, Forall₂ R a c → Forall₂ R b c → a = b
  | _, _, _, Forall₂.nil, Forall₂.nil => rfl
  | _, _, _, Forall₂.cons ha₀ h₀, Forall₂.cons ha₁ h₁ =>
    hr ha₀ ha₁ ▸ left_unique_forall₂' hr h₀ h₁ ▸ rfl

Left Uniqueness of Pairwise List Relation: $\text{Forall₂}\,R\,a\,c \land \text{Forall₂}\,R\,b\,c \to a = b$

Informal description

Let $R$ be a left unique relation. For any lists $a$, $b$, and $c$, if $\text{Forall₂}\,R\,a\,c$ and $\text{Forall₂}\,R\,b\,c$ hold, then $a = b$. In other words, if two lists $a$ and $b$ are both pairwise related via $R$ to the same list $c$, then $a$ and $b$ must be equal.

Relator.LeftUnique.forall₂ theorem

(hr : LeftUnique R) : LeftUnique (Forall₂ R)

Full source

theorem _root_.Relator.LeftUnique.forall₂ (hr : LeftUnique R) : LeftUnique (Forall₂ R) :=
  @left_unique_forall₂' _ _ _ hr

Left Uniqueness of Pairwise List Relation $\text{Forall₂}\, R$

Informal description

Let $R$ be a left unique relation. Then the pairwise list relation $\text{Forall₂}\, R$ is also left unique. That is, for any lists $l_1$, $l_2$, and $l_3$, if $\text{Forall₂}\, R\, l_1\, l_3$ and $\text{Forall₂}\, R\, l_2\, l_3$ hold, then $l_1 = l_2$.

List.right_unique_forall₂' theorem

(hr : RightUnique R) : ∀ {a b c}, Forall₂ R a b → Forall₂ R a c → b = c

Full source

theorem right_unique_forall₂' (hr : RightUnique R) :
    ∀ {a b c}, Forall₂ R a b → Forall₂ R a c → b = c
  | _, _, _, Forall₂.nil, Forall₂.nil => rfl
  | _, _, _, Forall₂.cons ha₀ h₀, Forall₂.cons ha₁ h₁ =>
    hr ha₀ ha₁ ▸ right_unique_forall₂' hr h₀ h₁ ▸ rfl

Right Uniqueness of List Element-wise Relation

Informal description

Let $R$ be a right unique relation. For any lists $a$, $b$, and $c$, if $R$ relates corresponding elements of $a$ and $b$ (i.e., $\text{Forall₂}\, R\, a\, b$) and $R$ relates corresponding elements of $a$ and $c$ (i.e., $\text{Forall₂}\, R\, a\, c$), then $b = c$.

Relator.RightUnique.forall₂ theorem

(hr : RightUnique R) : RightUnique (Forall₂ R)

Full source

theorem _root_.Relator.RightUnique.forall₂ (hr : RightUnique R) : RightUnique (Forall₂ R) :=
  @right_unique_forall₂' _ _ _ hr

Right Uniqueness of List-wise Relation $\text{Forall₂}\, R$

Informal description

Let $R$ be a right unique relation. Then the list-wise relation $\text{Forall₂}\, R$ is also right unique. That is, for any lists $l_1$, $l_2$, and $l_3$, if $\text{Forall₂}\, R\, l_1\, l_2$ and $\text{Forall₂}\, R\, l_1\, l_3$ hold, then $l_2 = l_3$.

Relator.BiUnique.forall₂ theorem

(hr : BiUnique R) : BiUnique (Forall₂ R)

Full source

theorem _root_.Relator.BiUnique.forall₂ (hr : BiUnique R) : BiUnique (Forall₂ R) :=
  ⟨hr.left.forall₂, hr.right.forall₂⟩

Bi-uniqueness of Pairwise List Relation $\text{Forall₂}\, R$

Informal description

Let $R$ be a bi-unique relation. Then the pairwise list relation $\text{Forall₂}\, R$ is also bi-unique. That is: 1. (Left unique) For any lists $l_1$, $l_2$, and $l_3$, if $\text{Forall₂}\, R\, l_1\, l_3$ and $\text{Forall₂}\, R\, l_2\, l_3$ hold, then $l_1 = l_2$. 2. (Right unique) For any lists $l_1$, $l_2$, and $l_3$, if $\text{Forall₂}\, R\, l_1\, l_2$ and $\text{Forall₂}\, R\, l_1\, l_3$ hold, then $l_2 = l_3$.

List.Forall₂.length_eq theorem

: ∀ {l₁ l₂}, Forall₂ R l₁ l₂ → length l₁ = length l₂

Full source

theorem Forall₂.length_eq : ∀ {l₁ l₂}, Forall₂ R l₁ l₂ → length l₁ = length l₂
  | _, _, Forall₂.nil => rfl
  | _, _, Forall₂.cons _ h₂ => congr_arg succ (Forall₂.length_eq h₂)

Length Preservation under `Forall₂` Relation

Informal description

For any two lists `l₁` and `l₂` and any binary relation `R`, if `Forall₂ R l₁ l₂` holds (meaning corresponding elements of `l₁` and `l₂` are related by `R`), then the lengths of `l₁` and `l₂` are equal.

List.Forall₂.get theorem

 :
  ∀ {x : List α} {y : List β},
    Forall₂ R x y → ∀ ⦃i : ℕ⦄ (hx : i < x.length) (hy : i < y.length), R (x.get ⟨i, hx⟩) (y.get ⟨i, hy⟩)

Full source

theorem Forall₂.get :
    ∀ {x : List α} {y : List β}, Forall₂ R x y →
      ∀ ⦃i : ℕ⦄ (hx : i < x.length) (hy : i < y.length), R (x.get ⟨i, hx⟩) (y.get ⟨i, hy⟩)
  | _, _, Forall₂.cons ha _, 0, _, _ => ha
  | _, _, Forall₂.cons _ hl, succ _, _, _ => hl.get _ _

Element-wise Relation Preservation under `Forall₂`

Informal description

For any two lists $x$ and $y$ of types $\alpha$ and $\beta$ respectively, if `Forall₂ R x y` holds, then for every index $i$ such that $i$ is less than the lengths of both $x$ and $y$, the relation $R$ holds between the $i$-th elements of $x$ and $y$. More formally, if $x = [x_0, \dots, x_{n-1}]$ and $y = [y_0, \dots, y_{n-1}]$ satisfy `Forall₂ R x y`, then for every $i$ with $0 \leq i < n$, we have $R(x_i, y_i)$.

List.forall₂_of_length_eq_of_get theorem

 : ∀ {x : List α} {y : List β}, x.length = y.length → (∀ i h₁ h₂, R (x.get ⟨i, h₁⟩) (y.get ⟨i, h₂⟩)) → Forall₂ R x y

Full source

theorem forall₂_of_length_eq_of_get :
    ∀ {x : List α} {y : List β},
      x.length = y.length → (∀ i h₁ h₂, R (x.get ⟨i, h₁⟩) (y.get ⟨i, h₂⟩)) → Forall₂ R x y
  | [], [], _, _ => Forall₂.nil
  | _ :: _, _ :: _, hl, h =>
    Forall₂.cons (h 0 (Nat.zero_lt_succ _) (Nat.zero_lt_succ _))
      (forall₂_of_length_eq_of_get (succ.inj hl) fun i h₁ h₂ =>
        h i.succ (succ_lt_succ h₁) (succ_lt_succ h₂))

Construction of $\text{Forall}_2$ Relation from Element-wise Condition

Informal description

For any two lists $x$ of type $\alpha$ and $y$ of type $\beta$, if the lengths of $x$ and $y$ are equal, and for every index $i$ with corresponding bounds $h_1$ and $h_2$, the relation $R$ holds between the $i$-th elements of $x$ and $y$, then the relation $\text{Forall}_2(R)$ holds between $x$ and $y$.

List.forall₂_iff_get theorem

 {l₁ : List α} {l₂ : List β} : Forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ i h₁ h₂, R (l₁.get ⟨i, h₁⟩) (l₂.get ⟨i, h₂⟩)

Full source

theorem forall₂_iff_get {l₁ : List α} {l₂ : List β} :
    Forall₂Forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ i h₁ h₂, R (l₁.get ⟨i, h₁⟩) (l₂.get ⟨i, h₂⟩) :=
  ⟨fun h => ⟨h.length_eq, h.get⟩, fun h => forall₂_of_length_eq_of_get h.1 h.2⟩

Characterization of $\text{Forall}_2$ Relation via List Length and Element-wise Condition

Informal description

For two lists $l₁$ of type $\alpha$ and $l₂$ of type $\beta$, the relation $\text{Forall}_2(R, l₁, l₂)$ holds if and only if the lengths of $l₁$ and $l₂$ are equal, and for every index $i$ with corresponding bounds $h₁$ and $h₂$, the relation $R$ holds between the $i$-th elements of $l₁$ and $l₂$. In other words, $\text{Forall}_2(R, l₁, l₂) \leftrightarrow \text{length}(l₁) = \text{length}(l₂) \land \forall i h₁ h₂, R(l₁[i], l₂[i])$.

List.forall₂_zip theorem

: ∀ {l₁ l₂}, Forall₂ R l₁ l₂ → ∀ {a b}, (a, b) ∈ zip l₁ l₂ → R a b

Full source

theorem forall₂_zip : ∀ {l₁ l₂}, Forall₂ R l₁ l₂ → ∀ {a b}, (a, b)(a, b) ∈ zip l₁ l₂ → R a b
  | _, _, Forall₂.cons h₁ h₂, x, y, hx => by
    rw [zip, zipWith, mem_cons] at hx
    match hx with
    | Or.inl rfl => exact h₁
    | Or.inr h₃ => exact forall₂_zip h₂ h₃

Zipped Elements Satisfy Relation in `Forall₂` Lists

Informal description

For any two lists `l₁` and `l₂` and a relation `R`, if `Forall₂ R l₁ l₂` holds (meaning the lists have the same length and corresponding elements are related by `R`), then for any pair `(a, b)` in the zip of `l₁` and `l₂`, the relation `R a b` holds.

List.forall₂_iff_zip theorem

{l₁ l₂} : Forall₂ R l₁ l₂ ↔ length l₁ = length l₂ ∧ ∀ {a b}, (a, b) ∈ zip l₁ l₂ → R a b

Full source

theorem forall₂_iff_zip {l₁ l₂} :
    Forall₂Forall₂ R l₁ l₂ ↔ length l₁ = length l₂ ∧ ∀ {a b}, (a, b) ∈ zip l₁ l₂ → R a b :=
  ⟨fun h => ⟨Forall₂.length_eq h, @forall₂_zip _ _ _ _ _ h⟩, fun h => by
    obtain ⟨h₁, h₂⟩ := h
    induction l₁ generalizing l₂ with
    | nil =>
      cases length_eq_zero_iff.1 h₁.symm
      constructor
    | cons a l₁ IH =>
      rcases l₂ with - | ⟨b, l₂⟩
      · simp at h₁
      · simp only [length_cons, succ.injEq] at h₁
        exact Forall₂.cons (h₂ <| by simp [zip])
          (IH h₁ fun h => h₂ <| by
            simp only [zip, zipWith, find?, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h)⟩

Characterization of $\text{Forall₂}\,R$ via List Length and Zipped Elements

Informal description

For two lists $l₁$ and $l₂$, the relation $\text{Forall₂}\,R\,l₁\,l₂$ holds if and only if the lengths of $l₁$ and $l₂$ are equal, and for every pair $(a, b)$ in the zip of $l₁$ and $l₂$, the relation $R\,a\,b$ holds.

List.forall₂_take theorem

: ∀ (n) {l₁ l₂}, Forall₂ R l₁ l₂ → Forall₂ R (take n l₁) (take n l₂)

Full source

theorem forall₂_take : ∀ (n) {l₁ l₂}, Forall₂ R l₁ l₂ → Forall₂ R (take n l₁) (take n l₂)
  | 0, _, _, _ => by simp only [Forall₂.nil, take]
  | _ + 1, _, _, Forall₂.nil => by simp only [Forall₂.nil, take]
  | n + 1, _, _, Forall₂.cons h₁ h₂ => by simp [And.intro h₁ h₂, forall₂_take n]

Preservation of $\text{Forall₂}\,R$ under Taking Prefixes of Lists

Informal description

For any natural number $n$ and any two lists $l₁$ and $l₂$ such that $\text{Forall₂}\,R\,l₁\,l₂$ holds (i.e., the lists have the same length and corresponding elements satisfy the relation $R$), the $\text{Forall₂}\,R$ relation also holds between the first $n$ elements of $l₁$ and the first $n$ elements of $l₂$.

List.forall₂_drop theorem

: ∀ (n) {l₁ l₂}, Forall₂ R l₁ l₂ → Forall₂ R (drop n l₁) (drop n l₂)

Full source

theorem forall₂_drop : ∀ (n) {l₁ l₂}, Forall₂ R l₁ l₂ → Forall₂ R (drop n l₁) (drop n l₂)
  | 0, _, _, h => by simp only [drop, h]
  | _ + 1, _, _, Forall₂.nil => by simp only [Forall₂.nil, drop]
  | n + 1, _, _, Forall₂.cons h₁ h₂ => by simp [And.intro h₁ h₂, forall₂_drop n]

Preservation of Element-wise Relation under List Drop Operation

Informal description

For any natural number $n$ and any two lists $l₁$ and $l₂$ of the same length, if the relation `Forall₂ R l₁ l₂` holds (meaning that corresponding elements of $l₁$ and $l₂$ satisfy the relation $R$), then the relation `Forall₂ R` also holds for the lists obtained by dropping the first $n$ elements from $l₁$ and $l₂$ respectively. In other words, $\text{drop}(n, l₁)$ and $\text{drop}(n, l₂)$ satisfy $R$ element-wise.

List.forall₂_take_append theorem

 (l : List α) (l₁ : List β) (l₂ : List β) (h : Forall₂ R l (l₁ ++ l₂)) : Forall₂ R (List.take (length l₁) l) l₁

Full source

theorem forall₂_take_append (l : List α) (l₁ : List β) (l₂ : List β) (h : Forall₂ R l (l₁ ++ l₂)) :
    Forall₂ R (List.take (length l₁) l) l₁ := by
  have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) :=
    forall₂_take (length l₁) h
  rwa [take_left] at h'

Preservation of $\text{Forall₂}\,R$ under Taking Prefix Matching First List in Concatenation

Informal description

Let $l$ be a list of elements of type $\alpha$, and $l₁$ and $l₂$ be lists of elements of type $\beta$. If $\text{Forall₂}\,R\,l\,(l₁ \mathbin{+\kern-0.5em+} l₂)$ holds (i.e., $l$ and the concatenation $l₁ \mathbin{+\kern-0.5em+} l₂$ have the same length and corresponding elements satisfy the relation $R$), then $\text{Forall₂}\,R\,(\text{take}\,(\text{length}\,l₁)\,l)\,l₁$ holds (i.e., the first $\text{length}\,l₁$ elements of $l$ satisfy $R$ with the corresponding elements of $l₁$).

List.forall₂_drop_append theorem

 (l : List α) (l₁ : List β) (l₂ : List β) (h : Forall₂ R l (l₁ ++ l₂)) : Forall₂ R (List.drop (length l₁) l) l₂

Full source

theorem forall₂_drop_append (l : List α) (l₁ : List β) (l₂ : List β) (h : Forall₂ R l (l₁ ++ l₂)) :
    Forall₂ R (List.drop (length l₁) l) l₂ := by
  have h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)) :=
    forall₂_drop (length l₁) h
  rwa [drop_left] at h'

Element-wise Relation Preservation under Drop and Append Operation

Informal description

For any lists $l$ (of type $\alpha$), $l₁$ and $l₂$ (of type $\beta$), if the relation `Forall₂ R l (l₁ ++ l₂)` holds (meaning $l$ and the concatenation $l₁ ++ l₂$ have the same length and their corresponding elements satisfy $R$), then the relation `Forall₂ R` also holds between the list obtained by dropping the first $|l₁|$ elements from $l$ and the list $l₂$. In other words, $\text{drop}(|l₁|, l)$ and $l₂$ satisfy $R$ element-wise.

List.rel_mem theorem

(hr : BiUnique R) : (R ⇒ Forall₂ R ⇒ Iff) (· ∈ ·) (· ∈ ·)

Full source

theorem rel_mem (hr : BiUnique R) : (R ⇒ Forall₂ R ⇒ Iff) (· ∈ ·) (· ∈ ·)
  | a, b, _, [], [], Forall₂.nil => by simp only [not_mem_nil]
  | a, b, h, a' :: as, b' :: bs, Forall₂.cons h₁ h₂ => by
    simp only [mem_cons]
    exact rel_or (rel_eq hr h h₁) (rel_mem hr h h₂)

Preservation of Membership under Bi-unique Relations and List Pairwise Relations

Informal description

For any bi-unique relation $R$, the membership relation $\in$ is preserved under $R$ in the following sense: given elements $a$ and $b$ such that $R(a, b)$ holds, and lists $l_1$ and $l_2$ such that $\text{Forall}_2(R)(l_1, l_2)$ holds, then $a \in l_1$ if and only if $b \in l_2$.

List.rel_map theorem

: ((R ⇒ P) ⇒ Forall₂ R ⇒ Forall₂ P) map map

Full source

theorem rel_map : ((R ⇒ P) ⇒ Forall₂ R ⇒ Forall₂ P) map map
  | _, _, _, [], [], Forall₂.nil => Forall₂.nil
  | _, _, h, _ :: _, _ :: _, Forall₂.cons h₁ h₂ => Forall₂.cons (h h₁) (rel_map (@h) h₂)

Preservation of List Relation under Mapping

Informal description

For any binary relations $R : \alpha \to \beta \to \text{Prop}$ and $P : \gamma \to \delta \to \text{Prop}$, the `map` operation preserves the `Forall₂` relation. That is, if $f : \alpha \to \gamma$ and $g : \beta \to \delta$ satisfy $(R \Rightarrow P)(f, g)$, and if two lists $l_1 : \text{List } \alpha$ and $l_2 : \text{List } \beta$ satisfy $\text{Forall}_2 R l_1 l_2$, then the mapped lists $\text{map } f l_1$ and $\text{map } g l_2$ satisfy $\text{Forall}_2 P (\text{map } f l_1) (\text{map } g l_2)$.

List.rel_append theorem

: (Forall₂ R ⇒ Forall₂ R ⇒ Forall₂ R) (· ++ ·) (· ++ ·)

Full source

theorem rel_append : (Forall₂Forall₂ R ⇒ Forall₂ R ⇒ Forall₂ R) (· ++ ·) (· ++ ·)
  | [], [], _, _, _, hl => hl
  | _, _, Forall₂.cons h₁ h₂, _, _, hl => Forall₂.cons h₁ (rel_append h₂ hl)

Concatenation Preserves Pairwise Relation $\text{Forall}_2(R)$

Informal description

For any binary relation $R$, if two pairs of lists $(l_1, l_2)$ and $(l_1', l_2')$ satisfy $\text{Forall}_2(R)$ (i.e., they have the same length and corresponding elements are related by $R$), then their concatenations $(l_1 ++ l_1', l_2 ++ l_2')$ also satisfy $\text{Forall}_2(R)$.

List.rel_reverse theorem

: (Forall₂ R ⇒ Forall₂ R) reverse reverse

Full source

theorem rel_reverse : (Forall₂Forall₂ R ⇒ Forall₂ R) reverse reverse
  | [], [], Forall₂.nil => Forall₂.nil
  | _, _, Forall₂.cons h₁ h₂ => by
    simp only [reverse_cons]
    exact rel_append (rel_reverse h₂) (Forall₂.cons h₁ Forall₂.nil)

Reversal Preserves Pairwise Relation $\text{Forall}_2(R)$

Informal description

For any binary relation $R$, if two lists $l_1$ and $l_2$ satisfy $\text{Forall}_2(R)$ (i.e., they have the same length and corresponding elements are related by $R$), then their reversed versions $\text{reverse}(l_1)$ and $\text{reverse}(l_2)$ also satisfy $\text{Forall}_2(R)$.

List.forall₂_reverse_iff theorem

{l₁ l₂} : Forall₂ R (reverse l₁) (reverse l₂) ↔ Forall₂ R l₁ l₂

Full source

@[simp]
theorem forall₂_reverse_iff {l₁ l₂} : Forall₂Forall₂ R (reverse l₁) (reverse l₂) ↔ Forall₂ R l₁ l₂ :=
  Iff.intro
    (fun h => by
      rw [← reverse_reverse l₁, ← reverse_reverse l₂]
      exact rel_reverse h)
    fun h => rel_reverse h

Reversed Lists Preserve Pairwise Relation $\text{Forall}_2(R)$ if and only if Original Lists Do

Informal description

For any binary relation $R$ and two lists $l₁$ and $l₂$, the reversed lists $\text{reverse}(l₁)$ and $\text{reverse}(l₂)$ satisfy $\text{Forall}_2(R)$ (i.e., they have the same length and corresponding elements are related by $R$) if and only if the original lists $l₁$ and $l₂$ satisfy $\text{Forall}_2(R)$.

List.rel_flatten theorem

: (Forall₂ (Forall₂ R) ⇒ Forall₂ R) flatten flatten

Full source

theorem rel_flatten : (Forall₂Forall₂ (Forall₂ R) ⇒ Forall₂ R) flatten flatten
  | [], [], Forall₂.nil => Forall₂.nil
  | _, _, Forall₂.cons h₁ h₂ => rel_append h₁ (rel_flatten h₂)

Flattening Preserves Pairwise Relation $\text{Forall}_2(R)$

Informal description

For any binary relation $R$, if two lists of lists $L_1$ and $L_2$ satisfy $\text{Forall}_2(\text{Forall}_2(R))$ (i.e., they have the same length and corresponding sublists are pairwise related by $\text{Forall}_2(R)$), then their flattened versions $\text{flatten}(L_1)$ and $\text{flatten}(L_2)$ satisfy $\text{Forall}_2(R)$.

List.rel_flatMap theorem

: (Forall₂ R ⇒ (R ⇒ Forall₂ P) ⇒ Forall₂ P) (Function.swap List.flatMap) (Function.swap List.flatMap)

Full source

theorem rel_flatMap : (Forall₂Forall₂ R ⇒ (R ⇒ Forall₂ P) ⇒ Forall₂ P)
    (Function.swap List.flatMap) (Function.swap List.flatMap) :=
  fun _ _ h₁ _ _ h₂ => rel_flatten (rel_map (@h₂) h₁)

Preservation of Pairwise Relation under Flat Mapping

Informal description

For any binary relations $R : \alpha \to \beta \to \text{Prop}$ and $P : \gamma \to \delta \to \text{Prop}$, the `flatMap` operation preserves the `Forall₂` relation. Specifically, if two lists $l_1 : \text{List } \alpha$ and $l_2 : \text{List } \beta$ satisfy $\text{Forall}_2 R l_1 l_2$, and if for any $a \in \alpha$ and $b \in \beta$ with $R(a, b)$, the lists $f(a)$ and $g(b)$ satisfy $\text{Forall}_2 P (f(a)) (g(b))$, then the flattened mapped lists $\text{flatMap } f l_1$ and $\text{flatMap } g l_2$ satisfy $\text{Forall}_2 P (\text{flatMap } f l_1) (\text{flatMap } g l_2)$.

List.rel_foldl theorem

: ((P ⇒ R ⇒ P) ⇒ P ⇒ Forall₂ R ⇒ P) foldl foldl

Full source

theorem rel_foldl : ((P ⇒ R ⇒ P) ⇒ P ⇒ Forall₂ R ⇒ P) foldl foldl
  | _, _, _, _, _, h, _, _, Forall₂.nil => h
  | _, _, hfg, _, _, hxy, _, _, Forall₂.cons hab hs => rel_foldl (@hfg) (hfg hxy hab) hs

Preservation of Relation Under Left Fold for Lists with Corresponding Elements

Informal description

Given a binary relation $P \Rightarrow R \Rightarrow P$ (where $P$ is a predicate and $R$ is a relation), an initial predicate $P_0$, and two lists related by `Forall₂ R`, then the `foldl` operation preserves the relation $P$ when applied to both lists. In other words, if we have: 1. A relation $f : P \Rightarrow R \Rightarrow P$ (where $f$ transforms a predicate $P$ and an element related by $R$ into a new predicate $P$) 2. An initial predicate $p_0 : P$ 3. Two lists $l_1$ and $l_2$ such that `Forall₂ R l₁ l₂` (meaning they have the same length and corresponding elements are related by $R$) Then the result of folding $f$ over $l_1$ starting with $p_0$ is related to the result of folding $f$ over $l_2$ starting with $p_0$ by the predicate $P$.

List.rel_foldr theorem

: ((R ⇒ P ⇒ P) ⇒ P ⇒ Forall₂ R ⇒ P) foldr foldr

Full source

theorem rel_foldr : ((R ⇒ P ⇒ P) ⇒ P ⇒ Forall₂ R ⇒ P) foldr foldr
  | _, _, _, _, _, h, _, _, Forall₂.nil => h
  | _, _, hfg, _, _, hxy, _, _, Forall₂.cons hab hs => hfg hab (rel_foldr (@hfg) hxy hs)

Preservation of List Folding Under Relation $\text{Forall}_2 R$

Informal description

Given a binary relation $R : \alpha \to \beta \to \text{Prop}$ and a type $P$, the `foldr` operation on lists preserves the relation $\text{Forall}_2 R$ when the folding functions are related by $(R \Rightarrow P \Rightarrow P)$ and the initial accumulators are equal. More precisely, for any functions $f : \alpha \to P \to P$ and $g : \beta \to P \to P$ such that for all $a \in \alpha$, $b \in \beta$ where $R(a,b)$, we have $f(a) = g(b)$ as functions $P \to P$, and for any lists $l_1$ and $l_2$ where $\text{Forall}_2 R\ l_1\ l_2$ holds, we have $\text{foldr}\ f\ z\ l_1 = \text{foldr}\ g\ z\ l_2$ for any $z \in P$.

List.rel_filter theorem

 {p : α → Bool} {q : β → Bool} (hpq : (R ⇒ (· ↔ ·)) (fun x => p x) (fun x => q x)) :
  (Forall₂ R ⇒ Forall₂ R) (filter p) (filter q)

Full source

theorem rel_filter {p : α → Bool} {q : β → Bool}
    (hpq : (R ⇒ (· ↔ ·)) (fun x => p x) (fun x => q x)) :
    (Forall₂Forall₂ R ⇒ Forall₂ R) (filter p) (filter q)
  | _, _, Forall₂.nil => Forall₂.nil
  | a :: as, b :: bs, Forall₂.cons h₁ h₂ => by
    dsimp [LiftFun] at hpq
    by_cases h : p a
    · have : q b := by rwa [← hpq h₁]
      simp only [filter_cons_of_pos h, filter_cons_of_pos this, forall₂_cons, h₁, true_and,
        rel_filter hpq h₂]
    · have : ¬q b := by rwa [← hpq h₁]
      simp only [filter_cons_of_neg h, filter_cons_of_neg this, rel_filter hpq h₂]

Preservation of Forall₂ Relation Under Filtering with Related Predicates

Informal description

Let $R$ be a relation between elements of types $\alpha$ and $\beta$, and let $p : \alpha \to \text{Bool}$ and $q : \beta \to \text{Bool}$ be predicates such that for any $x \in \alpha$ and $y \in \beta$ with $R(x,y)$, we have $p(x) \leftrightarrow q(y)$. Then for any two lists $l_1$ of $\alpha$ and $l_2$ of $\beta$ satisfying $\text{Forall}_2(R)(l_1,l_2)$, the filtered lists $\text{filter}(p)(l_1)$ and $\text{filter}(q)(l_2)$ also satisfy $\text{Forall}_2(R)$.

List.rel_filterMap theorem

: ((R ⇒ Option.Rel P) ⇒ Forall₂ R ⇒ Forall₂ P) filterMap filterMap

Full source

theorem rel_filterMap : ((R ⇒ Option.Rel P) ⇒ Forall₂ R ⇒ Forall₂ P) filterMap filterMap
  | _, _, _, _, _, Forall₂.nil => Forall₂.nil
  | f, g, hfg, a :: as, b :: bs, Forall₂.cons h₁ h₂ => by
    rw [filterMap_cons, filterMap_cons]
    exact
      match f a, g b, hfg h₁ with
      | _, _, Option.Rel.none => rel_filterMap (@hfg) h₂
      | _, _, Option.Rel.some h => Forall₂.cons h (rel_filterMap (@hfg) h₂)

Preservation of Pairwise Relation Under Filtered Mapping

Informal description

Given a relation $R$ between elements of types $\alpha$ and $\beta$, and a relation $P$ between elements of types $\gamma$ and $\delta$, if two functions $f : \alpha \to \text{Option}\ \gamma$ and $g : \beta \to \text{Option}\ \delta$ satisfy the lifted relation $(R \Rightarrow \text{Option.Rel}\ P)$, then applying `filterMap` to lists $l_1$ and $l_2$ that satisfy $\text{Forall}_2\ R$ results in lists that satisfy $\text{Forall}_2\ P$. In other words, if $R$ relates corresponding elements of $l_1$ and $l_2$, and for each such pair $(a,b)$, either: 1. $f(a) = \text{none}$ and $g(b) = \text{none}$, or 2. $f(a) = \text{some}\ c$, $g(b) = \text{some}\ d$, and $P\ c\ d$ holds, then $\text{filterMap}\ f\ l_1$ and $\text{filterMap}\ g\ l_2$ have the same length and their corresponding elements satisfy $P$.

List.SublistForall₂ inductive

(R : α → β → Prop) : List α → List β → Prop

Full source

/-- Given a relation `R`, `sublist_forall₂ r l₁ l₂` indicates that there is a sublist of `l₂` such
  that `forall₂ r l₁ l₂`. -/
inductive SublistForall₂ (R : α → β → Prop) : List α → List β → Prop
  | nil {l} : SublistForall₂ R [] l
  | cons {a₁ a₂ l₁ l₂} : R a₁ a₂ → SublistForall₂ R l₁ l₂ → SublistForall₂ R (a₁ :: l₁) (a₂ :: l₂)
  | cons_right {a l₁ l₂} : SublistForall₂ R l₁ l₂ → SublistForall₂ R l₁ (a :: l₂)

Sublist relation with pairwise condition

Informal description

Given a relation $ R $ between elements of types $ \alpha $ and $ \beta $, the predicate `SublistForall₂ R l₁ l₂` holds if there exists a sublist $ l $ of $ l₂ $ such that `Forall₂ R l₁ l` is satisfied. Here, `Forall₂ R l₁ l` means that the lists $ l₁ $ and $ l $ have the same length and for every corresponding pair of elements $ (a, b) $ from $ l₁ $ and $ l $, the relation $ R a b $ holds.

List.sublistForall₂_iff theorem

{l₁ : List α} {l₂ : List β} : SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Full source

theorem sublistForall₂_iff {l₁ : List α} {l₂ : List β} :
    SublistForall₂SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂ := by
  constructor <;> intro h
  · induction h with
    | nil => exact ⟨nil, Forall₂.nil, nil_sublist _⟩
    | @cons a b l1 l2 rab _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
    | cons_right _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
  · obtain ⟨l, hl1, hl2⟩ := h
    revert l₁
    induction hl2 with
    | slnil =>
      intro l₁ hl1
      rw [forall₂_nil_right_iff.1 hl1]
      exact SublistForall₂.nil
    | cons _ _ ih => intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)
    | cons₂ _ _ ih =>
      intro l₁ hl1
      obtain - | ⟨hr, hl⟩ := hl1
      exact SublistForall₂.cons hr (ih hl)

Characterization of SublistForall₂ via Existence of Pointwise Related Sublist

Informal description

For any two lists `l₁` of type `α` and `l₂` of type `β`, and any relation `R` between elements of `α` and `β`, the predicate `SublistForall₂ R l₁ l₂` holds if and only if there exists a sublist `l` of `l₂` such that: 1. The lists `l₁` and `l` have the same length, and 2. For every corresponding pair of elements `(a, b)` from `l₁` and `l`, the relation `R a b` holds. In other words, `SublistForall₂ R l₁ l₂` is equivalent to the existence of a sublist `l` of `l₂` that is pointwise related to `l₁` via `R`.

List.SublistForall₂.is_refl instance

[IsRefl α Rₐ] : IsRefl (List α) (SublistForall₂ Rₐ)

Full source

instance SublistForall₂.is_refl [IsRefl α Rₐ] : IsRefl (List α) (SublistForall₂ Rₐ) :=
  ⟨fun l => sublistForall₂_iff.2 ⟨l, forall₂_refl l, Sublist.refl l⟩⟩

Reflexivity of SublistForall₂ Relation

Informal description

For any reflexive binary relation $R_\alpha$ on a type $\alpha$, the relation $\text{SublistForall}_2(R_\alpha)$ on lists of elements of $\alpha$ is also reflexive. That is, for any list $l$ of type $\alpha$, the relation $\text{SublistForall}_2(R_\alpha)(l, l)$ holds.

List.SublistForall₂.is_trans instance

[IsTrans α Rₐ] : IsTrans (List α) (SublistForall₂ Rₐ)

Full source

instance SublistForall₂.is_trans [IsTrans α Rₐ] : IsTrans (List α) (SublistForall₂ Rₐ) :=
  ⟨fun a b c => by
    revert a b
    induction c with
    | nil =>
      rintro _ _ h1 h2
      cases h2
      exact h1
    | cons _ _ ih =>
      rintro a b h1 h2
      obtain - | ⟨hbc, tbc⟩ | btc := h2
      · cases h1
        exact SublistForall₂.nil
      · obtain - | ⟨hab, tab⟩ | atb := h1
        · exact SublistForall₂.nil
        · exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)
        · exact SublistForall₂.cons_right (ih _ _ atb tbc)
      · exact SublistForall₂.cons_right (ih _ _ h1 btc)⟩

Transitivity of SublistForall₂ Relation

Informal description

For any transitive relation $R$ on a type $\alpha$, the relation `SublistForall₂ R` on lists of elements of $\alpha$ is also transitive. That is, for any three lists $l_1, l_2, l_3$ of type $\alpha$, if `SublistForall₂ R l₁ l₂` and `SublistForall₂ R l₂ l₃` hold, then `SublistForall₂ R l₁ l₃` also holds.

List.Sublist.sublistForall₂ theorem

{l₁ l₂ : List α} (h : l₁ <+ l₂) [IsRefl α Rₐ] : SublistForall₂ Rₐ l₁ l₂

Full source

theorem Sublist.sublistForall₂ {l₁ l₂ : List α} (h : l₁ <+ l₂) [IsRefl α Rₐ] :
    SublistForall₂ Rₐ l₁ l₂ :=
  sublistForall₂_iff.2 ⟨l₁, forall₂_refl l₁, h⟩

Sublist Implies Pointwise Related Sublist for Reflexive Relations

Informal description

For any reflexive binary relation $R$ on a type $\alpha$ and any two lists $l_1$ and $l_2$ of elements of $\alpha$, if $l_1$ is a sublist of $l_2$, then there exists a sublist $l$ of $l_2$ such that: 1. $l_1$ and $l$ have the same length, and 2. For every corresponding pair of elements $(a, b)$ from $l_1$ and $l$, the relation $R(a, b)$ holds.

List.tail_sublistForall₂_self theorem

[IsRefl α Rₐ] (l : List α) : SublistForall₂ Rₐ l.tail l

Full source

theorem tail_sublistForall₂_self [IsRefl α Rₐ] (l : List α) : SublistForall₂ Rₐ l.tail l :=
  l.tail_sublist.sublistForall₂

Tail Sublist Relation for Reflexive Binary Relations

Informal description

For any reflexive binary relation $R$ on a type $\alpha$ and any list $l$ of elements of $\alpha$, the tail of $l$ (i.e., the list obtained by removing the first element) is related to $l$ itself under the `SublistForall₂ R` relation. This means there exists a sublist $l'$ of $l$ such that: 1. $l.\text{tail}$ and $l'$ have the same length, and 2. For every corresponding pair of elements $(a, b)$ from $l.\text{tail}$ and $l'$, the relation $R(a, b)$ holds.

List.sublistForall₂_map_left_iff theorem

 {f : γ → α} {l₁ : List γ} {l₂ : List β} : SublistForall₂ R (map f l₁) l₂ ↔ SublistForall₂ (fun c b => R (f c) b) l₁ l₂

Full source

@[simp]
theorem sublistForall₂_map_left_iff {f : γ → α} {l₁ : List γ} {l₂ : List β} :
    SublistForall₂SublistForall₂ R (map f l₁) l₂ ↔ SublistForall₂ (fun c b => R (f c) b) l₁ l₂ := by
  simp [sublistForall₂_iff]

Equivalence of Mapped Sublist Relation: $R(f(l_1), l_2) \leftrightarrow R_f(l_1, l_2)$

Informal description

For any function $f : \gamma \to \alpha$, list $l_1$ of elements in $\gamma$, and list $l_2$ of elements in $\beta$, the following are equivalent: 1. There exists a sublist $l$ of $l_2$ such that the mapped list $f(l_1)$ and $l$ have the same length and satisfy $R$ pointwise (i.e., $R (f c) b$ holds for corresponding elements $c \in l_1$ and $b \in l$). 2. There exists a sublist $l$ of $l_2$ such that $l_1$ and $l$ have the same length and satisfy the relation $\lambda c b, R (f c) b$ pointwise.

List.sublistForall₂_map_right_iff theorem

 {f : γ → β} {l₁ : List α} {l₂ : List γ} : SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun a c => R a (f c)) l₁ l₂

Full source

@[simp]
theorem sublistForall₂_map_right_iff {f : γ → β} {l₁ : List α} {l₂ : List γ} :
    SublistForall₂SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun a c => R a (f c)) l₁ l₂ := by
  simp only [sublistForall₂_iff]
  constructor
  · rintro ⟨l1, h1, h2⟩
    obtain ⟨l', hl1, rfl⟩ := sublist_map_iff.mp h2
    use l'
    simpa [hl1] using h1
  · rintro ⟨l1, h1, h2⟩
    use l1.map f
    simp [h1, h2.map]

Equivalence of SublistForall₂ under Right Mapping

Informal description

For any function $f : \gamma \to \beta$, list $l_1$ of elements in $\alpha$, and list $l_2$ of elements in $\gamma$, the following are equivalent: 1. There exists a sublist $l$ of $f$ applied to $l_2$ (i.e., $\text{map}\, f\, l_2$) such that $\text{Forall}_2\, R\, l_1\, l$ holds. 2. There exists a sublist $l'$ of $l_2$ such that $\text{Forall}_2\, (R\, a\, (f\, c))\, l_1\, l'$ holds. In other words, the relation $\text{SublistForall}_2\, R\, l_1\, (\text{map}\, f\, l_2)$ is equivalent to $\text{SublistForall}_2\, (R\, a\, (f\, c))\, l_1\, l_2$.