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 α} : List.Chain R a l ↔ List.Chain S a l

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)) : List.Chain R a l

theorem List.chain_map_of_chain {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a b → S (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 b → S (f a ha) (f b hb)) {a : α} {l : List α} (hl₁ : List.Chain R a l) (ha : p a) (hl₂ : ∀ (a : α), a ∈ l → p 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 ∈ l → p 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) : List.Chain R a l

theorem List.Chain.pairwise {α : Type u} {R : α → α → Prop} [IsTrans α R] {a : α} {l : List α} : List.Chain R a l → List.Pairwise R (a :: l)

theorem List.chain_iff_pairwise {α : Type u} {R : α → α → Prop} [IsTrans α R] {a : α} {l : List α} : List.Chain R a l ↔ List.Pairwise R (a :: l)

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_replicate_of_rel {α : Type u} {r : α → α → Prop} (n : ℕ) {a : α} (h : r a a) : List.Chain r a (List.replicate n a)

theorem List.chain_eq_iff_eq_replicate {α : Type u} {a : α} {l : List α} : List.Chain (fun (x1 x2 : α) => x1 = x2) a l ↔ l = List.replicate l.length a

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

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

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} : List.Chain' R []

@[simp]

theorem List.chain'_singleton {α : Type u} {R : α → α → Prop} (a : α) : List.Chain' R [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)) : List.Chain' R l

theorem List.chain'_map_of_chain' {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a b → S (f a) (f b)) {l : List α} (p : List.Chain' R l) : List.Chain' S (List.map f l)

theorem List.Pairwise.chain' {α : Type u} {R : α → α → Prop} {l : List α} : List.Pairwise R l → List.Chain' R l

theorem List.chain'_iff_pairwise {α : Type u} {R : α → α → Prop} [IsTrans α R] {l : List α} : List.Chain' R l ↔ List.Pairwise R l

theorem List.Chain'.sublist {α : Type u} {R : α → α → Prop} {l₁ : List α} {l₂ : List α} [IsTrans α R] (hl : List.Chain' R l₂) (h : l₁.Sublist l₂) : List.Chain' R 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 l → List.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₂)) : List.Chain' R l₁

theorem List.Chain'.right_of_append {α : Type u} {R : α → α → Prop} {l₁ : List α} {l₂ : List α} (h : List.Chain' R (l₁ ++ l₂)) : List.Chain' R l₂

theorem List.Chain'.infix {α : Type u} {R : α → α → Prop} {l : List α} {l₁ : List α} (h : List.Chain' R l) (h' : l₁ <:+: l) : List.Chain' R l₁

theorem List.Chain'.suffix {α : Type u} {R : α → α → Prop} {l : List α} {l₁ : List α} (h : List.Chain' R l) (h' : l₁ <:+ l) : List.Chain' R l₁

theorem List.Chain'.prefix {α : Type u} {R : α → α → Prop} {l : List α} {l₁ : List α} (h : List.Chain' R l) (h' : l₁ <+: l) : List.Chain' R l₁

theorem List.Chain'.drop {α : Type u} {R : α → α → Prop} {l : List α} (h : List.Chain' R l) (n : ℕ) : List.Chain' R (List.drop n l)

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 : ℕ) : List.Chain' R (List.take n l)

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 z → R 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 ∈ L → List.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 y → p x → p y) (initial : p a) (i : α) : i ∈ l → p 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 y → p x → p y) (initial : ∀ (lne : l ≠ []), p (l.head lne)) (i : α) : i ∈ l → p 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 y → p y → p x) (final : p b) (i : α) : i ∈ a :: l → p 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 y → p y → p 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) : Relation.ReflTransGen r a 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)) : List.Chain R v l

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]

theorem List.chain'_replicate_of_rel {α : Type u} {r : α → α → Prop} (n : ℕ) {a : α} (h : r a a) : List.Chain' r (List.replicate n a)

theorem List.chain'_eq_iff_eq_replicate {α : Type u} {l : List α} : List.Chain' (fun (x1 x2 : α) => x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = List.replicate l.length a

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

• List.chains r = { l : List α // List.Chain' (flip r) l }

@[reducible, inline]

abbrev List.lex_chains {α : Type u_1} (r : α → α → Prop) (l : List.chains r) (m : List.chains r) : Prop

The lexicographic order on the r-decreasing chains

Equations

• List.lex_chains r l m = List.Lex r ↑l ↑m

theorem Acc.list_chain' {α : Type u_1} {r : α → α → Prop} {l : List.chains r} (acc : ∀ (a : α), a ∈ (↑l).head? → Acc r a) : Acc (List.lex_chains r) l

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) : WellFounded (List.lex_chains 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] : IsWellFounded (List.chains r) (List.lex_chains r)

Equations

• ⋯ = ⋯