Mathlib.Data.List.Chain

List.Chain.iff theorem

{S : α → α → Prop} (H : ∀ a b, R a b ↔ S a b) {a : α} {l : List α} : Chain R a l ↔ Chain S a l

Full source

theorem Chain.iff {S : α → α → Prop} (H : ∀ a b, R a b ↔ S a b) {a : α} {l : List α} :
    ChainChain R a l ↔ Chain S a l :=
  ⟨Chain.imp fun a b => (H a b).1, Chain.imp fun a b => (H a b).2⟩

Equivalence of Chain Conditions Under Equivalent Relations

Informal description

Let $R$ and $S$ be two binary relations on a type $\alpha$ such that for all $a, b \in \alpha$, $R(a, b)$ holds if and only if $S(a, b)$ holds. Then for any starting element $a \in \alpha$ and any list $l$ of elements of $\alpha$, the chain condition `Chain R a l` holds if and only if `Chain S a l` holds. In other words, the chain property is preserved under equivalent relations.

List.Chain.iff_mem theorem

{a : α} {l : List α} : Chain R a l ↔ Chain (fun x y => x ∈ a :: l ∧ y ∈ l ∧ R x y) a l

Full source

theorem Chain.iff_mem {a : α} {l : List α} :
    ChainChain R a l ↔ Chain (fun x y => x ∈ a :: l ∧ y ∈ l ∧ R x y) a l :=
  ⟨fun p => by
    induction p with
    | nil => exact nil
    | @cons _ _ _ r _ IH =>
      constructor
      · exact ⟨mem_cons_self, mem_cons_self, r⟩
      · exact IH.imp fun a b ⟨am, bm, h⟩ => ⟨mem_cons_of_mem _ am, mem_cons_of_mem _ bm, h⟩,
    Chain.imp fun _ _ h => h.2.2⟩

Chain Equivalence via Membership-Restricted Relation

Informal description

For any relation $R$ on a type $\alpha$, an element $a \in \alpha$, and a list $l$ of elements of $\alpha$, the following are equivalent: 1. The list $l$ forms a chain starting at $a$ with respect to $R$ (i.e., $R$ holds between consecutive elements in $a::l$). 2. The list $l$ forms a chain starting at $a$ with respect to the restricted relation $\lambda x y. (x \in a::l) \land (y \in l) \land R(x,y)$.

List.chain_singleton theorem

{a b : α} : Chain R a [b] ↔ R a b

Full source

theorem chain_singleton {a b : α} : ChainChain R a [b] ↔ R a b := by
  simp only [chain_cons, Chain.nil, and_true]

Singleton Chain Condition: $R(a, b) \leftrightarrow \text{Chain}(R, a, [b])$

Informal description

For any binary relation $R$ on a type $\alpha$ and any elements $a, b \in \alpha$, the singleton list $[b]$ forms a chain starting at $a$ with respect to $R$ if and only if $R(a, b)$ holds.

List.chain_split theorem

{a b : α} {l₁ l₂ : List α} : Chain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂

Full source

theorem chain_split {a b : α} {l₁ l₂ : List α} :
    ChainChain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂ := by
  induction' l₁ with x l₁ IH generalizing a <;>
    simp only [*, nil_append, cons_append, Chain.nil, chain_cons, and_true, and_assoc]

Splitting a Chain at an Intermediate Element

Informal description

For any relation $R$ on a type $\alpha$, elements $a, b \in \alpha$, and lists $l₁, l₂$ of elements of $\alpha$, the following are equivalent: 1. The concatenated list $l₁ ++ b :: l₂$ forms a chain starting at $a$ with respect to $R$. 2. The list $l₁ ++ [b]$ forms a chain starting at $a$ with respect to $R$, and the list $l₂$ forms a chain starting at $b$ with respect to $R$.

List.chain_append_cons_cons theorem

 {a b c : α} {l₁ l₂ : List α} : Chain R a (l₁ ++ b :: c :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ R b c ∧ Chain R c l₂

Full source

@[simp]
theorem chain_append_cons_cons {a b c : α} {l₁ l₂ : List α} :
    ChainChain R a (l₁ ++ b :: c :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ R b c ∧ Chain R c l₂ := by
  rw [chain_split, chain_cons]

Chain Splitting at Two Consecutive Elements

Informal description

For any relation $R$ on a type $\alpha$, elements $a, b, c \in \alpha$, and lists $l₁, l₂$ of elements of $\alpha$, the following are equivalent: 1. The concatenated list $l₁ ++ b :: c :: l₂$ forms a chain starting at $a$ with respect to $R$. 2. The list $l₁ ++ [b]$ forms a chain starting at $a$ with respect to $R$, the relation $R(b, c)$ holds, and the list $l₂$ forms a chain starting at $c$ with respect to $R$.

List.chain_iff_forall₂ theorem

: ∀ {a : α} {l : List α}, Chain R a l ↔ l = [] ∨ Forall₂ R (a :: dropLast l) l

Full source

theorem chain_iff_forall₂ :
    ∀ {a : α} {l : List α}, ChainChain R a l ↔ l = [] ∨ Forall₂ R (a :: dropLast l) l
  | a, [] => by simp
  | a, b :: l => by
    by_cases h : l = [] <;>
    simp [@chain_iff_forall₂ b l, dropLast, *]

Characterization of Chains via Pairwise Relations

Informal description

For any relation $R$ on a type $\alpha$, an element $a \in \alpha$, and a list $l$ of elements of $\alpha$, the following are equivalent: 1. The list $l$ forms an $R$-chain starting at $a$ (i.e., consecutive elements in $a :: l$ are related by $R$). 2. Either $l$ is empty, or the relation $\text{Forall}_2 R$ holds between the lists $a :: \text{dropLast}(l)$ and $l$ (i.e., corresponding elements in these lists are related by $R$).

List.chain_append_singleton_iff_forall₂ theorem

: Chain R a (l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])

Full source

theorem chain_append_singleton_iff_forall₂ :
    ChainChain R a (l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b]) := by simp [chain_iff_forall₂]

Equivalence of Chain and Forall₂ for Appended Singleton Lists

Informal description

For a relation $R$ on a type $\alpha$, an element $a \in \alpha$, a list $l$ of elements of $\alpha$, and an element $b \in \alpha$, the following are equivalent: 1. The list $l \mathbin{+\!\!+} [b]$ forms an $R$-chain starting at $a$ (i.e., consecutive elements in $a :: l \mathbin{+\!\!+} [b]$ are related by $R$). 2. The relation $\text{Forall}_2 R$ holds between the lists $a :: l$ and $l \mathbin{+\!\!+} [b]$ (i.e., corresponding elements in these lists are related by $R$).

List.chain_map theorem

(f : β → α) {b : β} {l : List β} : Chain R (f b) (map f l) ↔ Chain (fun a b : β => R (f a) (f b)) b l

Full source

theorem chain_map (f : β → α) {b : β} {l : List β} :
    ChainChain R (f b) (map f l) ↔ Chain (fun a b : β => R (f a) (f b)) b l := by
  induction l generalizing b <;> simp only [map, Chain.nil, chain_cons, *]

Mapping Preserves Chain Relation: $f$ maps a $S$-chain to an $R$-chain if $S(a,b) \Leftrightarrow R(f(a), f(b))$

Informal description

Let $R$ be a relation on a type $\alpha$, $f : \beta \to \alpha$ a function, $b \in \beta$, and $l$ a list of elements of $\beta$. Then the following are equivalent: 1. The list obtained by applying $f$ to each element of $b::l$ forms an $R$-chain starting at $f(b)$. 2. The original list $l$ forms a chain with respect to the relation $S(a,b) := R(f(a), f(b))$ starting at $b$.

List.chain_of_chain_map theorem

 {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, S (f a) (f b) → R a b) {a : α} {l : List α}
  (p : Chain S (f a) (map f l)) : Chain R a l

Full source

theorem chain_of_chain_map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, S (f a) (f b) → R a b)
    {a : α} {l : List α} (p : Chain S (f a) (map f l)) : Chain R a l :=
  ((chain_map f).1 p).imp H

Chain Preservation Under Reverse Mapping: If $S(f(a), f(b)) \Rightarrow R(a, b)$, then $S$-chains lift to $R$-chains

Informal description

Let $R$ be a relation on a type $\alpha$, $S$ a relation on a type $\beta$, and $f : \alpha \to \beta$ a function such that for any $a, b \in \alpha$, if $S(f(a), f(b))$ holds then $R(a, b)$ holds. For any $a \in \alpha$ and list $l$ of elements of $\alpha$, if the mapped list $\text{map}\,f\,l$ forms an $S$-chain starting at $f(a)$, then $l$ forms an $R$-chain starting at $a$.

List.chain_map_of_chain theorem

 {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b)) {a : α} {l : List α} (p : Chain R a l) :
  Chain S (f a) (map f l)

Full source

theorem chain_map_of_chain {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
    {a : α} {l : List α} (p : Chain R a l) : Chain S (f a) (map f l) :=
  (chain_map f).2 <| p.imp H

Mapping Preserves Chain Relation: $R$-chain implies $S$-chain under $f$

Informal description

Let $R$ be a relation on a type $\alpha$, $S$ a relation on a type $\beta$, and $f : \alpha \to \beta$ a function such that for any $a, b \in \alpha$, $R(a, b)$ implies $S(f(a), f(b))$. Given a list $l$ of elements of $\alpha$ that forms an $R$-chain starting at $a$, then the list obtained by applying $f$ to each element of $a::l$ forms an $S$-chain starting at $f(a)$.

List.chain_pmap_of_chain theorem

 {S : β → β → Prop} {p : α → Prop} {f : ∀ a, p a → β} (H : ∀ a b ha hb, R a b → S (f a ha) (f b hb)) {a : α}
  {l : List α} (hl₁ : Chain R a l) (ha : p a) (hl₂ : ∀ a ∈ l, p a) : Chain S (f a ha) (List.pmap f l hl₂)

Full source

theorem chain_pmap_of_chain {S : β → β → Prop} {p : α → Prop} {f : ∀ a, p a → β}
    (H : ∀ a b ha hb, R a b → S (f a ha) (f b hb)) {a : α} {l : List α} (hl₁ : Chain R a l)
    (ha : p a) (hl₂ : ∀ a ∈ l, p a) : Chain S (f a ha) (List.pmap f l hl₂) := by
  induction' l with lh lt l_ih generalizing a
  · simp
  · simp [H _ _ _ _ (rel_of_chain_cons hl₁), l_ih (chain_of_chain_cons hl₁)]

Preservation of Chain Property under Partial Mapping

Informal description

Let $R$ be a relation on type $\alpha$ and $S$ a relation on type $\beta$. Given a predicate $p$ on $\alpha$ and a function $f$ that maps any $a \in \alpha$ satisfying $p(a)$ to $\beta$, if: 1. For any $a, b \in \alpha$ with proofs $ha : p(a)$ and $hb : p(b)$, $R(a, b)$ implies $S(f(a, ha), f(b, hb))$; 2. We have a chain $hl₁ : \text{Chain } R\ a\ l$ starting at $a$ with relation $R$; 3. The element $a$ satisfies $p$ (witnessed by $ha$); 4. All elements in $l$ satisfy $p$ (witnessed by $hl₂$); then the mapped list $\text{pmap}\ f\ l\ hl₂$ forms a chain starting at $f(a, ha)$ with relation $S$.

List.chain_of_chain_pmap theorem

 {S : β → β → Prop} {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (hl₁ : ∀ a ∈ l, p a) {a : α} (ha : p a)
  (hl₂ : Chain S (f a ha) (List.pmap f l hl₁)) (H : ∀ a b ha hb, S (f a ha) (f b hb) → R a b) : Chain R a l

Full source

theorem chain_of_chain_pmap {S : β → β → Prop} {p : α → Prop} (f : ∀ a, p a → β) {l : List α}
    (hl₁ : ∀ a ∈ l, p a) {a : α} (ha : p a) (hl₂ : Chain S (f a ha) (List.pmap f l hl₁))
    (H : ∀ a b ha hb, S (f a ha) (f b hb) → R a b) : Chain R a l := by
  induction' l with lh lt l_ih generalizing a
  · simp
  · simp [H _ _ _ _ (rel_of_chain_cons hl₂), l_ih _ _ (chain_of_chain_cons hl₂)]

Reconstruction of Relation Chain from Mapped Chain via Partial Mapping

Informal description

Let $R$ be a relation on type $\alpha$ and $S$ be a relation on type $\beta$. Given: 1. A predicate $p$ on $\alpha$ 2. A function $f : \forall a \in \alpha, p(a) \to \beta$ 3. For all $a \in l$ (where $l$ is a list of elements of $\alpha$), $p(a)$ holds 4. For some $a \in \alpha$, $p(a)$ holds 5. The list formed by applying $f$ to $a$ and elements of $l$ (via `pmap`) forms an $S$-chain starting at $f(a)$ 6. For any $a, b \in \alpha$ with $p(a)$ and $p(b)$, if $S(f(a), f(b))$ holds then $R(a,b)$ holds Then the original list $l$ forms an $R$-chain starting at $a$.

List.Chain.pairwise theorem

[IsTrans α R] : ∀ {a : α} {l : List α}, Chain R a l → Pairwise R (a :: l)

Full source

protected theorem Chain.pairwise [IsTrans α R] :
    ∀ {a : α} {l : List α}, Chain R a l → Pairwise R (a :: l)
  | _, [], Chain.nil => pairwise_singleton _ _
  | a, _, @Chain.cons _ _ _ b l h hb =>
    hb.pairwise.cons
      (by
        simp only [mem_cons, forall_eq_or_imp, h, true_and]
        exact fun c hc => _root_.trans h (rel_of_pairwise_cons hb.pairwise hc))

Chain Implies Pairwise Relation for Transitive Relations

Informal description

For any transitive relation $R$ on a type $\alpha$, any element $a \in \alpha$, and any list $l$ of elements of $\alpha$, if the list forms a chain starting at $a$ with respect to $R$ (i.e., $\text{Chain } R\ a\ l$), then the list $a :: l$ is pairwise related by $R$ (i.e., $\text{Pairwise } R\ (a :: l)$).

List.chain_iff_pairwise theorem

[IsTrans α R] {a : α} {l : List α} : Chain R a l ↔ Pairwise R (a :: l)

Full source

theorem chain_iff_pairwise [IsTrans α R] {a : α} {l : List α} : ChainChain R a l ↔ Pairwise R (a :: l) :=
  ⟨Chain.pairwise, Pairwise.chain⟩

Equivalence Between Chain and Pairwise Relation for Transitive Relations

Informal description

For any transitive relation $R$ on a type $\alpha$, an element $a \in \alpha$, and a list $l$ of elements of $\alpha$, the following are equivalent: 1. The list forms a chain starting at $a$ with respect to $R$ (i.e., $\text{Chain } R\ a\ l$) 2. The list $a :: l$ is pairwise related by $R$ (i.e., $\text{Pairwise } R\ (a :: l)$)

List.Chain.sublist theorem

[IsTrans α R] (hl : l₂.Chain R a) (h : l₁ <+ l₂) : l₁.Chain R a

Full source

protected theorem Chain.sublist [IsTrans α R] (hl : l₂.Chain R a) (h : l₁ <+ l₂) :
    l₁.Chain R a := by
  rw [chain_iff_pairwise] at hl ⊢
  exact hl.sublist (h.cons_cons a)

Sublist Preserves Chain Property for Transitive Relations

Informal description

Let $R$ be a transitive relation on a type $\alpha$, and let $a \in \alpha$. If a list $l_2$ forms a chain starting at $a$ with respect to $R$, and $l_1$ is a sublist of $l_2$, then $l_1$ also forms a chain starting at $a$ with respect to $R$.

List.Chain.rel theorem

[IsTrans α R] (hl : l.Chain R a) (hb : b ∈ l) : R a b

Full source

protected theorem Chain.rel [IsTrans α R] (hl : l.Chain R a) (hb : b ∈ l) : R a b := by
  rw [chain_iff_pairwise] at hl
  exact rel_of_pairwise_cons hl hb

Transitivity of Chain Relation: $R(a, b)$ for All $b$ in Chain

Informal description

For any transitive relation $R$ on a type $\alpha$, if a list $l$ forms a chain starting at $a$ with respect to $R$ (i.e., $\text{Chain } R\ a\ l$), then for every element $b$ in $l$, the relation $R(a, b)$ holds.

List.chain_iff_get theorem

 {R} :
  ∀ {a : α} {l : List α},
    Chain R a l ↔
      (∀ h : 0 < length l, R a (get l ⟨0, h⟩)) ∧
        ∀ (i : ℕ) (h : i < l.length - 1), R (get l ⟨i, by omega⟩) (get l ⟨i + 1, by omega⟩)

Full source

theorem chain_iff_get {R} : ∀ {a : α} {l : List α}, ChainChain R a l ↔
    (∀ h : 0 < length l, R a (get l ⟨0, h⟩)) ∧
      ∀ (i : ℕ) (h : i < l.length - 1),
        R (get l ⟨i, by omega⟩) (get l ⟨i+1, by omega⟩)
  | a, [] => iff_of_true (by simp) ⟨fun h => by simp at h, fun _ h => by simp at h⟩
  | a, b :: t => by
    rw [chain_cons, @chain_iff_get _ _ t]
    constructor
    · rintro ⟨R, ⟨h0, h⟩⟩
      constructor
      · intro _
        exact R
      intro i w
      rcases i with - | i
      · apply h0
      · exact h i (by simp only [length_cons] at w; omega)
    rintro ⟨h0, h⟩; constructor
    · apply h0
      simp
    constructor
    · apply h 0
    intro i w
    exact h (i+1) (by simp only [length_cons]; omega)

Characterization of Chains via Element-wise Relations

Informal description

For any relation $R$ on a type $\alpha$, an element $a \in \alpha$, and a list $l$ of elements of $\alpha$, the list $l$ forms a chain starting at $a$ with respect to $R$ if and only if: 1. For any proof $h$ that $0 < \text{length}(l)$, the relation $R(a, l_0)$ holds (where $l_0$ is the first element of $l$), and 2. For every natural number $i$ and proof $h$ that $i < \text{length}(l) - 1$, the relation $R(l_i, l_{i+1})$ holds (where $l_i$ and $l_{i+1}$ are consecutive elements in $l$).

List.chain_replicate_of_rel theorem

(n : ℕ) {a : α} (h : r a a) : Chain r a (replicate n a)

Full source

theorem chain_replicate_of_rel (n : ℕ) {a : α} (h : r a a) : Chain r a (replicate n a) :=
  match n with
  | 0 => Chain.nil
  | n + 1 => Chain.cons h (chain_replicate_of_rel n h)

Replicated List Forms Chain under Reflexive Relation

Informal description

For any natural number $n$ and any element $a$ of type $\alpha$, if the relation $r$ satisfies $r(a, a)$, then the list consisting of $n$ copies of $a$ forms a chain starting at $a$ with respect to $r$.

List.chain_eq_iff_eq_replicate theorem

{a : α} {l : List α} : Chain (· = ·) a l ↔ l = replicate l.length a

Full source

theorem chain_eq_iff_eq_replicate {a : α} {l : List α} :
    ChainChain (· = ·) a l ↔ l = replicate l.length a :=
  match l with
  | [] => by simp
  | b :: l => by
    rw [chain_cons]
    simp +contextual [eq_comm, replicate_succ, chain_eq_iff_eq_replicate]

Characterization of Constant Chains via Replication

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the list $l$ forms a chain where each element is equal to the previous one (starting from $a$) if and only if $l$ is equal to the list obtained by replicating $a$ exactly $\text{length}(l)$ times.

List.Chain'.imp theorem

{S : α → α → Prop} (H : ∀ a b, R a b → S a b) {l : List α} (p : Chain' R l) : Chain' S l

Full source

theorem Chain'.imp {S : α → α → Prop} (H : ∀ a b, R a b → S a b) {l : List α} (p : Chain' R l) :
    Chain' S l := by cases l <;> [trivial; exact Chain.imp H p]

Chain Preservation Under Relation Implication

Informal description

Let $R$ and $S$ be two binary relations on a type $\alpha$ such that for all $a, b \in \alpha$, $R(a, b)$ implies $S(a, b)$. If a list $l$ is a chain with respect to $R$ (i.e., for every pair of consecutive elements $x_i, x_{i+1}$ in $l$, $R(x_i, x_{i+1})$ holds), then $l$ is also a chain with respect to $S$.

List.Chain'.iff theorem

{S : α → α → Prop} (H : ∀ a b, R a b ↔ S a b) {l : List α} : Chain' R l ↔ Chain' S l

Full source

theorem Chain'.iff {S : α → α → Prop} (H : ∀ a b, R a b ↔ S a b) {l : List α} :
    Chain'Chain' R l ↔ Chain' S l :=
  ⟨Chain'.imp fun a b => (H a b).1, Chain'.imp fun a b => (H a b).2⟩

Equivalence of Chain Definitions Under Relation Equivalence

Informal description

Let $R$ and $S$ be two binary relations on a type $\alpha$ such that for all $a, b \in \alpha$, $R(a, b)$ holds if and only if $S(a, b)$ holds. Then, for any list $l$ of elements of type $\alpha$, $l$ is a chain with respect to $R$ if and only if $l$ is a chain with respect to $S$.

List.Chain'.iff_mem theorem

: ∀ {l : List α}, Chain' R l ↔ Chain' (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l

Full source

theorem Chain'.iff_mem : ∀ {l : List α}, Chain'Chain' R l ↔ Chain' (fun x y => x ∈ l ∧ y ∈ l ∧ R x y) l
  | [] => Iff.rfl
  | _ :: _ =>
    ⟨fun h => (Chain.iff_mem.1 h).imp fun _ _ ⟨h₁, h₂, h₃⟩ => ⟨h₁, mem_cons.2 (Or.inr h₂), h₃⟩,
      Chain'.imp fun _ _ h => h.2.2⟩

Chain Equivalence via Membership-Restricted Relation (List Version)

Informal description

For any binary relation $R$ on a type $\alpha$ and any list $l$ of elements of $\alpha$, the following are equivalent: 1. The list $l$ is a chain with respect to $R$ (i.e., $R$ holds between every pair of consecutive elements in $l$). 2. The list $l$ is a chain with respect to the restricted relation $\lambda x y. (x \in l) \land (y \in l) \land R(x,y)$.

List.chain'_nil theorem

: Chain' R []

Full source

@[simp]
theorem chain'_nil : Chain' R [] :=
  trivial

Empty List is a Chain for Any Relation

Informal description

For any binary relation $R$ on a type $\alpha$, the empty list is a chain with respect to $R$.

List.chain'_singleton theorem

(a : α) : Chain' R [a]

Full source

@[simp]
theorem chain'_singleton (a : α) : Chain' R [a] :=
  Chain.nil

Singleton List is a Chain

Informal description

For any relation $R$ on a type $\alpha$ and any element $a \in \alpha$, the singleton list $[a]$ is a chain with respect to $R$.

List.chain'_cons theorem

{x y l} : Chain' R (x :: y :: l) ↔ R x y ∧ Chain' R (y :: l)

Full source

@[simp]
theorem chain'_cons {x y l} : Chain'Chain' R (x :: y :: l) ↔ R x y ∧ Chain' R (y :: l) :=
  chain_cons

Chain condition for a list with at least two elements

Informal description

For any relation $R$ on a type $\alpha$ and elements $x, y \in \alpha$ and list $l$ of elements of $\alpha$, the list $x :: y :: l$ is a chain with respect to $R$ (written as $\text{Chain'}\,R\,(x :: y :: l)$) if and only if $R\,x\,y$ holds and the list $y :: l$ is also a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(y :: l)$ holds).

List.chain'_isInfix theorem

: ∀ l : List α, Chain' (fun x y => [x, y] <:+: l) l

Full source

theorem chain'_isInfix : ∀ l : List α, Chain' (fun x y => [x, y][x, y] <:+: l) l
  | [] => chain'_nil
  | [_] => chain'_singleton _
  | a :: b :: l =>
    chain'_cons.2
      ⟨⟨[], l, by simp⟩, (chain'_isInfix (b :: l)).imp fun _ _ h => h.trans ⟨[a], [], by simp⟩⟩

List is a Chain Under Its Own Infix Relation

Informal description

For any list $l$ of elements of type $\alpha$, the list $l$ is a chain with respect to the relation $\lambda x y, [x, y] \text{ is an infix of } l$. That is, for every pair of consecutive elements $x_i, x_{i+1}$ in $l$, the sublist $[x_i, x_{i+1}]$ appears as a contiguous subsequence somewhere in $l$.

List.chain'_split theorem

{a : α} : ∀ {l₁ l₂ : List α}, Chain' R (l₁ ++ a :: l₂) ↔ Chain' R (l₁ ++ [a]) ∧ Chain' R (a :: l₂)

Full source

theorem chain'_split {a : α} :
    ∀ {l₁ l₂ : List α}, Chain'Chain' R (l₁ ++ a :: l₂) ↔ Chain' R (l₁ ++ [a]) ∧ Chain' R (a :: l₂)
  | [], _ => (and_iff_right (chain'_singleton a)).symm
  | _ :: _, _ => chain_split

Splitting a Chain at an Intermediate Element (Generalized Version)

Informal description

For any relation $R$ on a type $\alpha$, any element $a \in \alpha$, and any lists $l₁, l₂$ of elements of $\alpha$, the following are equivalent: 1. The concatenated list $l₁ ++ a :: l₂$ forms a chain with respect to $R$. 2. The list $l₁ ++ [a]$ forms a chain with respect to $R$, and the list $a :: l₂$ forms a chain with respect to $R$.

List.chain'_append_cons_cons theorem

 {b c : α} {l₁ l₂ : List α} : Chain' R (l₁ ++ b :: c :: l₂) ↔ Chain' R (l₁ ++ [b]) ∧ R b c ∧ Chain' R (c :: l₂)

Full source

@[simp]
theorem chain'_append_cons_cons {b c : α} {l₁ l₂ : List α} :
    Chain'Chain' R (l₁ ++ b :: c :: l₂) ↔ Chain' R (l₁ ++ [b]) ∧ R b c ∧ Chain' R (c :: l₂) := by
  rw [chain'_split, chain'_cons]

Chain Splitting at Two Consecutive Elements

Informal description

For any relation $R$ on a type $\alpha$, elements $b, c \in \alpha$, and lists $l₁, l₂$ of elements of $\alpha$, the following are equivalent: 1. The concatenated list $l₁ ++ b :: c :: l₂$ forms a chain with respect to $R$. 2. The list $l₁ ++ [b]$ forms a chain with respect to $R$, the relation $R\,b\,c$ holds, and the list $c :: l₂$ forms a chain with respect to $R$.

List.chain'_iff_forall_rel_of_append_cons_cons theorem

{l : List α} : Chain' R l ↔ ∀ ⦃a b l₁ l₂⦄, l = l₁ ++ a :: b :: l₂ → R a b

Full source

theorem chain'_iff_forall_rel_of_append_cons_cons {l : List α} :
    Chain'Chain' R l ↔ ∀ ⦃a b l₁ l₂⦄, l = l₁ ++ a :: b :: l₂ → R a b := by
  refine ⟨fun h _ _ _ _ eq => (chain'_append_cons_cons.mp (eq ▸ h)).2.1, ?_⟩
  induction l with
  | nil => exact fun _ ↦ chain'_nil
  | cons head tail ih =>
    match tail with
    | nil => exact fun _ ↦ chain'_singleton head
    | cons head' tail =>
      refine fun h ↦ chain'_cons.mpr ⟨h (nil_append _).symm, ih fun ⦃a b l₁ l₂⦄ eq => ?_⟩
      apply h
      rw [eq, cons_append]

Chain Characterization via All Consecutive Pairs

Informal description

For any relation $R$ on a type $\alpha$ and any list $l$ of elements of $\alpha$, the following are equivalent: 1. The list $l$ is a chain with respect to $R$ (i.e., consecutive elements satisfy $R$). 2. For any elements $a, b \in \alpha$ and any sublists $l₁, l₂$ such that $l = l₁ ++ a :: b :: l₂$, the relation $R(a, b)$ holds.

List.chain'_map theorem

(f : β → α) {l : List β} : Chain' R (map f l) ↔ Chain' (fun a b : β => R (f a) (f b)) l

Full source

theorem chain'_map (f : β → α) {l : List β} :
    Chain'Chain' R (map f l) ↔ Chain' (fun a b : β => R (f a) (f b)) l := by
  cases l <;> [rfl; exact chain_map _]

Mapping Preserves Chain Relation: $f$ maps an $S$-chain to an $R$-chain if $S(a,b) \Leftrightarrow R(f(a), f(b))$

Informal description

Let $R$ be a relation on a type $\alpha$, $f : \beta \to \alpha$ a function, and $l$ a list of elements of $\beta$. Then the following are equivalent: 1. The list obtained by applying $f$ to each element of $l$ forms an $R$-chain (i.e., consecutive elements satisfy $R$). 2. The original list $l$ forms a chain with respect to the relation $S(a,b) := R(f(a), f(b))$.

List.chain'_of_chain'_map theorem

 {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, S (f a) (f b) → R a b) {l : List α} (p : Chain' S (map f l)) :
  Chain' R l

Full source

theorem chain'_of_chain'_map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, S (f a) (f b) → R a b)
    {l : List α} (p : Chain' S (map f l)) : Chain' R l :=
  ((chain'_map f).1 p).imp H

Chain Lifting via Function Mapping: $S$-chain on $f(l)$ implies $R$-chain on $l$ under implication condition

Informal description

Let $R$ be a relation on a type $\alpha$, $S$ a relation on a type $\beta$, and $f : \alpha \to \beta$ a function such that for all $a, b \in \alpha$, $S(f(a), f(b))$ implies $R(a, b)$. If the list obtained by applying $f$ to each element of a list $l$ in $\alpha$ forms an $S$-chain, then $l$ itself forms an $R$-chain.

List.chain'_map_of_chain' theorem

 {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b)) {l : List α} (p : Chain' R l) :
  Chain' S (map f l)

Full source

theorem chain'_map_of_chain' {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
    {l : List α} (p : Chain' R l) : Chain' S (map f l) :=
  (chain'_map f).2 <| p.imp H

Mapping Preserves Chain Relation: $R$-chain on $l$ implies $S$-chain on $f(l)$ under implication condition

Informal description

Let $R$ be a relation on a type $\alpha$, $S$ a relation on a type $\beta$, and $f : \alpha \to \beta$ a function such that for all $a, b \in \alpha$, $R(a, b)$ implies $S(f(a), f(b))$. If a list $l$ of elements of $\alpha$ forms an $R$-chain (i.e., consecutive elements satisfy $R$), then the list obtained by applying $f$ to each element of $l$ forms an $S$-chain.

List.Pairwise.chain' theorem

: ∀ {l : List α}, Pairwise R l → Chain' R l

Full source

theorem Pairwise.chain' : ∀ {l : List α}, Pairwise R l → Chain' R l
  | [], _ => trivial
  | _ :: _, h => Pairwise.chain h

Pairwise Relation Implies Chain Formation

Informal description

For any list `l` of elements of type `α`, if the elements are pairwise related by the relation `R` (i.e., `Pairwise R l` holds), then the list forms a chain with respect to `R` (i.e., `Chain' R l` holds).

List.chain'_iff_pairwise theorem

[IsTrans α R] : ∀ {l : List α}, Chain' R l ↔ Pairwise R l

Full source

theorem chain'_iff_pairwise [IsTrans α R] : ∀ {l : List α}, Chain'Chain' R l ↔ Pairwise R l
  | [] => (iff_true_intro Pairwise.nil).symm
  | _ :: _ => chain_iff_pairwise

Equivalence Between Chain and Pairwise Relation for Transitive Relations

Informal description

For any transitive relation $R$ on a type $\alpha$ and any list $l$ of elements of $\alpha$, the following are equivalent: 1. The list $l$ forms a chain with respect to $R$ (i.e., consecutive elements satisfy $R$) 2. The elements of $l$ are pairwise related by $R$

List.Chain'.sublist theorem

[IsTrans α R] (hl : l₂.Chain' R) (h : l₁ <+ l₂) : l₁.Chain' R

Full source

protected theorem Chain'.sublist [IsTrans α R] (hl : l₂.Chain' R) (h : l₁ <+ l₂) : l₁.Chain' R := by
  rw [chain'_iff_pairwise] at hl ⊢
  exact hl.sublist h

Sublist Preservation of Chain Condition for Transitive Relations

Informal description

Let $R$ be a transitive relation on a type $\alpha$. For any lists $l₁$ and $l₂$ of elements of $\alpha$, if $l₂$ forms a chain with respect to $R$ (i.e., consecutive elements satisfy $R$) and $l₁$ is a sublist of $l₂$, then $l₁$ also forms a chain with respect to $R$.

List.Chain'.cons theorem

{x y l} (h₁ : R x y) (h₂ : Chain' R (y :: l)) : Chain' R (x :: y :: l)

Full source

theorem Chain'.cons {x y l} (h₁ : R x y) (h₂ : Chain' R (y :: l)) : Chain' R (x :: y :: l) :=
  chain'_cons.2 ⟨h₁, h₂⟩

Cons Extension Preserves Chain Condition

Informal description

For any relation $R$ on a type $\alpha$, elements $x, y \in \alpha$, and a list $l$ of elements of $\alpha$, if $R(x, y)$ holds and the list $y :: l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(y :: l)$), then the list $x :: y :: l$ also forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(x :: y :: l)$).

List.Chain'.tail theorem

: ∀ {l}, Chain' R l → Chain' R l.tail

Full source

theorem Chain'.tail : ∀ {l}, Chain' R l → Chain' R l.tail
  | [], _ => trivial
  | [_], _ => trivial
  | _ :: _ :: _, h => (chain'_cons.mp h).right

Tail of a Chain is a Chain

Informal description

For any relation $R$ on a type $\alpha$ and any list $l$ of elements of $\alpha$, if $l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds), then the tail of $l$ (denoted $l.\text{tail}$) also forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(l.\text{tail})$ holds).

List.Chain'.rel_head theorem

{x y l} (h : Chain' R (x :: y :: l)) : R x y

Full source

theorem Chain'.rel_head {x y l} (h : Chain' R (x :: y :: l)) : R x y :=
  rel_of_chain_cons h

Relation Holds for First Two Elements in a Chain

Informal description

For any relation $R$ on a type $\alpha$ and elements $x, y \in \alpha$ and a list $l$ of elements of $\alpha$, if the list $x :: y :: l$ forms a chain with respect to $R$ (i.e., `Chain' R (x :: y :: l)` holds), then the relation $R(x, y)$ holds between the first two elements $x$ and $y$.

List.Chain'.rel_head? theorem

{x l} (h : Chain' R (x :: l)) ⦃y⦄ (hy : y ∈ head? l) : R x y

Full source

theorem Chain'.rel_head? {x l} (h : Chain' R (x :: l)) ⦃y⦄ (hy : y ∈ head? l) : R x y := by
  rw [← cons_head?_tail hy] at h
  exact h.rel_head

Relation Holds Between First Element and Head of Tail in a Chain

Informal description

For any relation $R$ on a type $\alpha$, element $x \in \alpha$, and list $l$ of elements of $\alpha$, if the list $x :: l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(x :: l)$ holds), and if $y$ is an element of the optional head of $l$ (i.e., $y \in \text{head?}(l)$), then the relation $R(x, y)$ holds between $x$ and $y$.

List.Chain'.cons' theorem

{x} : ∀ {l : List α}, Chain' R l → (∀ y ∈ l.head?, R x y) → Chain' R (x :: l)

Full source

theorem Chain'.cons' {x} : ∀ {l : List α}, Chain' R l → (∀ y ∈ l.head?, R x y) → Chain' R (x :: l)
  | [], _, _ => chain'_singleton x
  | _ :: _, hl, H => hl.cons <| H _ rfl

Chain Extension via Head Condition

Informal description

For any relation $R$ on a type $\alpha$, element $x \in \alpha$, and list $l$ of elements of $\alpha$, if $l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds), and for every element $y$ in the optional head of $l$ (i.e., $y \in \text{head?}(l)$) the relation $R(x, y)$ holds, then the extended list $x :: l$ also forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(x :: l)$ holds).

List.chain'_cons' theorem

{x l} : Chain' R (x :: l) ↔ (∀ y ∈ head? l, R x y) ∧ Chain' R l

Full source

theorem chain'_cons' {x l} : Chain'Chain' R (x :: l) ↔ (∀ y ∈ head? l, R x y) ∧ Chain' R l :=
  ⟨fun h => ⟨h.rel_head?, h.tail⟩, fun ⟨h₁, h₂⟩ => h₂.cons' h₁⟩

Characterization of Chain Formation via Head Condition and Tail Chain

Informal description

For any relation $R$ on a type $\alpha$, element $x \in \alpha$, and list $l$ of elements of $\alpha$, the list $x :: l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(x :: l)$ holds) if and only if: 1. For every element $y$ in the optional head of $l$ (i.e., $y \in \text{head?}(l)$), the relation $R(x, y)$ holds, and 2. The list $l$ itself forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds).

List.chain'_append theorem

 : ∀ {l₁ l₂ : List α}, Chain' R (l₁ ++ l₂) ↔ Chain' R l₁ ∧ Chain' R l₂ ∧ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y

Full source

theorem chain'_append :
    ∀ {l₁ l₂ : List α},
      Chain'Chain' R (l₁ ++ l₂) ↔ Chain' R l₁ ∧ Chain' R l₂ ∧ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y
  | [], l => by simp
  | [a], l => by simp [chain'_cons', and_comm]
  | a :: b :: l₁, l₂ => by
    rw [cons_append, cons_append, chain'_cons, chain'_cons, ← cons_append, chain'_append, and_assoc]
    simp

Concatenation of Chains Condition

Informal description

For any relation $R$ on a type $\alpha$ and lists $l₁, l₂$ of elements of $\alpha$, the concatenated list $l₁ ++ l₂$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(l₁ ++ l₂)$ holds) if and only if: 1. $l₁$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l₁$ holds), 2. $l₂$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l₂$ holds), and 3. For every element $x$ in the last element of $l₁$ (if it exists) and every element $y$ in the first element of $l₂$ (if it exists), the relation $R(x, y)$ holds.

List.Chain'.append theorem

 (h₁ : Chain' R l₁) (h₂ : Chain' R l₂) (h : ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y) : Chain' R (l₁ ++ l₂)

Full source

theorem Chain'.append (h₁ : Chain' R l₁) (h₂ : Chain' R l₂)
    (h : ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y) : Chain' R (l₁ ++ l₂) :=
  chain'_append.2 ⟨h₁, h₂, h⟩

Concatenation of Chains under Relation $R$

Informal description

Let $R$ be a relation on a type $\alpha$, and let $l_1$ and $l_2$ be lists of elements of $\alpha$. If: 1. $l_1$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l_1$ holds), 2. $l_2$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l_2$ holds), and 3. For every element $x$ in the last element of $l_1$ (if it exists) and every element $y$ in the first element of $l_2$ (if it exists), the relation $R(x, y)$ holds, then the concatenated list $l_1 ++ l_2$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(l_1 ++ l_2)$ holds).

List.Chain'.left_of_append theorem

(h : Chain' R (l₁ ++ l₂)) : Chain' R l₁

Full source

theorem Chain'.left_of_append (h : Chain' R (l₁ ++ l₂)) : Chain' R l₁ :=
  (chain'_append.1 h).1

Left Subchain Preservation under Concatenation

Informal description

For any relation $R$ on a type $\alpha$ and lists $l₁, l₂$ of elements of $\alpha$, if the concatenated list $l₁ ++ l₂$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(l₁ ++ l₂)$ holds), then $l₁$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l₁$ holds).

List.Chain'.right_of_append theorem

(h : Chain' R (l₁ ++ l₂)) : Chain' R l₂

Full source

theorem Chain'.right_of_append (h : Chain' R (l₁ ++ l₂)) : Chain' R l₂ :=
  (chain'_append.1 h).2.1

Right Subchain Preservation under Concatenation

Informal description

For any relation $R$ on a type $\alpha$ and lists $l₁, l₂$ of elements of $\alpha$, if the concatenated list $l₁ ++ l₂$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(l₁ ++ l₂)$ holds), then $l₂$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l₂$ holds).

List.Chain'.infix theorem

(h : Chain' R l) (h' : l₁ <:+: l) : Chain' R l₁

Full source

theorem Chain'.infix (h : Chain' R l) (h' : l₁ <:+: l) : Chain' R l₁ := by
  rcases h' with ⟨l₂, l₃, rfl⟩
  exact h.left_of_append.right_of_append

Infix Subchain Preservation under Chain Relation

Informal description

For any relation $R$ on a type $\alpha$ and lists $l, l₁$ of elements of $\alpha$, if $l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds) and $l₁$ is an infix of $l$ (i.e., $l₁$ appears as a contiguous sublist within $l$), then $l₁$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l₁$ holds).

List.Chain'.suffix theorem

(h : Chain' R l) (h' : l₁ <:+ l) : Chain' R l₁

Full source

theorem Chain'.suffix (h : Chain' R l) (h' : l₁ <:+ l) : Chain' R l₁ :=
  h.infix h'.isInfix

Suffix Subchain Preservation under Chain Relation

Informal description

For any relation $R$ on a type $\alpha$ and lists $l, l₁$ of elements of $\alpha$, if $l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds) and $l₁$ is a suffix of $l$ (i.e., $l₁$ appears at the end of $l$), then $l₁$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l₁$ holds).

List.Chain'.prefix theorem

(h : Chain' R l) (h' : l₁ <+: l) : Chain' R l₁

Full source

theorem Chain'.prefix (h : Chain' R l) (h' : l₁ <+: l) : Chain' R l₁ :=
  h.infix h'.isInfix

Prefix Subchain Preservation under Chain Relation

Informal description

For any relation $R$ on a type $\alpha$ and lists $l, l₁$ of elements of $\alpha$, if $l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds) and $l₁$ is a prefix of $l$ (i.e., $l₁$ appears at the beginning of $l$), then $l₁$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l₁$ holds).

List.Chain'.drop theorem

(h : Chain' R l) (n : ℕ) : Chain' R (drop n l)

Full source

theorem Chain'.drop (h : Chain' R l) (n : ℕ) : Chain' R (drop n l) :=
  h.suffix (drop_suffix _ _)

Preservation of Chain Relation Under Dropping Elements

Informal description

For any relation $R$ on a type $\alpha$ and a list $l$ of elements of $\alpha$, if $l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds), then for any natural number $n$, the list obtained by dropping the first $n$ elements of $l$ (denoted $\text{drop}\,n\,l$) also forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(\text{drop}\,n\,l)$ holds).

List.Chain'.init theorem

(h : Chain' R l) : Chain' R l.dropLast

Full source

theorem Chain'.init (h : Chain' R l) : Chain' R l.dropLast :=
  h.prefix l.dropLast_prefix

Chain Preservation Under Last Element Removal

Informal description

For any relation $R$ on a type $\alpha$ and a list $l$ of elements of $\alpha$, if $l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds), then the list obtained by removing the last element of $l$ (denoted $l\text{.dropLast}$) also forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(l\text{.dropLast})$ holds).

List.Chain'.take theorem

(h : Chain' R l) (n : ℕ) : Chain' R (take n l)

Full source

theorem Chain'.take (h : Chain' R l) (n : ℕ) : Chain' R (take n l) :=
  h.prefix (take_prefix _ _)

Prefix of Chain is Chain

Informal description

For any relation $R$ on a type $\alpha$ and a list $l$ of elements of $\alpha$, if $l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds), then for any natural number $n$, the first $n$ elements of $l$ (i.e., $\text{take}\,n\,l$) also form a chain with respect to $R$.

List.chain'_pair theorem

{x y} : Chain' R [x, y] ↔ R x y

Full source

theorem chain'_pair {x y} : Chain'Chain' R [x, y] ↔ R x y := by
  simp only [chain'_singleton, chain'_cons, and_true]

Pair Chain Condition: $\text{Chain}'\, R\, [x, y] \leftrightarrow R\, x\, y$

Informal description

For any elements $x$ and $y$, the list $[x, y]$ forms a chain with respect to relation $R$ (i.e., $\text{Chain}'\, R\, [x, y]$) if and only if $R\, x\, y$ holds.

List.Chain'.imp_head theorem

{x y} (h : ∀ {z}, R x z → R y z) {l} (hl : Chain' R (x :: l)) : Chain' R (y :: l)

Full source

theorem Chain'.imp_head {x y} (h : ∀ {z}, R x z → R y z) {l} (hl : Chain' R (x :: l)) :
    Chain' R (y :: l) :=
  hl.tail.cons' fun _ hz => h <| hl.rel_head? hz

Chain Preservation Under Head Relation Implication

Informal description

For any relation $R$ on a type $\alpha$ and elements $x, y \in \alpha$, if for all $z \in \alpha$ the implication $R(x, z) \to R(y, z)$ holds, and if the list $x :: l$ forms a chain with respect to $R$, then the list $y :: l$ also forms a chain with respect to $R$.

List.chain'_reverse theorem

: ∀ {l}, Chain' R (reverse l) ↔ Chain' (flip R) l

Full source

theorem chain'_reverse : ∀ {l}, Chain'Chain' R (reverse l) ↔ Chain' (flip R) l
  | [] => Iff.rfl
  | [a] => by simp only [chain'_singleton, reverse_singleton]
  | a :: b :: l => by
    rw [chain'_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      chain'_split, ← reverse_cons, @chain'_reverse (b :: l), and_comm, chain'_pair, flip]

Reversed List Chain Condition: $\text{Chain'}\,R\,(\text{reverse}(l)) \leftrightarrow \text{Chain'}\,(\text{flip}\,R)\,l$

Informal description

For any relation $R$ on a type $\alpha$ and any list $l$ of elements of $\alpha$, the reversed list $\text{reverse}(l)$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(\text{reverse}(l))$) if and only if the original list $l$ forms a chain with respect to the flipped relation $\text{flip}\,R$ (i.e., $\text{Chain'}\,(\text{flip}\,R)\,l$).

List.chain'_iff_get theorem

 {R} : ∀ {l : List α}, Chain' R l ↔ ∀ (i : ℕ) (h : i < length l - 1), R (get l ⟨i, by omega⟩) (get l ⟨i + 1, by omega⟩)

Full source

theorem chain'_iff_get {R} : ∀ {l : List α}, Chain'Chain' R l ↔
    ∀ (i : ℕ) (h : i < length l - 1),
      R (get l ⟨i, by omega⟩) (get l ⟨i + 1, by omega⟩)
  | [] => iff_of_true (by simp) (fun _ h => by simp at h)
  | [a] => iff_of_true (by simp) (fun _ h => by simp at h)
  | a :: b :: t => by
    rw [← and_forall_add_one, chain'_cons, chain'_iff_get]
    simp

Characterization of Chains via Element-wise Relation Condition

Informal description

For any relation $R$ on a type $\alpha$ and any list $l$ of elements of $\alpha$, the list $l$ is a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds) if and only if for every index $i$ such that $i < \text{length}\,l - 1$, the relation $R$ holds between the $i$-th element of $l$ and the $(i+1)$-th element of $l$.

List.Chain'.append_overlap theorem

 {l₁ l₂ l₃ : List α} (h₁ : Chain' R (l₁ ++ l₂)) (h₂ : Chain' R (l₂ ++ l₃)) (hn : l₂ ≠ []) : Chain' R (l₁ ++ l₂ ++ l₃)

Full source

/-- If `l₁ l₂` and `l₃` are lists and `l₁ ++ l₂` and `l₂ ++ l₃` both satisfy
  `Chain' R`, then so does `l₁ ++ l₂ ++ l₃` provided `l₂ ≠ []` -/
theorem Chain'.append_overlap {l₁ l₂ l₃ : List α} (h₁ : Chain' R (l₁ ++ l₂))
    (h₂ : Chain' R (l₂ ++ l₃)) (hn : l₂ ≠ []) : Chain' R (l₁ ++ l₂ ++ l₃) :=
  h₁.append h₂.right_of_append <| by
    simpa only [getLast?_append_of_ne_nil _ hn] using (chain'_append.1 h₂).2.2

Chain Preservation under Overlapping Concatenation: $\text{Chain'}\,R\,(l_1 ++ l_2 ++ l_3)$ from $\text{Chain'}\,R\,(l_1 ++ l_2)$ and $\text{Chain'}\,R\,(l_2 ++ l_3)$ with $l_2 \neq []$

Informal description

Let $R$ be a relation on a type $\alpha$, and let $l_1$, $l_2$, $l_3$ be lists of elements of $\alpha$ such that $l_2$ is non-empty. If both concatenated lists $l_1 ++ l_2$ and $l_2 ++ l_3$ form chains with respect to $R$ (i.e., $\text{Chain'}\,R\,(l_1 ++ l_2)$ and $\text{Chain'}\,R\,(l_2 ++ l_3)$ hold), then the concatenated list $l_1 ++ l_2 ++ l_3$ also forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(l_1 ++ l_2 ++ l_3)$ holds).

List.chain'_flatten theorem

 :
  ∀ {L : List (List α)},
    [] ∉ L →
      (Chain' R L.flatten ↔ (∀ l ∈ L, Chain' R l) ∧ L.Chain' (fun l₁ l₂ => ∀ᵉ (x ∈ l₁.getLast?) (y ∈ l₂.head?), R x y))

Full source

lemma chain'_flatten : ∀ {L : List (List α)}, [][] ∉ L →
    (Chain'Chain' R L.flatten ↔ (∀ l ∈ L, Chain' R l) ∧
    L.Chain' (fun l₁ l₂ => ∀ᵉ (x ∈ l₁.getLast?) (y ∈ l₂.head?), R x y))
| [], _ => by simp
| [l], _ => by simp [flatten]
| (l₁ :: l₂ :: L), hL => by
    rw [mem_cons, not_or, ← Ne] at hL
    rw [flatten, chain'_append, chain'_flatten hL.2, forall_mem_cons, chain'_cons]
    rw [mem_cons, not_or, ← Ne] at hL
    simp only [forall_mem_cons, and_assoc, flatten, head?_append_of_ne_nil _ hL.2.1.symm]
    exact Iff.rfl.and (Iff.rfl.and <| Iff.rfl.and and_comm)

Flattened List Chain Condition for Non-Empty Sublists

Informal description

For a relation $R$ on a type $\alpha$ and a list of lists $L$ of elements of $\alpha$ where none of the sublists is empty, the flattened list $\text{flatten}\,L$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,(\text{flatten}\,L)$ holds) if and only if: 1. Every sublist $l \in L$ is a chain with respect to $R$ (i.e., $\forall l \in L, \text{Chain'}\,R\,l$), and 2. The list $L$ itself forms a chain with respect to the relation that for any consecutive sublists $l₁, l₂$ in $L$, the relation $R(x, y)$ holds for every $x$ in the last element of $l₁$ and every $y$ in the first element of $l₂$.

List.chain'_attachWith theorem

 {l : List α} {p : α → Prop} (h : ∀ x ∈ l, p x) {r : { a // p a } → { a // p a } → Prop} :
  (l.attachWith p h).Chain' r ↔ l.Chain' fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩

Full source

theorem chain'_attachWith {l : List α} {p : α → Prop} (h : ∀ x ∈ l, p x)
    {r : {a // p a} → {a // p a} → Prop} :
    (l.attachWith p h).Chain' r ↔ l.Chain' fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩ := by
  induction l with
  | nil => rfl
  | cons a l IH =>
    rw [attachWith_cons, chain'_cons', chain'_cons', IH, and_congr_left]
    simp_rw [head?_attachWith]
    intros
    constructor <;>
    intro hc b (hb : _ = _)
    · simp_rw [hb, Option.pbind_some] at hc
      have hb' := h b (mem_cons_of_mem a (mem_of_mem_head? hb))
      exact ⟨h a mem_cons_self, hb', hc ⟨b, hb'⟩ rfl⟩
    · cases l <;> aesop

Equivalence of Chain Conditions for Attached List and Original List with Predicate

Informal description

For a list $l$ of elements of type $\alpha$ and a predicate $p$ on $\alpha$ such that every element in $l$ satisfies $p$ (i.e., $\forall x \in l, p(x)$), and for a relation $r$ on the subtype $\{a \in \alpha \mid p(a)\}$, the following equivalence holds: The list $l.\text{attachWith}\,p\,h$ (where $h$ is the proof that all elements satisfy $p$) forms a chain with respect to $r$ if and only if the original list $l$ forms a chain with respect to the relation $\lambda a b, \exists (ha : p(a)) (hb : p(b)), r(\langle a, ha \rangle, \langle b, hb \rangle)$.

List.chain'_attach theorem

 {l : List α} {r : { a // a ∈ l } → { a // a ∈ l } → Prop} :
  l.attach.Chain' r ↔ l.Chain' fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩

Full source

theorem chain'_attach {l : List α} {r : {a // a ∈ l} → {a // a ∈ l} → Prop} :
    l.attach.Chain' r ↔ l.Chain' fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩ :=
  chain'_attachWith fun _ ↦ id

Equivalence of Chain Conditions for Attached List and Original List

Informal description

For a list $l$ of elements of type $\alpha$ and a relation $r$ on the subtype $\{a \in \alpha \mid a \in l\}$, the attached list $l.\text{attach}$ forms a chain with respect to $r$ if and only if the original list $l$ forms a chain with respect to the relation $\lambda a b, \exists (ha : a \in l) (hb : b \in l), r(\langle a, ha \rangle, \langle b, hb \rangle)$.

List.exists_chain_of_relationReflTransGen theorem

(h : Relation.ReflTransGen r a b) : ∃ l, Chain r a l ∧ getLast (a :: l) (cons_ne_nil _ _) = b

Full source

/-- If `a` and `b` are related by the reflexive transitive closure of `r`, then there is an
`r`-chain starting from `a` and ending on `b`.
The converse of `relationReflTransGen_of_exists_chain`.
-/
theorem exists_chain_of_relationReflTransGen (h : Relation.ReflTransGen r a b) :
    ∃ l, Chain r a l ∧ getLast (a :: l) (cons_ne_nil _ _) = b := by
  refine Relation.ReflTransGen.head_induction_on h ?_ ?_
  · exact ⟨[], Chain.nil, rfl⟩
  · intro c d e _ ih
    obtain ⟨l, hl₁, hl₂⟩ := ih
    refine ⟨d :: l, Chain.cons e hl₁, ?_⟩
    rwa [getLast_cons_cons]

Existence of Chain from Reflexive Transitive Closure

Informal description

Let $r$ be a relation on a type $\alpha$, and let $a, b \in \alpha$ be such that $b$ is in the reflexive transitive closure of $r$ starting from $a$. Then there exists a list $l$ of elements of $\alpha$ such that: 1. The list $[a] \mathbin{+\!\!+} l$ forms an $r$-chain starting at $a$, and 2. The last element of $[a] \mathbin{+\!\!+} l$ is $b$. In other words, if $a$ can reach $b$ via a finite sequence of $r$-related steps (including the reflexive case where $a = b$), then there is an explicit chain of elements connected by $r$ from $a$ to $b$.

List.Chain.induction theorem

 (p : α → Prop) (l : List α) (h : Chain r a l) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) : ∀ i ∈ l, p i

Full source

/-- Given a chain from `a` to `b`, and a predicate true at `a`, if `r x y → p x → p y` then
the predicate is true everywhere in the chain.
That is, we can propagate the predicate down the chain.
-/
theorem Chain.induction (p : α → Prop) (l : List α) (h : Chain r a l)
    (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) : ∀ i ∈ l, p i := by
  induction h with
  | nil => simp
  | @cons a b t hab _ h_ind =>
    simp only [mem_cons, forall_eq_or_imp]
    exact ⟨carries hab initial, h_ind (carries hab initial)⟩

Induction Principle for Chain Propagation

Informal description

Let $r$ be a relation on a type $\alpha$, and let $[a_2, \ldots, a_n]$ be a list of elements of $\alpha$ forming a chain starting at $a_1$ with respect to $r$ (i.e., $r a_1 a_2$, $r a_2 a_3$, $\ldots$, $r a_{n-1} a_n$ hold). Given a predicate $p : \alpha \to \mathrm{Prop}$ that holds at $a_1$ and satisfies the propagation property that for any $x, y \in \alpha$, if $r x y$ and $p x$ hold, then $p y$ holds, then $p$ holds for every element in the list $[a_2, \ldots, a_n]$.

List.Chain'.induction theorem

 (p : α → Prop) (l : List α) (h : Chain' r l) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y)
  (initial : (lne : l ≠ []) → p (l.head lne)) : ∀ i ∈ l, p i

Full source

/-- A version of `List.Chain.induction` for `List.Chain'`
-/
theorem Chain'.induction (p : α → Prop) (l : List α) (h : Chain' r l)
    (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : (lne : l ≠ []) → p (l.head lne)) :
    ∀ i ∈ l, p i := by
  unfold Chain' at h
  split at h
  · simp
  · simp_all only [ne_eq, not_false_eq_true, head_cons, true_implies, mem_cons, forall_eq_or_imp,
      true_and, reduceCtorEq]
    exact h.induction p _ carries initial

Induction Principle for Nonempty Chain Propagation

Informal description

Let $r$ be a relation on a type $\alpha$, and let $[a_1, \ldots, a_n]$ be a nonempty list of elements of $\alpha$ forming a chain with respect to $r$ (i.e., $r a_1 a_2$, $r a_2 a_3$, $\ldots$, $r a_{n-1} a_n$ hold). Given a predicate $p : \alpha \to \mathrm{Prop}$ that holds at the head of the list (when the list is nonempty) and satisfies the propagation property that for any $x, y \in \alpha$, if $r x y$ and $p x$ hold, then $p y$ holds, then $p$ holds for every element in the list $[a_1, \ldots, a_n]$.

List.Chain.backwards_induction theorem

 (p : α → Prop) (l : List α) (h : Chain r a l) (hb : getLast (a :: l) (cons_ne_nil _ _) = b)
  (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) : ∀ i ∈ a :: l, p i

Full source

/-- Given a chain from `a` to `b`, and a predicate true at `b`, if `r x y → p y → p x` then
the predicate is true everywhere in the chain and at `a`.
That is, we can propagate the predicate up the chain.
-/
theorem Chain.backwards_induction (p : α → Prop) (l : List α) (h : Chain r a l)
    (hb : getLast (a :: l) (cons_ne_nil _ _) = b) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x)
    (final : p b) : ∀ i ∈ a :: l, p i := by
  have : Chain' (flip (flip r)) (a :: l) := by simpa [Chain']
  replace this := chain'_reverse.mpr this
  simp_rw +singlePass [← List.mem_reverse]
  apply this.induction _ _ (fun _ _ h ↦ carries h)
  simpa only [ne_eq, reverse_eq_nil_iff, not_false_eq_true, head_reverse, forall_true_left, hb,
    reduceCtorEq]

Backward Induction Principle for Chain Propagation

Informal description

Let $r$ be a relation on a type $\alpha$, and let $[a_2, \ldots, a_n]$ be a list forming a chain starting at $a_1$ with respect to $r$ (i.e., $r a_1 a_2$, $r a_2 a_3$, $\ldots$, $r a_{n-1} a_n$ hold). Let $b$ be the last element of the chain $a_1 :: [a_2, \ldots, a_n]$. Given a predicate $p : \alpha \to \mathrm{Prop}$ that holds at $b$ and satisfies the backward propagation property that for any $x, y \in \alpha$, if $r x y$ and $p y$ hold, then $p x$ holds, then $p$ holds for every element in the chain $a_1 :: [a_2, \ldots, a_n]$.

List.Chain.backwards_induction_head theorem

 (p : α → Prop) (l : List α) (h : Chain r a l) (hb : getLast (a :: l) (cons_ne_nil _ _) = b)
  (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) : p a

Full source

/-- Given a chain from `a` to `b`, and a predicate true at `b`, if `r x y → p y → p x` then
the predicate is true at `a`.
That is, we can propagate the predicate all the way up the chain.
-/
@[elab_as_elim]
theorem Chain.backwards_induction_head (p : α → Prop) (l : List α) (h : Chain r a l)
    (hb : getLast (a :: l) (cons_ne_nil _ _) = b) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x)
    (final : p b) : p a :=
  (Chain.backwards_induction p l h hb carries final) _ mem_cons_self

Backward Induction on Chain Head: $p(a_1)$ from $p(b)$ via Relation $r$

Informal description

Let $r$ be a relation on a type $\alpha$, and let $[a_2, \ldots, a_n]$ be a list forming a chain starting at $a_1$ with respect to $r$ (i.e., $r a_1 a_2$, $r a_2 a_3$, $\ldots$, $r a_{n-1} a_n$ hold). Let $b$ be the last element of the chain $a_1 :: [a_2, \ldots, a_n]$. Given a predicate $p : \alpha \to \mathrm{Prop}$ that holds at $b$ and satisfies the backward propagation property that for any $x, y \in \alpha$, if $r x y$ and $p y$ hold, then $p x$ holds, then $p$ holds at the head element $a_1$ of the chain.

List.relationReflTransGen_of_exists_chain theorem

(l : List α) (hl₁ : Chain r a l) (hl₂ : getLast (a :: l) (cons_ne_nil _ _) = b) : Relation.ReflTransGen r a b

Full source

/--
If there is an `r`-chain starting from `a` and ending at `b`, then `a` and `b` are related by the
reflexive transitive closure of `r`. The converse of `exists_chain_of_relationReflTransGen`.
-/
theorem relationReflTransGen_of_exists_chain (l : List α) (hl₁ : Chain r a l)
    (hl₂ : getLast (a :: l) (cons_ne_nil _ _) = b) : Relation.ReflTransGen r a b :=
  Chain.backwards_induction_head _ l hl₁ hl₂ (fun _ _ => Relation.ReflTransGen.head)
    Relation.ReflTransGen.refl

Chain Implication for Reflexive Transitive Closure: $\text{Chain}\, r\, a_1\, [a_2, \ldots, a_n]$ implies $\text{ReflTransGen}\, r\, a_1\, b$ where $b$ is the last element

Informal description

Let $r$ be a relation on a type $\alpha$, and let $[a_2, \ldots, a_n]$ be a list forming a chain starting at $a_1$ with respect to $r$ (i.e., $r a_1 a_2$, $r a_2 a_3$, $\ldots$, $r a_{n-1} a_n$ hold). If $b$ is the last element of the chain $a_1 :: [a_2, \ldots, a_n]$, then $a_1$ and $b$ are related by the reflexive transitive closure of $r$, denoted $\text{ReflTransGen}\, r\, a_1\, b$.

List.Chain'.cons_of_le theorem

 [LinearOrder α] {a : α} {as m : List α} (ha : List.Chain' (· > ·) (a :: as)) (hm : List.Chain' (· > ·) m)
  (hmas : m ≤ as) : List.Chain' (· > ·) (a :: m)

Full source

theorem Chain'.cons_of_le [LinearOrder α] {a : α} {as m : List α}
    (ha : List.Chain' (· > ·) (a :: as)) (hm : List.Chain' (· > ·) m) (hmas : m ≤ as) :
    List.Chain' (· > ·) (a :: m) := by
  cases m with
  | nil => simp only [List.chain'_singleton]
  | cons b bs =>
    apply hm.cons
    cases as with
    | nil =>
      simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas
      exact (List.not_lt_nil _ hmas).elim
    | cons a' as =>
      rw [List.chain'_cons] at ha
      refine gt_of_gt_of_ge ha.1 ?_
      rw [le_iff_lt_or_eq] at hmas
      rcases hmas with hmas | hmas
      · by_contra! hh
        rw [← not_le] at hmas
        apply hmas
        apply le_of_lt
        exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel hh)
      · simp_all only [List.cons.injEq, le_refl]

Lexicographic Order Preserves Strictly Decreasing Chains: $a :: m$ is decreasing when $a :: as$ and $m$ are decreasing and $m \leq as$

Informal description

Let $\alpha$ be a linearly ordered type, and let $a$ be an element of $\alpha$. Suppose we have two lists $as$ and $m$ of elements of $\alpha$ such that: 1. The list $a :: as$ forms a strictly decreasing chain (i.e., $\text{Chain'}\,(>)\,(a :: as)$ holds), 2. The list $m$ forms a strictly decreasing chain (i.e., $\text{Chain'}\,(>)\,m$ holds), and 3. The list $m$ is lexicographically less than or equal to $as$ (i.e., $m \leq as$ in the lexicographic order). Then the list $a :: m$ also forms a strictly decreasing chain (i.e., $\text{Chain'}\,(>)\,(a :: m)$ holds).

List.Chain'.chain theorem

 {α : Type*} {R : α → α → Prop} {l : List α} {v : α} (hl : l.Chain' R) (hv : (lne : l ≠ []) → R v (l.head lne)) :
  l.Chain R v

Full source

lemma Chain'.chain {α : Type*} {R : α → α → Prop} {l : List α} {v : α}
    (hl : l.Chain' R) (hv : (lne : l ≠ []) → R v (l.head lne)) : l.Chain R v := by
  rw [List.chain_iff_get]
  constructor
  · intro h
    rw [List.get_mk_zero]
    apply hv
  · exact List.chain'_iff_get.mp hl

Extending a Chain with a New Head Element

Informal description

For any type $\alpha$ with a relation $R : \alpha \to \alpha \to Prop$, a list $l$ of elements of $\alpha$, and an element $v \in \alpha$, if: 1. $l$ forms a chain with respect to $R$ (i.e., $\text{Chain'}\,R\,l$ holds), and 2. For any proof that $l$ is non-empty, $R(v, \text{head}\,l)$ holds (where $\text{head}\,l$ is the first element of $l$), then the list $l$ forms a chain starting at $v$ with respect to $R$ (i.e., $\text{Chain}\,R\,v\,l$ holds).

List.Chain'.iterate_eq_of_apply_eq theorem

 {α : Type*} {f : α → α} {l : List α} (hl : l.Chain' (fun x y ↦ f x = y)) (i : ℕ) (hi : i < l.length) :
  f^[i] l[0] = l[i]

Full source

lemma Chain'.iterate_eq_of_apply_eq {α : Type*} {f : α → α} {l : List α}
    (hl : l.Chain' (fun x y ↦ f x = y)) (i : ℕ) (hi : i < l.length) :
    f^[i] l[0] = l[i] := by
  induction' i with i h
  · rfl
  · rw [Function.iterate_succ', Function.comp_apply, h (by omega)]
    rw [List.chain'_iff_get] at hl
    apply hl
    omega

Iteration Equals Chain Elements: $f^{[i]}(l[0]) = l[i]$ for Function-Generated Chains

Informal description

Let $\alpha$ be a type, $f : \alpha \to \alpha$ a function, and $l$ a list of elements of $\alpha$. If $l$ forms a chain with respect to the relation $\lambda x y, f x = y$ (i.e., each element after the first is obtained by applying $f$ to the previous element), then for any natural number $i$ such that $i < \text{length}(l)$, the $i$-th iterate of $f$ applied to the first element of $l$ equals the $i$-th element of $l$, i.e., $f^{[i]}(l[0]) = l[i]$.

List.chain'_replicate_of_rel theorem

(n : ℕ) {a : α} (h : r a a) : Chain' r (replicate n a)

Full source

theorem chain'_replicate_of_rel (n : ℕ) {a : α} (h : r a a) : Chain' r (replicate n a) :=
  match n with
  | 0 => chain'_nil
  | n + 1 => chain_replicate_of_rel n h

Replicated List Forms Chain under Reflexive Relation

Informal description

For any natural number $n$ and any element $a$ of type $\alpha$, if the relation $r$ satisfies $r(a, a)$, then the list consisting of $n$ copies of $a$ forms a chain with respect to $r$.

List.chain'_eq_iff_eq_replicate theorem

{l : List α} : Chain' (· = ·) l ↔ ∀ a ∈ l.head?, l = replicate l.length a

Full source

theorem chain'_eq_iff_eq_replicate {l : List α} :
    Chain'Chain' (· = ·) l ↔ ∀ a ∈ l.head?, l = replicate l.length a :=
  match l with
  | [] => by simp
  | a :: l => by simp [Chain', chain_eq_iff_eq_replicate, replicate_succ]

Characterization of Equality Chains as Replicated Lists

Informal description

For any list $l$ of elements of type $\alpha$, the following are equivalent: 1. The list $l$ is a chain with respect to the equality relation (i.e., all elements are equal). 2. There exists an element $a$ in the head of $l$ (if $l$ is non-empty) such that $l$ is equal to the list obtained by replicating $a$ exactly $\text{length}(l)$ times.

List.chains abbrev

Full source

/-- The type of `r`-decreasing chains -/
abbrev List.chains := { l : List α // l.Chain' (flip r) }

Type of $r$-Decreasing Chains with Lexicographic Order

Informal description

The type of $r$-decreasing chains, where a chain is a list of elements such that each consecutive pair satisfies the relation $r$ in reverse order (i.e., `Chain' (flip r)`). These chains are equipped with the lexicographic order `List.Lex r`.

List.lex_chains abbrev

(l m : List.chains r) : Prop

Full source

/-- The lexicographic order on the `r`-decreasing chains -/
abbrev List.lex_chains (l m : List.chains r) : Prop := List.Lex r l.val m.val

Lexicographic Order on $r$-Decreasing Chains

Informal description

The lexicographic order on $r$-decreasing chains is a relation between two chains $l$ and $m$ of type `List.chains r`, denoted as $l \prec_{\text{lex}} m$, where the order is defined by the lexicographic comparison of the lists with respect to the relation $r$.

Acc.list_chain' theorem

{l : List.chains r} (acc : ∀ a ∈ l.val.head?, Acc r a) : Acc (List.lex_chains r) l

Full source

/-- If an `r`-decreasing chain `l` is empty or its head is accessible by `r`, then
  `l` is accessible by the lexicographic order `List.Lex r`. -/
theorem Acc.list_chain' {l : List.chains r} (acc : ∀ a ∈ l.val.head?, Acc r a) :
    Acc (List.lex_chains r) l := by
  obtain ⟨_ | ⟨a, l⟩, hl⟩ := l
  · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
  specialize acc a _
  · rw [List.head?_cons, Option.mem_some_iff]
  /- For an r-decreasing chain of the form a :: l, apply induction on a -/
  induction acc generalizing l with
  | intro a _ ih =>
    /- Bundle l with a proof that it is r-decreasing to form l' -/
    have hl' := (List.chain'_cons'.1 hl).2
    let l' : List.chains r := ⟨l, hl'⟩
    have : Acc (List.lex_chains r) l' := by
      rcases l with - | ⟨b, l⟩
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      /- l' is accessible by induction hypothesis -/
      · apply ih b (List.chain'_cons.1 hl).1
    /- make l' a free variable and induct on l' -/
    revert hl
    rw [(by rfl : l = l'.1)]
    clear_value l'
    induction this with
    | intro l _ ihl =>
      intro hl
      apply Acc.intro
      rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      · apply ih b hr
      · apply ihl ⟨m, (List.chain'_cons'.1 hm).2⟩ hr

Accessibility of $r$-Decreasing Chains under Lexicographic Order

Informal description

Let $r$ be a relation on a type $\alpha$, and let $l$ be an $r$-decreasing chain (i.e., a list where each consecutive pair satisfies the relation $r$ in reverse order). If either $l$ is empty or every element in the head of $l$ is accessible with respect to $r$, then $l$ is accessible with respect to the lexicographic order `List.Lex r` on chains.

WellFounded.list_chain' theorem

(hwf : WellFounded r) : WellFounded (List.lex_chains r)

Full source

/-- If `r` is well-founded, the lexicographic order on `r`-decreasing chains is also. -/
theorem WellFounded.list_chain' (hwf : WellFounded r) :
    WellFounded (List.lex_chains r) :=
  ⟨fun _ ↦ Acc.list_chain' (fun _ _ => hwf.apply _)⟩

Well-foundedness of Lexicographic Order on $r$-Decreasing Chains

Informal description

If $r$ is a well-founded relation on a type $\alpha$, then the lexicographic order on $r$-decreasing chains (lists where each consecutive pair satisfies the relation $r$ in reverse order) is also well-founded.

instIsWellFoundedChainsLex_chains instance

[hwf : IsWellFounded α r] : IsWellFounded (List.chains r) (List.lex_chains r)

Full source

instance [hwf : IsWellFounded α r] :
    IsWellFounded (List.chains r) (List.lex_chains r) :=
  ⟨hwf.wf.list_chain'⟩

Well-foundedness of Lexicographic Order on Decreasing Chains

Informal description

For any type $\alpha$ with a well-founded relation $r$, the lexicographic order on $r$-decreasing chains (lists where each consecutive pair satisfies the relation $r$ in reverse order) is also well-founded.