Pumping CFG Utilities

This file contains helper lemmas for repeated concatenation and derivation induction.

Main declarations

• nTimes_add
• nTimes_mul
• Derives.head_induction_on

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

Equations

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

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

Equations

• «term_^+^_» = Lean.ParserDescr.trailingNode `«term_^+^_» 69 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^+^ ") (Lean.ParserDescr.cat `term 70))

theorem nTimes_succ_l {α : Type u_1} {l : List α} {n : ℕ} : l ^+^ n.succ = l ++ l ^+^ n

theorem nTimes_succ_r {α : Type u_1} {l : List α} {n : ℕ} : l ^+^ n.succ = l ^+^ n ++ l

theorem nTimes_map {α : Type u_2} {l : List α} {n : ℕ} {β : Type u_1} {f : α → β} : List.map f l ^+^ n = List.map f (l ^+^ n)

theorem nTimes_add {α : Type u_1} {l : List α} {n m : ℕ} : l ^+^ (m + n) = l ^+^ m ++ l ^+^ n

theorem nTimes_mul {α : Type u_1} {l : List α} {n m : ℕ} : l ^+^ m * n = l ^+^ m ^+^ n

theorem ContextFreeGrammar.Derives.head_induction_on {T : Type uT} {g : ContextFreeGrammar T} {v : List (Symbol T g.NT)} {P : (u : List (Symbol T g.NT)) → g.Derives u v → Prop} {u : List (Symbol T g.NT)} (huv : g.Derives u v) (refl : P v ⋯) (head : ∀ {u w : List (Symbol T g.NT)} (huw : g.Produces u w) (hwv : g.Derives w v), P w hwv → P u ⋯) : P u huv