Composition, transitivity, and antisymmetry of List.Forall₂

List.Forall₂ R relates lists of equal length pointwise. It composes pointwise (List.forall₂_comp_iff), so it inherits transitivity and antisymmetry from R, as List.SublistForall₂ does in Mathlib/Data/List/Forall2.lean; with R := (· ≤ ·) this is the pointwise order on lists of equal length, which the lexicographic order refines (List.Forall₂.le, List.Forall₂.lt_of_ne), as Pi.toLex_monotone and Pi.toLex_strictMono say of Pi.Lex; the pointwise witnesses of Phonology/Tone/Register.lean lift to the lexicographic order this way. [UPSTREAM] candidates for that file, beside List.SublistForall₂.is_refl and List.SublistForall₂.is_trans.

Main results

• List.forall₂_comp_iff: Forall₂ (R ∘r S) is the pointwise composite of Forall₂ R and Forall₂ S.
• List.Forall₂.trans, List.Forall₂.antisymm, and the Std.Refl, IsTrans, Std.Antisymm instances on Forall₂ R.
• List.Forall₂.le, List.Forall₂.lt_of_ne: lists ordered pointwise are ordered lexicographically.
• List.decidableForall₂: a Decidable (Forall₂ R l₁ l₂) instance that decide can evaluate.

Implementation notes

Batteries decides Forall₂ through List.all₂, whose body it stopped exposing to other modules in batteries#2006, so decide gets stuck on it. List.decidableForall₂ takes priority over that instance; remove it once Batteries exposes List.all₂ again.

theorem List.forall₂_comp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : α → β → Prop} {S : β → γ → Prop} {l₁ : List α} {l₃ : List γ} : Forall₂ (Relation.Comp R S) l₁ l₃ ↔ ∃ (l₂ : List β), Forall₂ R l₁ l₂ ∧ Forall₂ S l₂ l₃

Forall₂ for a composite relation is the pointwise composite of the two Forall₂s.

theorem List.Forall₂.trans {α : Type u_1} {R : α → α → Prop} [IsTrans α R] {l₁ l₂ l₃ : List α} (h₁ : Forall₂ R l₁ l₂) (h₂ : Forall₂ R l₂ l₃) : Forall₂ R l₁ l₃

theorem List.Forall₂.antisymm {α : Type u_1} {R : α → α → Prop} [Std.Antisymm R] {l₁ l₂ : List α} : Forall₂ R l₁ l₂ → Forall₂ R l₂ l₁ → l₁ = l₂

instance List.Forall₂.instRefl {α : Type u_1} {R : α → α → Prop} [Std.Refl R] : Std.Refl (Forall₂ R)

instance List.Forall₂.instIsTrans {α : Type u_1} {R : α → α → Prop} [IsTrans α R] : IsTrans (List α) (Forall₂ R)

instance List.Forall₂.instAntisymm {α : Type u_1} {R : α → α → Prop} [Std.Antisymm R] : Std.Antisymm (Forall₂ R)

Decidability

@[instance_reducible, instance 10000]

instance List.decidableForall₂ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [(a : α) → (b : β) → Decidable (R a b)] (l₁ : List α) (l₂ : List β) : Decidable (Forall₂ R l₁ l₂)

Forall₂ R decided by structural recursion on both lists, so that decide evaluates it outside this module.

Equations

• [].decidableForall₂ [] = isTrue ⋯
• [].decidableForall₂ (head :: tail) = isFalse ⋯
• (head :: tail).decidableForall₂ [] = isFalse ⋯
• (a :: l₁).decidableForall₂ (b :: l₂) = decidable_of_iff (R a b ∧ List.Forall₂ R l₁ l₂) ⋯

The lexicographic order refines the pointwise order

theorem List.Forall₂.le {α : Type u_1} [Preorder α] {l₁ l₂ : List α} (h : Forall₂ (fun (x1 x2 : α) => x1 ≤ x2) l₁ l₂) : l₁ ≤ l₂

Lists ordered pointwise are ordered lexicographically, the list form of Pi.toLex_monotone.

theorem List.Forall₂.lt_of_ne {α : Type u_1} [PartialOrder α] {l₁ l₂ : List α} (h : Forall₂ (fun (x1 x2 : α) => x1 ≤ x2) l₁ l₂) (hne : l₁ ≠ l₂) : l₁ < l₂

Distinct lists ordered pointwise are strictly ordered lexicographically, the list form of Pi.toLex_strictMono.