Relation chain

This file provides basic results about List.IsChain from Batteries. A list [a₁, a₂, ..., aₙ] satisfies IsChain with respect to the relation r if r a₁ a₂ and r a₂ a₃ and ... and r aₙ₋₁ aₙ. We write it IsChain r [a₁, a₂, ..., aₙ]. A graph-specialized version is in development and will hopefully be added under combinatorics. sometime soon.

theorem List.isChain_iff {α : Type u_1} (R : α → α → Prop) (a✝ : List α) : IsChain R a✝ ↔ a✝ = [] ∨ (∃ (a : α), a✝ = [a]) ∨ ∃ (a : α), ∃ (b : α), ∃ (l : List α), R a b ∧ IsChain R (b :: l) ∧ a✝ = a :: b :: l

theorem List.isChain_nil {α : Type u} {R : α → α → Prop} : IsChain R []

theorem List.isChain_singleton {α : Type u} {R : α → α → Prop} (a : α) : IsChain R [a]

theorem List.isChain_cons_iff {α : Type u} (R : α → α → Prop) (a : α) (l : List α) : IsChain R (a :: l) ↔ l = [] ∨ ∃ (b : α), ∃ (l' : List α), R a b ∧ IsChain R (b :: l') ∧ l = b :: l'

theorem List.IsChain.imp_of_mem_tail_imp {α : Type u} {R S : α → α → Prop} {l : List α} (H : ∀ (a b : α), a ∈ l → b ∈ l.tail → R a b → S a b) (p : IsChain R l) : IsChain S l

theorem List.IsChain.imp_of_mem_imp {α : Type u} {R S : α → α → Prop} {l : List α} (H : ∀ (a b : α), a ∈ l → b ∈ l → R a b → S a b) (p : IsChain R l) : IsChain S l

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

theorem List.IsChain.iff_of_mem_imp {α : Type u} {R S : α → α → Prop} {l : List α} (H : ∀ (a b : α), a ∈ l → b ∈ l → (R a b ↔ S a b)) : IsChain R l ↔ IsChain S l

theorem List.IsChain.iff_of_mem_tail_imp {α : Type u} {R S : α → α → Prop} {l : List α} (H : ∀ (a b : α), a ∈ l → b ∈ l.tail → (R a b ↔ S a b)) : IsChain R l ↔ IsChain S l

theorem List.IsChain.iff_mem {α : Type u} {R : α → α → Prop} {l : List α} : IsChain R l ↔ IsChain (fun (x y : α) => x ∈ l ∧ y ∈ l ∧ R x y) l

theorem List.IsChain.iff_mem_mem_tail {α : Type u} {R : α → α → Prop} {l : List α} : IsChain R l ↔ IsChain (fun (x y : α) => x ∈ l ∧ y ∈ l.tail ∧ R x y) l

theorem List.isChain_pair {α : Type u} {R : α → α → Prop} {x y : α} : IsChain R [x, y] ↔ R x y

theorem List.isChain_isInfix {α : Type u} (l : List α) : IsChain (fun (x y : α) => [x, y] <:+: l) l

theorem List.isChain_split {α : Type u} {R : α → α → Prop} {c : α} {l₁ l₂ : List α} : IsChain R (l₁ ++ c :: l₂) ↔ IsChain R (l₁ ++ [c]) ∧ IsChain R (c :: l₂)

theorem List.isChain_cons_split {α : Type u} {R : α → α → Prop} {a c : α} {l₁ l₂ : List α} : IsChain R (a :: (l₁ ++ c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [c])) ∧ IsChain R (c :: l₂)

@[simp]

theorem List.isChain_append_cons_cons {α : Type u} {R : α → α → Prop} {b c : α} {l₁ l₂ : List α} : IsChain R (l₁ ++ b :: c :: l₂) ↔ IsChain R (l₁ ++ [b]) ∧ R b c ∧ IsChain R (c :: l₂)

@[simp]

theorem List.isChain_cons_append_cons_cons {α : Type u} {R : α → α → Prop} {a b c : α} {l₁ l₂ : List α} : IsChain R (a :: (l₁ ++ b :: c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [b])) ∧ R b c ∧ IsChain R (c :: l₂)

theorem List.isChain_iff_forall_rel_of_append_cons_cons {α : Type u} {R : α → α → Prop} {l : List α} : IsChain R l ↔ ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b

theorem List.isChain_iff_forall₂ {α : Type u} {R : α → α → Prop} {l : List α} : IsChain R l ↔ Forall₂ R l.dropLast l.tail

theorem List.isChain_cons_iff_forall₂ {α : Type u} {R : α → α → Prop} {l : List α} {a : α} : IsChain R (a :: l) ↔ l = [] ∨ Forall₂ R (a :: l.dropLast) l

theorem List.isChain_cons_append_singleton_iff_forall₂ {α : Type u} {R : α → α → Prop} {l : List α} {a b : α} : IsChain R (a :: l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])

theorem List.isChain_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {l : List β} : IsChain R (map f l) ↔ IsChain (fun (a b : β) => R (f a) (f b)) l

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

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

theorem List.isChain_cons_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {l : List β} {b : β} : IsChain R (f b :: map f l) ↔ IsChain (fun (a b : β) => R (f a) (f b)) (b :: l)

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

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

theorem List.isChain_pmap {α : Type u} {β : Type v} {S : β → β → Prop} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (hl : ∀ (a : α), a ∈ l → p a) : IsChain S (pmap f l hl) ↔ IsChain (fun (a b : α) => ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) l

theorem List.isChain_pmap_of_isChain {α : 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)) {l : List α} (hl₁ : IsChain R l) (hl₂ : ∀ (a : α), a ∈ l → p a) : IsChain S (pmap f l hl₂)

theorem List.isChain_of_isChain_pmap {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (hl₁ : ∀ (a : α), a ∈ l → p a) (hl₂ : IsChain S (pmap f l hl₁)) (H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b) : IsChain R l

theorem List.isChain_cons_pmap {α : Type u} {β : Type v} {R : α → α → Prop} {p : β → Prop} (f : (b : β) → p b → α) {l : List β} (hl : ∀ (b : β), b ∈ l → p b) {a : β} (ha : p a) : IsChain R (f a ha :: pmap f l hl) ↔ IsChain (fun (a b : β) => ∃ (ha : p a), ∃ (hb : p b), R (f a ha) (f b hb)) (a :: l)

theorem List.isChain_cons_pmap_of_isChain_cons {α : 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)) {l : List α} {a : α} (ha : p a) (hl₁ : IsChain R (a :: l)) (hl₂ : ∀ (a : α), a ∈ l → p a) : IsChain S (f a ha :: pmap f l hl₂)

theorem List.isChain_cons_of_isChain_cons_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₂ : IsChain S (f a ha :: pmap f l hl₁)) (H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b) : IsChain R (a :: l)

theorem List.IsChain.sublist {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} [Trans R R R] (hl : IsChain R l₂) (h : l₁.Sublist l₂) : IsChain R l₁

theorem List.IsChain.rel_cons {α : Type u} {R : α → α → Prop} {l : List α} {a b : α} [Trans R R R] (hl : IsChain R (a :: l)) (hb : b ∈ l) : R a b

theorem List.IsChain.tail {α : Type u} {R : α → α → Prop} {l : List α} (h : IsChain R l) : IsChain R l.tail

theorem List.IsChain.rel_head {α : Type u} {R : α → α → Prop} {x y : α} {l : List α} (h : IsChain R (x :: y :: l)) : R x y

theorem List.IsChain.rel_head? {α : Type u} {R : α → α → Prop} {x : α} {l : List α} (h : IsChain R (x :: l)) ⦃y : α⦄ (hy : y ∈ l.head?) : R x y

theorem List.IsChain.cons {α : Type u} {R : α → α → Prop} {x : α} {l : List α} : IsChain R l → (∀ (y : α), y ∈ l.head? → R x y) → IsChain R (x :: l)

@[deprecated List.IsChain.cons (since := "2025-10-16")]

theorem List.IsChain.cons' {α : Type u} {R : α → α → Prop} {x : α} {l : List α} : IsChain R l → (∀ (y : α), y ∈ l.head? → R x y) → IsChain R (x :: l)

Alias of List.IsChain.cons.

theorem List.IsChain.cons_of_ne_nil {α : Type u} {R : α → α → Prop} {x : α} {l : List α} (l_ne_nil : l ≠ []) (hl : IsChain R l) (h : R x (l.head l_ne_nil)) : IsChain R (x :: l)

theorem List.isChain_cons {α : Type u} {R : α → α → Prop} {x : α} {l : List α} : IsChain R (x :: l) ↔ (∀ (y : α), y ∈ l.head? → R x y) ∧ IsChain R l

@[deprecated List.isChain_cons (since := "2025-10-16")]

theorem List.isChain_cons' {α : Type u} {R : α → α → Prop} {x : α} {l : List α} : IsChain R (x :: l) ↔ (∀ (y : α), y ∈ l.head? → R x y) ∧ IsChain R l

Alias of List.isChain_cons.

theorem List.isChain_append {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} : IsChain R (l₁ ++ l₂) ↔ IsChain R l₁ ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

theorem List.IsChain.append {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} (h₁ : IsChain R l₁) (h₂ : IsChain R l₂) (h : ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) : IsChain R (l₁ ++ l₂)

theorem List.IsChain.left_of_append {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} (h : IsChain R (l₁ ++ l₂)) : IsChain R l₁

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

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

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

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

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

theorem List.IsChain.dropLast {α : Type u} {R : α → α → Prop} {l : List α} (h : IsChain R l) : IsChain R l.dropLast

theorem List.IsChain.take {α : Type u} {R : α → α → Prop} {l : List α} (h : IsChain R l) (n : ℕ) : IsChain R (List.take n l)

theorem List.IsChain.imp_head {α : Type u} {R : α → α → Prop} {x y : α} (h : ∀ {z : α}, R x z → R y z) {l : List α} (hl : IsChain R (x :: l)) : IsChain R (y :: l)

@[deprecated List.isChain_iff_getElem (since := "2025-11-25")]

theorem List.isChain_iff_get {α : Type u} {R : α → α → Prop} {l : List α} : IsChain R l ↔ ∀ (i : Fin l.length.pred), R (l.get (Fin.cast ⋯ i.castSucc)) (l.get (Fin.cast ⋯ i.succ))

@[deprecated List.isChain_iff_getElem (since := "2025-11-25")]

theorem List.isChain_cons_iff_get {α : Type u} {R : α → α → Prop} {a : α} {l : List α} : IsChain R (a :: l) ↔ ∀ (i : Fin l.length), R ((a :: l).get i.castSucc) ((a :: l).get i.succ)

theorem List.exists_not_getElem_of_not_isChain {α : Type u} {R : α → α → Prop} {l : List α} (h : ¬IsChain R l) : ∃ (n : ℕ), ∃ (h : n + 1 < l.length), ¬R l[n] l[n + 1]

theorem List.isChain_reverse {α : Type u} {R : α → α → Prop} {l : List α} : IsChain R l.reverse ↔ IsChain (fun (a b : α) => R b a) l

theorem List.IsChain.append_overlap {α : Type u} {R : α → α → Prop} {l₁ l₂ l₃ : List α} (h₁ : IsChain R (l₁ ++ l₂)) (h₂ : IsChain R (l₂ ++ l₃)) (hn : l₂ ≠ []) : IsChain R (l₁ ++ l₂ ++ l₃)

If l₁ l₂ and l₃ are lists and l₁ ++ l₂ and l₂ ++ l₃ both satisfy IsChain R, then so does l₁ ++ l₂ ++ l₃ provided l₂ ≠ []

theorem List.isChain_flatten {α : Type u} {R : α → α → Prop} {L : List (List α)} : ¬[] ∈ L → (IsChain R L.flatten ↔ (∀ (l : List α), l ∈ L → IsChain R l) ∧ IsChain (fun (l₁ l₂ : List α) => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) L)

theorem List.isChain_attachWith {α : Type u} {l : List α} {p : α → Prop} (h : ∀ (x : α), x ∈ l → p x) {r : { a : α // p a } → { a : α // p a } → Prop} : IsChain r (l.attachWith p h) ↔ IsChain (fun (a b : α) => ∃ (ha : p a), ∃ (hb : p b), r ⟨a, ha⟩ ⟨b, hb⟩) l

theorem List.isChain_attach {α : Type u} {l : List α} {r : { a : α // a ∈ l } → { a : α // a ∈ l } → Prop} : IsChain r l.attach ↔ IsChain (fun (a b : α) => ∃ (ha : a ∈ l), ∃ (hb : b ∈ l), r ⟨a, ha⟩ ⟨b, hb⟩) l

theorem List.exists_isChain_cons_of_relationReflTransGen {α : Type u} {r : α → α → Prop} {a b : α} (h : Relation.ReflTransGen r a b) : ∃ (l : List α), IsChain 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.

theorem List.exists_isChain_ne_nil_of_relationReflTransGen {α : Type u} {r : α → α → Prop} {a b : α} (h : Relation.ReflTransGen r a b) : ∃ (l : List α), ∃ (hl : l ≠ []), IsChain r l ∧ l.head hl = a ∧ l.getLast hl = 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.

theorem List.IsChain.induction {α : Type u} {r : α → α → Prop} (p : α → Prop) (l : List α) (h : IsChain r l) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : ∀ (lne : l ≠ []), p (l.head lne)) (i : α) : i ∈ l → p i

Given a chain l, such that a predicate p holds for its head if it is nonempty, and 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.IsChain.cons_induction {α : Type u} {r : α → α → Prop} {a : α} (p : α → Prop) (l : List α) (h : IsChain 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.IsChain.concat_induction {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : IsChain r (l ++ [b])) (hb : (l ++ [b]).head ⋯ = a) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) (i : α) : i ∈ l ++ [b] → p i

theorem List.IsChain.concat_induction_head {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : IsChain r (l ++ [b])) (hb : (l ++ [b]).head ⋯ = a) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) : p b

theorem List.IsChain.backwards_induction {α : Type u} {r : α → α → Prop} (p : α → Prop) (l : List α) (h : IsChain r l) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : ∀ (lne : l ≠ []), p (l.getLast lne)) (i : α) : i ∈ 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.IsChain.backwards_concat_induction {α : Type u} {r : α → α → Prop} {b : α} (p : α → Prop) (l : List α) (h : IsChain r (l ++ [b])) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) (i : α) : i ∈ 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.IsChain.backwards_cons_induction {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : IsChain 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

theorem List.IsChain.backwards_cons_induction_head {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : IsChain 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_isChain {α : Type u} {r : α → α → Prop} (l : List α) (hl₁ : IsChain r l) (hne : l ≠ []) : Relation.ReflTransGen r (l.head hne) (l.getLast hne)

If there is a non-empty r-chain, its head and last element are related by the reflexive transitive closure of r.

theorem List.relationReflTransGen_of_exists_isChain_cons {α : Type u} {r : α → α → Prop} {a b : α} (l : List α) (hl₁ : IsChain 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.

theorem List.IsChain.cons_of_le {α : Type u} [LinearOrder α] {a : α} {as m : List α} (ha : IsChain (fun (x1 x2 : α) => x1 > x2) (a :: as)) (hm : IsChain (fun (x1 x2 : α) => x1 > x2) m) (hmas : m ≤ as) : IsChain (fun (x1 x2 : α) => x1 > x2) (a :: m)

theorem List.IsChain.isChain_cons {α : Type u_1} {R : α → α → Prop} {l : List α} {v : α} (hl : IsChain R l) (hv : ∀ (lne : l ≠ []), R v (l.head lne)) : IsChain R (v :: l)

theorem List.IsChain.iterate_eq_of_apply_eq {α : Type u_1} {f : α → α} {l : List α} (hl : IsChain (fun (x y : α) => f x = y) l) (i : ℕ) (hi : i < l.length) : f^[i] l[0] = l[i]

theorem List.isChain_replicate_of_rel {α : Type u} {r : α → α → Prop} (n : ℕ) {a : α} (h : r a a) : IsChain r (replicate n a)

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

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

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

@[reducible, inline]

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

The type of r-decreasing chains

Equations

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

@[reducible, inline]

abbrev List.lex_chains {α : Type u_1} (r : α → α → Prop) (l m : 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)