Documentation

Mathlib.Data.List.Chain

Relation chain #

This file provides basic results about List.Chain (definition in Data.List.Defs). A list [a₂, ..., aₙ] is a Chain starting at a₁ with respect to the relation r if r a₁ a₂ and r a₂ a₃ and ... and r aₙ₋₁ aₙ. We write it Chain r a₁ [a₂, ..., aₙ]. A graph-specialized version is in development and will hopefully be added under combinatorics. sometime soon.

theorem List.chain_iff {α : Type u_1} (R : ααProp) :
∀ (a : α) (a_1 : List α), List.Chain R a a_1 a_1 = [] b l, R a b List.Chain R b l a_1 = b :: l
theorem List.Chain.iff {α : Type u} {R : ααProp} {S : ααProp} (H : ∀ (a b : α), R a b S a b) {a : α} {l : List α} :
theorem List.Chain.iff_mem {α : Type u} {R : ααProp} {a : α} {l : List α} :
List.Chain R a l List.Chain (fun x y => x a :: l y l R x y) a l
theorem List.chain_singleton {α : Type u} {R : ααProp} {a : α} {b : α} :
List.Chain R a [b] R a b
theorem List.chain_split {α : Type u} {R : ααProp} {a : α} {b : α} {l₁ : List α} {l₂ : List α} :
List.Chain R a (l₁ ++ b :: l₂) List.Chain R a (l₁ ++ [b]) List.Chain R b l₂
@[simp]
theorem List.chain_append_cons_cons {α : Type u} {R : ααProp} {a : α} {b : α} {c : α} {l₁ : List α} {l₂ : List α} :
List.Chain R a (l₁ ++ b :: c :: l₂) List.Chain R a (l₁ ++ [b]) R b c List.Chain R c l₂
theorem List.chain_iff_forall₂ {α : Type u} {R : ααProp} {a : α} {l : List α} :
theorem List.chain_append_singleton_iff_forall₂ {α : Type u} {R : ααProp} {l : List α} {a : α} {b : α} :
List.Chain R a (l ++ [b]) List.Forall₂ R (a :: l) (l ++ [b])
theorem List.chain_map {α : Type u} {β : Type v} {R : ααProp} (f : βα) {b : β} {l : List β} :
List.Chain R (f b) (List.map f l) List.Chain (fun a b => R (f a) (f b)) b l
theorem List.chain_of_chain_map {α : Type u} {β : Type v} {R : ααProp} {S : ββProp} (f : αβ) (H : (a b : α) → S (f a) (f b)R a b) {a : α} {l : List α} (p : List.Chain S (f a) (List.map f l)) :
theorem List.chain_map_of_chain {α : Type u} {β : Type v} {R : ααProp} {S : ββProp} (f : αβ) (H : (a b : α) → R a bS (f a) (f b)) {a : α} {l : List α} (p : List.Chain R a l) :
List.Chain S (f a) (List.map f l)
theorem List.chain_pmap_of_chain {α : Type u} {β : Type v} {R : ααProp} {S : ββProp} {p : αProp} {f : (a : α) → p aβ} (H : (a b : α) → (ha : p a) → (hb : p b) → R a bS (f a ha) (f b hb)) {a : α} {l : List α} (hl₁ : List.Chain R a l) (ha : p a) (hl₂ : (a : α) → a lp a) :
List.Chain S (f a ha) (List.pmap f l hl₂)
theorem List.chain_of_chain_pmap {α : Type u} {β : Type v} {R : ααProp} {S : ββProp} {p : αProp} (f : (a : α) → p aβ) {l : List α} (hl₁ : (a : α) → a lp a) {a : α} (ha : p a) (hl₂ : List.Chain S (f a ha) (List.pmap f l hl₁)) (H : (a b : α) → (ha : p a) → (hb : p b) → S (f a ha) (f b hb)R a b) :
theorem List.Chain.pairwise {α : Type u} {R : ααProp} [IsTrans α R] {a : α} {l : List α} :
List.Chain R a lList.Pairwise R (a :: l)
theorem List.chain_iff_pairwise {α : Type u} {R : ααProp} [IsTrans α R] {a : α} {l : List α} :
theorem List.Chain.sublist {α : Type u} {R : ααProp} {l₁ : List α} {l₂ : List α} {a : α} [IsTrans α R] (hl : List.Chain R a l₂) (h : List.Sublist l₁ l₂) :
List.Chain R a l₁
theorem List.Chain.rel {α : Type u} {R : ααProp} {l : List α} {a : α} {b : α} [IsTrans α R] (hl : List.Chain R a l) (hb : b l) :
R a b
theorem List.chain_iff_get {α : Type u} {R : ααProp} {a : α} {l : List α} :
List.Chain R a l ((h : 0 < List.length l) → R a (List.get l { val := 0, isLt := h })) ((i : ) → (h : i < List.length l - 1) → R (List.get l { val := i, isLt := (_ : i < List.length l) }) (List.get l { val := i + 1, isLt := (_ : Nat.succ i < List.length l) }))
@[deprecated List.chain_iff_get]
theorem List.chain_iff_nthLe {α : Type u} {R : ααProp} {a : α} {l : List α} :
List.Chain R a l ((h : 0 < List.length l) → R a (List.nthLe l 0 h)) ((i : ) → (h : i < List.length l - 1) → R (List.nthLe l i (_ : i < List.length l)) (List.nthLe l (i + 1) (_ : Nat.succ i < List.length l)))
theorem List.Chain'.imp {α : Type u} {R : ααProp} {S : ααProp} (H : (a b : α) → R a bS a b) {l : List α} (p : List.Chain' R l) :
theorem List.Chain'.iff {α : Type u} {R : ααProp} {S : ααProp} (H : ∀ (a b : α), R a b S a b) {l : List α} :
theorem List.Chain'.iff_mem {α : Type u} {R : ααProp} {l : List α} :
List.Chain' R l List.Chain' (fun x y => x l y l R x y) l
@[simp]
theorem List.chain'_nil {α : Type u} {R : ααProp} :
@[simp]
theorem List.chain'_singleton {α : Type u} {R : ααProp} (a : α) :
@[simp]
theorem List.chain'_cons {α : Type u} {R : ααProp} {x : α} {y : α} {l : List α} :
List.Chain' R (x :: y :: l) R x y List.Chain' R (y :: l)
theorem List.chain'_isInfix {α : Type u} (l : List α) :
List.Chain' (fun x y => [x, y] <:+: l) l
theorem List.chain'_split {α : Type u} {R : ααProp} {a : α} {l₁ : List α} {l₂ : List α} :
List.Chain' R (l₁ ++ a :: l₂) List.Chain' R (l₁ ++ [a]) List.Chain' R (a :: l₂)
@[simp]
theorem List.chain'_append_cons_cons {α : Type u} {R : ααProp} {b : α} {c : α} {l₁ : List α} {l₂ : List α} :
List.Chain' R (l₁ ++ b :: c :: l₂) List.Chain' R (l₁ ++ [b]) R b c List.Chain' R (c :: l₂)
theorem List.chain'_map {α : Type u} {β : Type v} {R : ααProp} (f : βα) {l : List β} :
List.Chain' R (List.map f l) List.Chain' (fun a b => R (f a) (f b)) l
theorem List.chain'_of_chain'_map {α : Type u} {β : Type v} {R : ααProp} {S : ββProp} (f : αβ) (H : (a b : α) → S (f a) (f b)R a b) {l : List α} (p : List.Chain' S (List.map f l)) :
theorem List.chain'_map_of_chain' {α : Type u} {β : Type v} {R : ααProp} {S : ββProp} (f : αβ) (H : (a b : α) → R a bS (f a) (f b)) {l : List α} (p : List.Chain' R l) :
theorem List.Pairwise.chain' {α : Type u} {R : ααProp} {l : List α} :
theorem List.chain'_iff_pairwise {α : Type u} {R : ααProp} [IsTrans α R] {l : List α} :
theorem List.Chain'.sublist {α : Type u} {R : ααProp} {l₁ : List α} {l₂ : List α} [IsTrans α R] (hl : List.Chain' R l₂) (h : List.Sublist l₁ l₂) :
theorem List.Chain'.cons {α : Type u} {R : ααProp} {x : α} {y : α} {l : List α} (h₁ : R x y) (h₂ : List.Chain' R (y :: l)) :
List.Chain' R (x :: y :: l)
theorem List.Chain'.tail {α : Type u} {R : ααProp} {l : List α} :
theorem List.Chain'.rel_head {α : Type u} {R : ααProp} {x : α} {y : α} {l : List α} (h : List.Chain' R (x :: y :: l)) :
R x y
theorem List.Chain'.rel_head? {α : Type u} {R : ααProp} {x : α} {l : List α} (h : List.Chain' R (x :: l)) ⦃y : α (hy : y List.head? l) :
R x y
theorem List.Chain'.cons' {α : Type u} {R : ααProp} {x : α} {l : List α} :
List.Chain' R l((y : α) → y List.head? lR x y) → List.Chain' R (x :: l)
theorem List.chain'_cons' {α : Type u} {R : ααProp} {x : α} {l : List α} :
List.Chain' R (x :: l) ((y : α) → y List.head? lR x y) List.Chain' R l
theorem List.chain'_append {α : Type u} {R : ααProp} {l₁ : List α} {l₂ : List α} :
List.Chain' R (l₁ ++ l₂) List.Chain' R l₁ List.Chain' R l₂ ((x : α) → x List.getLast? l₁(y : α) → y List.head? l₂R x y)
theorem List.Chain'.append {α : Type u} {R : ααProp} {l₁ : List α} {l₂ : List α} (h₁ : List.Chain' R l₁) (h₂ : List.Chain' R l₂) (h : (x : α) → x List.getLast? l₁(y : α) → y List.head? l₂R x y) :
List.Chain' R (l₁ ++ l₂)
theorem List.Chain'.left_of_append {α : Type u} {R : ααProp} {l₁ : List α} {l₂ : List α} (h : List.Chain' R (l₁ ++ l₂)) :
theorem List.Chain'.right_of_append {α : Type u} {R : ααProp} {l₁ : List α} {l₂ : List α} (h : List.Chain' R (l₁ ++ l₂)) :
theorem List.Chain'.infix {α : Type u} {R : ααProp} {l : List α} {l₁ : List α} (h : List.Chain' R l) (h' : l₁ <:+: l) :
theorem List.Chain'.suffix {α : Type u} {R : ααProp} {l : List α} {l₁ : List α} (h : List.Chain' R l) (h' : l₁ <:+ l) :
theorem List.Chain'.prefix {α : Type u} {R : ααProp} {l : List α} {l₁ : List α} (h : List.Chain' R l) (h' : l₁ <+: l) :
theorem List.Chain'.drop {α : Type u} {R : ααProp} {l : List α} (h : List.Chain' R l) (n : ) :
theorem List.Chain'.init {α : Type u} {R : ααProp} {l : List α} (h : List.Chain' R l) :
theorem List.Chain'.take {α : Type u} {R : ααProp} {l : List α} (h : List.Chain' R l) (n : ) :
theorem List.chain'_pair {α : Type u} {R : ααProp} {x : α} {y : α} :
List.Chain' R [x, y] R x y
theorem List.Chain'.imp_head {α : Type u} {R : ααProp} {x : α} {y : α} (h : {z : α} → R x zR y z) {l : List α} (hl : List.Chain' R (x :: l)) :
List.Chain' R (y :: l)
theorem List.chain'_reverse {α : Type u} {R : ααProp} {l : List α} :
theorem List.chain'_iff_get {α : Type u} {R : ααProp} {l : List α} :
List.Chain' R l (i : ) → (h : i < List.length l - 1) → R (List.get l { val := i, isLt := (_ : i < List.length l) }) (List.get l { val := i + 1, isLt := (_ : Nat.succ i < List.length l) })
@[deprecated List.chain'_iff_get]
theorem List.chain'_iff_nthLe {α : Type u} {R : ααProp} {l : List α} :
List.Chain' R l (i : ) → (h : i < List.length l - 1) → R (List.nthLe l i (_ : i < List.length l)) (List.nthLe l (i + 1) (_ : Nat.succ i < List.length l))
theorem List.Chain'.append_overlap {α : Type u} {R : ααProp} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : List.Chain' R (l₁ ++ l₂)) (h₂ : List.Chain' R (l₂ ++ l₃)) (hn : l₂ []) :
List.Chain' R (l₁ ++ l₂ ++ l₃)

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 List.chain'_join {α : Type u} {R : ααProp} {L : List (List α)} :
¬[] L → (List.Chain' R (List.join L) (∀ (l : List α), l LList.Chain' R l) List.Chain' (fun l₁ l₂ => (x : α) → x List.getLast? l₁(y : α) → y List.head? l₂R x y) L)
theorem List.exists_chain_of_relationReflTransGen {α : Type u} {r : ααProp} {a : α} {b : α} (h : Relation.ReflTransGen r a b) :
l, List.Chain r a l List.getLast (a :: l) (_ : a :: l []) = b

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 List.Chain.induction {α : Type u} {r : ααProp} {a : α} {b : α} (p : αProp) (l : List α) (h : List.Chain r a l) (hb : List.getLast (a :: l) (_ : a :: l []) = b) (carries : x y : α⦄ → r x yp yp x) (final : p b) (i : α) :
i a :: lp i

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 List.Chain.induction_head {α : Type u} {r : ααProp} {a : α} {b : α} (p : αProp) (l : List α) (h : List.Chain r a l) (hb : List.getLast (a :: l) (_ : a :: l []) = b) (carries : x y : α⦄ → r x yp yp x) (final : p b) :
p a

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.

theorem List.relationReflTransGen_of_exists_chain {α : Type u} {r : ααProp} {a : α} {b : α} (l : List α) (hl₁ : List.Chain r a l) (hl₂ : List.getLast (a :: l) (_ : a :: l []) = b) :

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.

In this section, we consider the type of r-decreasing chains (List.Chain' (flip r)) equipped with lexicographic order List.Lex r.

@[inline, reducible]
abbrev List.chains {α : Type u_1} (r : ααProp) :
Type u_1

The type of r-decreasing chains

Equations
Instances For
    @[inline, reducible]
    abbrev List.lex_chains {α : Type u_1} (r : ααProp) (l : List.chains r) (m : List.chains r) :

    The lexicographic order on the r-decreasing chains

    Equations
    Instances For
      theorem Acc.list_chain' {α : Type u_1} {r : ααProp} {l : List.chains r} (acc : ∀ (a : α), a List.head? lAcc r a) :

      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 WellFounded.list_chain' {α : Type u_1} {r : ααProp} (hwf : WellFounded r) :

      If r is well-founded, the lexicographic order on r-decreasing chains is also.