List Utilities

This file collects list lemmas and auxiliary definitions used in grammar constructions and derivation arguments.

Main declarations

• count_in_flatten
• mem_iff_nth_le
• nth_take
• nth_drop
• nth_append

def tacticIn_list_explicit : Lean.ParserDescr

Equations

• tacticIn_list_explicit = Lean.ParserDescr.node `tacticIn_list_explicit 1024 (Lean.ParserDescr.nonReservedSymbol "in_list_explicit" false)

def tacticSplit_ile : Lean.ParserDescr

Equations

• tacticSplit_ile = Lean.ParserDescr.node `tacticSplit_ile 1024 (Lean.ParserDescr.nonReservedSymbol "split_ile" false)

theorem List.length_append_append {α : Type u_1} {x y z : List α} : (x ++ y ++ z).length = x.length + y.length + z.length

theorem List.map_append_append {α : Type u_1} {β : Type u_2} {x y z : List α} {f : α → β} : map f (x ++ y ++ z) = map f x ++ map f y ++ map f z

theorem List.filter_map_append_append {α : Type u_1} {β : Type u_2} {x y z : List α} {f : α → Option β} : filterMap f (x ++ y ++ z) = filterMap f x ++ filterMap f y ++ filterMap f z

theorem List.reverse_append_append {α : Type u_1} {x y z : List α} : (x ++ y ++ z).reverse = z.reverse ++ y.reverse ++ x.reverse

theorem List.forall_mem_append_append {α : Type u_1} {x y z : List α} {p : α → Prop} : (∀ a ∈ x ++ y ++ z, p a) ↔ (∀ a ∈ x, p a) ∧ (∀ a ∈ y, p a) ∧ ∀ a ∈ z, p a

theorem List.replicate_succ_eq_singleton_append {α : Type u_1} (s : α) (n : ℕ) : replicate n.succ s = [s] ++ replicate n s

theorem List.replicate_succ_eq_append_singleton {α : Type u_1} (s : α) (n : ℕ) : replicate n.succ s = replicate n s ++ [s]

def List.n_times {α : Type u_1} (l : List α) (n : ℕ) : List α

Equations

• l ^ n = (List.replicate n l).flatten

def List.«term_^_» : Lean.TrailingParserDescr

Equations

• List.«term_^_» = Lean.ParserDescr.trailingNode `List.«term_^_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^ ") (Lean.ParserDescr.cat `term 101))

def List.count_in {α : Type u_1} [DecidableEq α] (l : List α) (a : α) : ℕ

Equations

• l.count_in a = (List.map (fun (s : α) => if s = a then 1 else 0) l).sum

theorem List.count_in_nil {α : Type u_1} [DecidableEq α] (a : α) : [].count_in a = 0

theorem List.count_in_cons {α : Type u_1} {x : List α} [DecidableEq α] (a b : α) : (b :: x).count_in a = (if b = a then 1 else 0) + x.count_in a

theorem List.count_in_append {α : Type u_1} {x y : List α} [DecidableEq α] (a : α) : (x ++ y).count_in a = x.count_in a + y.count_in a

theorem List.count_in_replicate_eq {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) : (replicate n a).count_in a = n

theorem List.count_in_replicate_neq {α : Type u_1} [DecidableEq α] {a b : α} (hyp : a ≠ b) (n : ℕ) : (replicate n a).count_in b = 0

theorem List.count_in_singleton_eq {α : Type u_1} [DecidableEq α] (a : α) : [a].count_in a = 1

theorem List.count_in_singleton_neq {α : Type u_1} [DecidableEq α] {a b : α} (hyp : a ≠ b) : [a].count_in b = 0

theorem List.count_in_pos_of_in {α : Type u_1} {x : List α} [DecidableEq α] {a : α} (hyp : a ∈ x) : x.count_in a > 0

theorem List.count_in_zero_of_notin {α : Type u_1} {x : List α} [DecidableEq α] {a : α} (hyp : a ∉ x) : x.count_in a = 0

theorem List.count_in_flatten {α : Type u_1} [DecidableEq α] (L : List (List α)) (a : α) : L.flatten.count_in a = (map (fun (w : List α) => w.count_in a) L).sum

theorem split_at_separator {α : Type} {a b u mid v : List α} {sep : α} (h_sep_not_in_mid : sep ∉ mid) (h_eq : a ++ [sep] ++ b = u ++ mid ++ v) : (∃ (u' : List α), a = u ++ mid ++ u' ∧ v = u' ++ [sep] ++ b) ∨ ∃ (v' : List α), u = a ++ [sep] ++ v' ∧ b = v' ++ mid ++ v

If a ++ [sep] ++ b = u ++ mid ++ v and sep ∉ mid, then the separator falls either entirely within a or entirely within b.

theorem head_unique_elem {α : Type} {s : List α} {elem : α} {u rest : List α} (_h_head : s = elem :: s.tail) (h_not_in_tail : elem ∉ s.tail) (h_eq : s = u ++ [elem] ++ rest) : u = []

If elem appears only at the head of s, and s = u ++ [elem] ++ rest, then u = [].

def List.nth {α : Type} (l : List α) (n : ℕ) : Option α

Equations

• [].nth n = none
• (a :: tail).nth 0 = some a
• (head :: tail).nth k.succ = tail.nth k

def List.nthLe {α : Type} (l : List α) (n : ℕ) : n < l.length → α

Equations

• [].nthLe x x_1 = ⋯.elim
• (a :: tail).nthLe 0 x_3 = a
• (head :: tail).nthLe n.succ h = tail.nthLe n ⋯

theorem List.get?_eq_nth {α : Type} {l : List α} {n : ℕ} : l[n]? = l.nth n

theorem List.nthLe_nth {α : Type} {l : List α} {n : ℕ} (h : n < l.length) : l.nth n = some (l.nthLe n h)

theorem List.nthLe_mem {α : Type} {l : List α} {n : ℕ} (h : n < l.length) : l.nthLe n h ∈ l

theorem List.nthLe_map {α β : Type} {f : α → β} {l : List α} {n : ℕ} (h : n < (map f l).length) : (map f l).nthLe n h = f (l.nthLe n ⋯)

theorem List.nthLe_append_right {α : Type} {l₁ l₂ : List α} {n : ℕ} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : (l₁ ++ l₂).nthLe n h₂ = l₂.nthLe (n - l₁.length) ⋯

theorem List.nthLe_congr {α : Type} {l : List α} {n : ℕ} {h₁ h₂ : n < l.length} : l.nthLe n h₁ = l.nthLe n h₂

theorem List.nthLe_of_eq {α : Type} {l₁ l₂ : List α} (h : l₁ = l₂) {n : ℕ} (hn : n < l₁.length) : l₁.nthLe n hn = l₂.nthLe n ⋯

theorem List.nthLe_append {α : Type} {l₁ l₂ : List α} {n : ℕ} (h₁ : n < l₁.length) (h₂ : n < (l₁ ++ l₂).length) : (l₁ ++ l₂).nthLe n h₂ = l₁.nthLe n h₁

theorem List.nthLe_of_mem {α : Type} {l : List α} {a : α} (h : a ∈ l) : ∃ (n : ℕ) (h' : n < l.length), l.nthLe n h' = a

theorem List.nthLe_replicate {α : Type} (a : α) {n i : ℕ} (h : i < (replicate n a).length) : (replicate n a).nthLe i h = a

theorem List.nth_eq_none_iff {α : Type} {l : List α} {n : ℕ} : l.nth n = none ↔ l.length ≤ n

theorem List.nth_take {α : Type} {l : List α} {m n : ℕ} (h : n < m) : (take m l).nth n = l.nth n

theorem List.nth_drop {α : Type} {l : List α} {m n : ℕ} : (drop m l).nth n = l.nth (m + n)

theorem List.nth_append_right {α : Type} {l₁ l₂ : List α} {n : ℕ} (h : l₁.length ≤ n) : (l₁ ++ l₂).nth n = l₂.nth (n - l₁.length)

theorem List.nth_append {α : Type} {l₁ l₂ : List α} {n : ℕ} (h : n < l₁.length) : (l₁ ++ l₂).nth n = l₁.nth n