Chains with a designated start and end

This file defines List.IsChainFromTo, a variant of List.IsChain that also fixes the first and last element of the chain. Such a chain is an explicit witness for the fact that its end point is reachable from its start point, and its length bounds the number of steps that are needed.

Main definitions

• List.IsChainFromTo r chain a b: chain is a non-empty list whose adjacent elements are related by r, whose first element is a and whose last element is b.

Main results

• List.IsChainFromTo.reflTransGen: the start and the end of a chain are related by Relation.ReflTransGen.
• List.IsChainFromTo.head_induction_on: induction on a chain, peeling off elements at the start.
• List.IsChainFromTo.exists_length_lt_of_not_nodup: a chain with duplicates can always be shortened.
• List.IsChainFromTo.exists_nodup: iterating the above yields a chain without duplicates.

structure List.IsChainFromTo {α : Type u_2} (r : α → α → Prop) (chain : List α) (a b : α) : Prop

A "chain from to" is a list of elements where adjacent elements relate to each other (cf. List.IsChain) and start and end with specific elements.

• isChain : IsChain r chain
• ne_nil : chain ≠ []
• head_eq : chain.head ⋯ = a
• getLast_eq : chain.getLast ⋯ = b

theorem List.IsChainFromTo.length_pos {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) : 0 < chain.length

A chain has at least one element.

theorem List.IsChainFromTo.getElem_zero {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) : chain[0] = a

The first element of an r-chain from a to b is a.

theorem List.IsChainFromTo.getElem_length_sub_one {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) : chain[chain.length - 1] = b

The last element of an r-chain from a to b is b.

theorem List.IsChainFromTo.reflTransGen {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) : Relation.ReflTransGen r a b

The start and the end of an r-chain are reflexively-transitively related by r.

theorem List.IsChain.isChainFromTo_of_ne_nil {α : Type u_1} {r : α → α → Prop} {chain : List α} (hc : IsChain r chain) (h_ne_nil : chain ≠ []) : IsChainFromTo r chain (chain.head h_ne_nil) (chain.getLast h_ne_nil)

Create a List.IsChainFromTo from a non-empty List.IsChain.

@[simp]

theorem List.isChainFromTo_singleton {α : Type u_1} {r : α → α → Prop} {a : α} : IsChainFromTo r [a] a a

A one-element list is an r-chain from that element to itself.

theorem List.IsChainFromTo.cons {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b c : α} (h : r a b) (hc : IsChainFromTo r chain b c) : IsChainFromTo r (a :: chain) a c

Prepend an r-related element to the start of the chain.

@[simp]

theorem List.isChainFromTo_pair_iff {α : Type u_1} {r : α → α → Prop} {a a' b b' : α} : IsChainFromTo r [a, b] a' b' ↔ r a b ∧ a = a' ∧ b = b'

theorem List.IsChainFromTo.of_cons_cons {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b x y : α} (hc : IsChainFromTo r (x :: y :: chain) a b) : IsChainFromTo r (y :: chain) y b

Removing the head yields a valid chain.

theorem List.IsChainFromTo.append_tail {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b c : α} (hc : IsChainFromTo r chain a b) {chain' : List α} (hc' : IsChainFromTo r chain' b c) : IsChainFromTo r (chain ++ chain'.tail) a c

Appending a chain and the tail of a second one whose start point equals the end point of the first yields a valid chain.

theorem List.IsChainFromTo.snoc {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b c : α} (hc : IsChainFromTo r chain a b) (h : r b c) : IsChainFromTo r (chain ++ [c]) a c

Add an r-related element to the end of the chain.

theorem List.IsChainFromTo.append_dropLast {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b c : α} (hc : IsChainFromTo r chain a b) {chain' : List α} (hc' : IsChainFromTo r chain' b c) : IsChainFromTo r (chain.dropLast ++ chain') a c

Appending a chain, dropping its last element and another chain whose start point equals the end point of the first chain yields a valid chain.

theorem List.IsChainFromTo.take {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) {i : ℕ} (hi : i < chain.length) : IsChainFromTo r (List.take (i + 1) chain) a chain[i]

Taking the first i + 1 elements of a chain yields a chain from the same start point to chain[i].

theorem List.IsChainFromTo.drop {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) {i : ℕ} (hi : i < chain.length) : IsChainFromTo r (List.drop i chain) chain[i] b

Dropping the first i elements of a chain yields a chain from chain[i] to the same end point.

theorem List.IsChainFromTo.head_induction_on {α : Type u_1} {r : α → α → Prop} {motive : {chain : List α} → {a b : α} → IsChainFromTo r chain a b → Prop} (h_refl : ∀ {a : α}, motive ⋯) (h_head : ∀ {a b c : α} {chain : List α} (hab : r a b) (hc : IsChainFromTo r chain b c), motive hc → motive ⋯) {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) : motive hc

theorem List.IsChainFromTo.reflTransGen_of_mem {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) {x : α} (mem : x ∈ chain) : Relation.ReflTransGen r a x

Any element of an r-chain from a to b is reflexively-transitively related from a.

theorem List.IsChainFromTo.reflTransGen_of_mem' {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) {x : α} (mem : x ∈ chain) : Relation.ReflTransGen r x b

Any element of an r-chain from a to b is reflexively-transitively related to b.

theorem List.IsChainFromTo.exists_length_lt_of_not_nodup {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) (h_dup : ¬chain.Nodup) : ∃ (chain' : List α), IsChainFromTo r chain' a b ∧ chain'.length < chain.length

If there is an r-chain from a to b with duplicates, then there is a shorter r-chain from a to b (the one that skips the part between the duplicates).

theorem List.IsChainFromTo.exists_nodup {α : Type u_1} {r : α → α → Prop} {chain : List α} {a b : α} (hc : IsChainFromTo r chain a b) : ∃ (chain' : List α), IsChainFromTo r chain' a b ∧ chain'.Nodup

For any r-chain from a to b there is one without duplicates.