Extra lemmas about context-free grammars

Additions to Mathlib.Computability.ContextFreeGrammar from the authors' in-review Mathlib branch (alex-loitzl-cnf) that are not yet available in the Mathlib release pinned here: the step-counting derivation relation ContextFreeGrammar.DerivesIn with its induction principles and splitting lemmas, plus a few facts about ContextFreeGrammar.Produces.

theorem ContextFreeGrammar.Produces.input_output {T : Type uT} {g : ContextFreeGrammar T} {r : ContextFreeRule T g.NT} (hrg : r ∈ g.rules) : g.Produces [Symbol.nonterminal r.input] r.output

theorem ContextFreeGrammar.Produces.rule {T : Type uT} {g : ContextFreeGrammar T} {n : g.NT} {u : List (Symbol T g.NT)} (hnu : g.Produces [Symbol.nonterminal n] u) : { input := n, output := u } ∈ g.rules

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

Alternative definition of ContextFreeGrammar.Derives which allows to use well-founded induction on derivations, by explicitely counting the number of steps of the transformation

inductive ContextFreeGrammar.DerivesIn {T : Type uT} (g : ContextFreeGrammar T) : List (Symbol T g.NT) → List (Symbol T g.NT) → ℕ → Prop

Given a context-free grammar g, strings u and v, and number n g.DerivesIn u v n means that g can transform u to v in n rewriting steps.

• refl {T : Type uT} {g : ContextFreeGrammar T} (w : List (Symbol T g.NT)) : g.DerivesIn w w 0

  0 steps entail no transformation

• tail {T : Type uT} {g : ContextFreeGrammar T} (u v w : List (Symbol T g.NT)) (n : ℕ) : g.DerivesIn u v n → g.Produces v w → g.DerivesIn u w n.succ

  n + 1 steps, if transforms u to v in n steps, and v to w in 1 step

theorem ContextFreeGrammar.derives_iff_derivesIn {T : Type uT} (g : ContextFreeGrammar T) (v w : List (Symbol T g.NT)) : g.Derives v w ↔ ∃ (n : ℕ), g.DerivesIn v w n

theorem ContextFreeGrammar.mem_language_iff_derivesIn {T : Type uT} (g : ContextFreeGrammar T) (w : List T) : w ∈ g.language ↔ ∃ (n : ℕ), g.DerivesIn [Symbol.nonterminal g.initial] (List.map Symbol.terminal w) n

theorem ContextFreeGrammar.DerivesIn.zero_steps {T : Type uT} {g : ContextFreeGrammar T} (w : List (Symbol T g.NT)) : g.DerivesIn w w 0

theorem ContextFreeGrammar.Produces.single_step {T : Type uT} {g : ContextFreeGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.Produces v w) : g.DerivesIn v w 1

theorem ContextFreeGrammar.DerivesIn.trans_produces {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {u v w : List (Symbol T g.NT)} (huv : g.DerivesIn u v n) (hvw : g.Produces v w) : g.DerivesIn u w n.succ

theorem ContextFreeGrammar.DerivesIn.trans {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {u v w : List (Symbol T g.NT)} {m : ℕ} (huv : g.DerivesIn u v n) (hvw : g.DerivesIn v w m) : g.DerivesIn u w (n + m)

theorem ContextFreeGrammar.Produces.trans_derivesIn {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {u v w : List (Symbol T g.NT)} (huv : g.Produces u v) (hvw : g.DerivesIn v w n) : g.DerivesIn u w n.succ

theorem ContextFreeGrammar.DerivesIn.tail_of_succ {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {u w : List (Symbol T g.NT)} (huw : g.DerivesIn u w n.succ) : ∃ (v : List (Symbol T g.NT)), g.DerivesIn u v n ∧ g.Produces v w

theorem ContextFreeGrammar.DerivesIn.head_of_succ {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {u w : List (Symbol T g.NT)} (huw : g.DerivesIn u w n.succ) : ∃ (v : List (Symbol T g.NT)), g.Produces u v ∧ g.DerivesIn v w n

theorem ContextFreeGrammar.DerivesIn.append_left {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {v w : List (Symbol T g.NT)} (hvw : g.DerivesIn v w n) (p : List (Symbol T g.NT)) : g.DerivesIn (p ++ v) (p ++ w) n

Add extra prefix to context-free deriving (number of steps unchanged).

theorem ContextFreeGrammar.DerivesIn.append_right {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {v w : List (Symbol T g.NT)} (hvw : g.DerivesIn v w n) (p : List (Symbol T g.NT)) : g.DerivesIn (v ++ p) (w ++ p) n

Add extra postfix to context-free deriving (number of steps unchanged).

theorem ContextFreeGrammar.DerivesIn.append_split {T : Type uT} {g : ContextFreeGrammar T} {p q w : List (Symbol T g.NT)} {n : ℕ} (hpqw : g.DerivesIn (p ++ q) w n) : ∃ (x : List (Symbol T g.NT)) (y : List (Symbol T g.NT)) (m₁ : ℕ) (m₂ : ℕ), w = x ++ y ∧ g.DerivesIn p x m₁ ∧ g.DerivesIn q y m₂ ∧ n = m₁ + m₂

theorem ContextFreeGrammar.DerivesIn.three_split {T : Type uT} {g : ContextFreeGrammar T} {p q r w : List (Symbol T g.NT)} {n : ℕ} (hg : g.DerivesIn (p ++ q ++ r) w n) : ∃ (x : List (Symbol T g.NT)) (y : List (Symbol T g.NT)) (z : List (Symbol T g.NT)) (m₁ : ℕ) (m₂ : ℕ) (m₃ : ℕ), w = x ++ y ++ z ∧ g.DerivesIn p x m₁ ∧ g.DerivesIn q y m₂ ∧ g.DerivesIn r z m₃ ∧ n = m₁ + m₂ + m₃

theorem ContextFreeGrammar.DerivesIn.head_induction_on {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {b : List (Symbol T g.NT)} {P : (n : ℕ) → (a : List (Symbol T g.NT)) → g.DerivesIn a b n → Prop} (refl : P 0 b ⋯) (head : ∀ {n : ℕ} {a c : List (Symbol T g.NT)} (hac : g.Produces a c) (hcb : g.DerivesIn c b n), P n c hcb → P n.succ a ⋯) {a : List (Symbol T g.NT)} (hab : g.DerivesIn a b n) : P n a hab