Interleaving lists

This file defines interleaving of lists as an operation.

@[irreducible]

def List.interleave {α : Type u_1} : List α → List α → List α

Interleave two lists l₁ and l₂, starting with an element of l₁.

This operation fully interleave the two lists when the length of l₁ is either the length of l₂ or one more. If one of the lists runs out early, the remainder of the other list is kept without further interleaving, so that l₁.interleave l₂ is always a permutation of l₁ ++ l₂. See interleave_perm_append.

#eval interleave [0, 2, 4] [1] -- [0, 1, 2, 4] -- The second list is too short
#eval interleave [0, 2, 4] [1, 3] -- [0, 1, 2, 3, 4]
#eval interleave [0, 2] [1, 3] -- [0, 1, 2, 3]
#eval interleave [0] [1, 3] -- [0, 1, 3] -- The first list is too short

Equations

• [].interleave x✝ = x✝
• (a :: l₁).interleave x✝ = a :: x✝.interleave l₁

@[simp]

theorem List.nil_interleave {α : Type u_1} (l₂ : List α) : [].interleave l₂ = l₂

@[simp]

theorem List.interleave_nil {α : Type u_1} (l₁ : List α) : l₁.interleave [] = l₁

@[simp]

theorem List.cons_interleave {α : Type u_1} (a : α) (l₁ l₂ : List α) : (a :: l₁).interleave l₂ = a :: l₂.interleave l₁

@[simp]

theorem List.interleave_perm_append {α : Type u_1} {l₁ l₂ : List α} : (l₁.interleave l₂).Perm (l₁ ++ l₂)

@[simp]

theorem List.interleave_eq_nil {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁.interleave l₂ = [] ↔ l₁ = [] ∧ l₂ = []

theorem List.Perm.interleave {α✝ : Type u_1} {l₁ l₃ l₂ l₄ : List α✝} (h₁₃ : l₁.Perm l₃) (h₂₄ : l₂.Perm l₄) : (l₁.interleave l₂).Perm (l₃.interleave l₄)

@[simp]

theorem List.length_interleave {α : Type u_1} (l₁ l₂ : List α) : (l₁.interleave l₂).length = l₁.length + l₂.length

@[simp]

theorem List.countP_interleave {α : Type u_1} (l₁ l₂ : List α) (p : α → Bool) : countP p (l₁.interleave l₂) = countP p l₁ + countP p l₂

@[simp]

theorem List.count_interleave {α : Type u_1} [BEq α] (l₁ l₂ : List α) (a : α) : count a (l₁.interleave l₂) = count a l₁ + count a l₂

@[simp]

theorem List.interleave_append_append_of_length_eq_length {α : Type u_1} {l₁ l₂ : List α} (_h₁₂ : l₁.length = l₂.length) (l₃ l₄ : List α) : (l₁ ++ l₃).interleave (l₂ ++ l₄) = l₁.interleave l₂ ++ l₃.interleave l₄

@[simp]

theorem List.interleave_append_append_of_length_eq_length_add_one {α : Type u_1} {l₁ l₂ : List α} (_h₁₂ : l₁.length = l₂.length + 1) (l₃ l₄ : List α) : (l₁ ++ l₃).interleave (l₂ ++ l₄) = l₁.interleave l₂ ++ l₄.interleave l₃

@[simp]

theorem List.interleave_append_left {α : Type u_1} {l₁ l₂ : List α} (_h₂₁ : l₂.length ≤ l₁.length) (l₃ : List α) : (l₁ ++ l₃).interleave l₂ = l₁.interleave l₂ ++ l₃

@[simp]

theorem List.interleave_append_right {α : Type u_1} {l₁ l₂ : List α} (_h₁₂ : l₁.length ≤ l₂.length + 1) (l₃ : List α) : l₁.interleave (l₂ ++ l₃) = l₁.interleave l₂ ++ l₃

theorem List.interleave_flatten_flatten_of_length_eq_length {α : Type u_1} {L₁ L₂ : List (List α)} (h₁₂ : L₁.length = L₂.length) : (∀ (i : Nat) (hi : i + 1 < L₁.length), L₁[i].length = L₂[i].length) → L₁.flatten.interleave L₂.flatten = (zipWith interleave L₁ L₂).flatten

@[simp]

theorem List.reverse_interleave_of_length_eq_length {α : Type u_1} {l₁ l₂ : List α} : l₁.length = l₂.length → (l₁.interleave l₂).reverse = l₂.reverse.interleave l₁.reverse

@[simp]

theorem List.reverse_interleave_of_length_eq_length_add_one {α : Type u_1} {l₁ l₂ : List α} : l₁.length = l₂.length + 1 → (l₁.interleave l₂).reverse = l₁.reverse.interleave l₂.reverse

@[simp]

theorem List.interleave_ofFn_ofFn_even {α : Type u_1} {n : Nat} {f g : Fin n → α} : (ofFn f).interleave (ofFn g) = ofFn fun (i : Fin (2 * n)) => if ↑i % 2 = 0 then f ⟨↑i / 2, ⋯⟩ else g ⟨↑i / 2, ⋯⟩

theorem List.interleave_ofFn_ofFn_odd {α : Type u_1} {n : Nat} {f : Fin (n + 1) → α} {g : Fin n → α} : (ofFn f).interleave (ofFn g) = ofFn fun (i : Fin (2 * n + 1)) => if hi : ↑i % 2 = 0 then f ⟨↑i / 2, ⋯⟩ else g ⟨↑i / 2, ⋯⟩

@[simp]

theorem List.right_sublist_interleave {α : Type u_1} {l₁ l₂ : List α} : l₂.Sublist (l₁.interleave l₂)

@[simp]

theorem List.left_sublist_interleave {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁.Sublist (l₁.interleave l₂)

@[simp]

theorem List.IsPrefix.interleave {α✝ : Type u_1} {l₁ l₃ l₂ l₄ : List α✝} : l₁.length = l₂.length ∨ l₁.length = l₂.length + 1 → l₁ <+: l₃ → l₂ <+: l₄ → l₁.interleave l₂ <+: l₃.interleave l₄