Interleaving lists

This file defines interleaving of lists as a relation.

See also

Interleaving of lists as an operation is defined in Batteries/Data/List/Interleave.lean.

inductive List.Interleaves {α : Type u_1} (r : α → α → Prop) : List α → List α → Prop

Relation for interleaving lists. l₁.Interleaves l₂ r means that l₁ r-interleaves l₂, i.e. the length of l₂ is either the length of l₁ or one more and for each i the i-th rightmost element of l₁ is r-related to both the i-th and i + 1-st rightmost elements of l₂, except possibly when i = l₁.length.

For example, [1, 3] (· ≤ ·)-interleaves both of [0, 2, 4] and [0, 2].

See interleaves_iff_length_isChain_interleave for the connection with List.interleave.

• nil_nil {α : Type u_1} {r : α → α → Prop} : Interleaves r [] []

  The empty list interleaves itself.

• nil_singleton {α : Type u_1} {r : α → α → Prop} (a : α) : Interleaves r [] [a]

  The empty list interleaves any singleton list.

• cons_symm {α : Type u_1} {r : α → α → Prop} ⦃a b : α⦄ (hab : r a b) ⦃l₁ l₂ : List α⦄ (hl : Interleaves r l₁ (b :: l₂)) : Interleaves r (b :: l₂) (a :: l₁)

  If l₁ interleaves b :: l₂ and a is related to b, then b :: l₂ interleaves a :: l₁.

theorem List.interleaves_iff {α : Type u_1} (r : α → α → Prop) (a✝ a✝¹ : List α) : Interleaves r a✝ a✝¹ ↔ a✝ = [] ∧ a✝¹ = [] ∨ (∃ (a : α), a✝ = [] ∧ a✝¹ = [a]) ∨ ∃ (a : α) (b : α), r a b ∧ ∃ (l₁ : List α) (l₂ : List α), Interleaves r l₁ (b :: l₂) ∧ a✝ = b :: l₂ ∧ a✝¹ = a :: l₁

@[simp]

theorem List.interleaves_nil_cons {α : Type u_1} {r : α → α → Prop} {l : List α} {a : α} : Interleaves r [] (a :: l) ↔ l = []

@[simp]

theorem List.not_interleaves_cons_nil {α : Type u_1} {r : α → α → Prop} {l : List α} {a : α} : ¬Interleaves r (a :: l) []

@[simp]

theorem List.interleaves_cons_cons {α : Type u_1} {r : α → α → Prop} {l₁ l₂ : List α} {a b : α} : Interleaves r (a :: l₁) (b :: l₂) ↔ r b a ∧ Interleaves r l₂ (a :: l₁)

@[simp]

theorem List.interleaves_singleton_singleton {α : Type u_1} {r : α → α → Prop} {a b : α} : Interleaves r [a] [b] ↔ r b a

theorem List.Interleaves.mono {α : Type u_1} {r s : α → α → Prop} (hrs : ∀ ⦃a b : α⦄, r a b → s a b) (l₁ l₂ : List α) : Interleaves r l₁ l₂ → Interleaves s l₁ l₂

theorem List.interleaves_iff_length_isChain_interleave {α : Type u_1} {r : α → α → Prop} {l₁ l₂ : List α} : Interleaves r l₁ l₂ ↔ l₁.length ⩿ l₂.length ∧ IsChain r (l₂.interleave l₁)

@[simp]

theorem List.interleaves_append_singleton_append_singleton_of_length_eq_length {α : Type u_1} {r : α → α → Prop} {l₁ l₂ : List α} {a b : α} (h : l₁.length = l₂.length) : Interleaves r (l₁ ++ [a]) (l₂ ++ [b]) ↔ r b a ∧ Interleaves r l₁ (l₂ ++ [b])

@[simp]

theorem List.interleaves_append_singleton_append_singleton_of_length_eq_length_add_one {α : Type u_1} {r : α → α → Prop} {l₁ l₂ : List α} {a b : α} (h : l₁.length + 1 = l₂.length) : Interleaves r (l₁ ++ [a]) (l₂ ++ [b]) ↔ r a b ∧ Interleaves r (l₁ ++ [a]) l₂

theorem List.interleaves_reverse_reverse_of_length_eq_length {α : Type u_1} {r : α → α → Prop} {l₁ l₂ : List α} (h : l₁.length = l₂.length) : Interleaves r l₁.reverse l₂.reverse ↔ Interleaves (Function.swap r) l₂ l₁

theorem List.interleaves_reverse_reverse_of_length_eq_length_add_one {α : Type u_1} {r : α → α → Prop} {l₁ l₂ : List α} (h : l₁.length + 1 = l₂.length) : Interleaves r l₁.reverse l₂.reverse ↔ Interleaves (Function.swap r) l₁ l₂

theorem List.interleaves_ofFn_even {α : Type u_1} {r : α → α → Prop} {n : ℕ} {f g : Fin n → α} : Interleaves r (ofFn f) (ofFn g) ↔ (∀ (i : Fin n), r (g i) (f i)) ∧ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (g ⟨i + 1, hi⟩)

theorem List.interleaves_ofFn_odd {α : Type u_1} {r : α → α → Prop} {n : ℕ} {f : Fin n → α} {g : Fin (n + 1) → α} : Interleaves r (ofFn f) (ofFn g) ↔ (∀ (i : Fin n), r (f i) (g i.succ)) ∧ ∀ (i : Fin n), r (g i.castSucc) (f i)

theorem List.Interleaves.pairwise_left {α : Type u_1} {r : α → α → Prop} {l₁ l₂ : List α} [IsTrans α r] (hl : Interleaves r l₁ l₂) : Pairwise r l₁

theorem List.Interleaves.pairwise_right {α : Type u_1} {r : α → α → Prop} {l₁ l₂ : List α} [IsTrans α r] (hl : Interleaves r l₁ l₂) : Pairwise r l₂