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}
{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 :: List.dropLast l) 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 : 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 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]
@[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 : List.Sublist l₁ 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 (List.tail l)
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? l → 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 ∈ List.head? l → 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 ∈ 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₂))
:
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 (List.dropLast l)
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 (List.reverse l) ↔ List.Chain' (flip R) l
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 ∈ L → List.Chain' R l) ∧ List.Chain' (fun (l₁ l₂ : List α) => ∀ (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 α), 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 y → p y → p x)
(final : p b)
(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 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₂ : List.getLast (a :: l) (_ : a :: l ≠ []) = 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 (x x_1 : α) => x > x_1) (a :: as))
(hm : List.Chain' (fun (x x_1 : α) => x > x_1) m)
(hmas : m ≤ as)
:
List.Chain' (fun (x x_1 : α) => x > x_1) (a :: m)
In this section, we consider the type of r-decreasing chains (List.Chain' (flip r))
equipped with lexicographic order List.Lex r.
@[inline, reducible]
The type of r-decreasing chains
Equations
- List.chains r = { l : List α // List.Chain' (flip r) l }
Instances For
@[inline, reducible]
The lexicographic order on the r-decreasing chains
Equations
- List.lex_chains r l m = List.Lex r ↑l ↑m
Instances For
theorem
Acc.list_chain'
{α : Type u_1}
{r : α → α → Prop}
{l : List.chains r}
(acc : ∀ (a : α), a ∈ List.head? ↑l → 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.
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
- (_ : IsWellFounded (List.chains r) (List.lex_chains r)) = (_ : IsWellFounded (List.chains r) (List.lex_chains r))