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 : List α), 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 α} :
List.Chain R a l l = [] List.Forall₂ R (a :: l.dropLast) l
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 : l₁.Sublist 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 < l.length), R a (l.get 0, h)) ∀ (i : ) (h : i < l.length - 1), R (l.get i, ) (l.get i + 1, )
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 : l₁.Sublist 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 α} :
List.Chain' R lList.Chain' R l.tail
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 l.head?) :
R x y
theorem List.Chain'.cons' {α : Type u} {R : ααProp} {x : α} {l : List α} :
List.Chain' R l(∀ (y : α), y l.head?R 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 l.head?R 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 l₁.getLast?∀ (y : α), y l₂.head?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 l₁.getLast?∀ (y : α), y l₂.head?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) :
List.Chain' R l.dropLast
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 α} :
List.Chain' R l.reverse List.Chain' (flip R) l
theorem List.chain'_iff_get {α : Type u} {R : ααProp} {l : List α} :
List.Chain' R l ∀ (i : ) (h : i < l.length - 1), R (l.get i, ) (l.get i + 1, )
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 L.join (∀ (l : List α), l LList.Chain' R l) List.Chain' (fun (l₁ l₂ : List α) => ∀ (x : α), x l₁.getLast?∀ (y : α), y l₂.head?R x y) L)
theorem List.exists_chain_of_relationReflTransGen {α : Type u} {r : ααProp} {a : α} {b : α} (h : Relation.ReflTransGen r a b) :
∃ (l : List α), List.Chain r a l (a :: l).getLast = 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 : α} (p : αProp) (l : List α) (h : List.Chain r a l) (carries : ∀ ⦃x y : α⦄, r x yp xp y) (initial : p a) (i : α) :
i lp i

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 List.Chain'.induction {α : Type u} {r : ααProp} (p : αProp) (l : List α) (h : List.Chain' r l) (carries : ∀ ⦃x y : α⦄, r x yp xp y) (initial : ∀ (lne : l []), p (l.head lne)) (i : α) :
i lp i

A version of List.Chain.induction for List.Chain'

theorem List.Chain.backwards_induction {α : Type u} {r : ααProp} {a : α} {b : α} (p : αProp) (l : List α) (h : List.Chain r a l) (hb : (a :: l).getLast = 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.backwards_induction_head {α : Type u} {r : ααProp} {a : α} {b : α} (p : αProp) (l : List α) (h : List.Chain r a l) (hb : (a :: l).getLast = 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₂ : (a :: l).getLast = 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.

theorem List.Chain'.cons_of_le {α : Type u} [LinearOrder α] {a : α} {as : List α} {m : List α} (ha : List.Chain' (fun (x1 x2 : α) => x1 > x2) (a :: as)) (hm : List.Chain' (fun (x1 x2 : α) => x1 > x2) m) (hmas : m as) :
List.Chain' (fun (x1 x2 : α) => x1 > x2) (a :: m)
theorem List.Chain'.chain {α : Type u_1} {R : ααProp} {l : List α} {v : α} (hl : List.Chain' R l) (hv : ∀ (lne : l []), R v (l.head lne)) :
theorem List.Chain'.iterate_eq_of_apply_eq {α : Type u_1} {f : αα} {l : List α} (hl : List.Chain' (fun (x y : α) => f x = y) l) (i : ) (hi : i < l.length) :
f^[i] l[0] = l[i]

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

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

The type of r-decreasing chains

Equations
Instances For
    @[reducible, inline]
    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 (↑l).head?Acc 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.

      instance instIsWellFoundedChainsLex_chains {α : Type u_1} {r : ααProp} [hwf : IsWellFounded α r] :
      Equations
      • =