Counting Derivation Steps in CNF

This file tracks derivation lengths for grammars already in Chomsky normal form.

Main declarations

• derives_iff_derivesIn
• mem_language_iff_derivesIn
• DerivesIn.append_split

inductive ChomskyNormalFormGrammar.DerivesIn {T : Type uT} (g : ChomskyNormalFormGrammar 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 : ChomskyNormalFormGrammar T} (w : List (Symbol T g.NT)) : g.DerivesIn w w 0

  0 steps entail no transformation

• tail {T : Type uT} {g : ChomskyNormalFormGrammar 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 ChomskyNormalFormGrammar.derives_iff_derivesIn {T : Type uT} (g : ChomskyNormalFormGrammar T) (v w : List (Symbol T g.NT)) : g.Derives v w ↔ ∃ (n : ℕ), g.DerivesIn v w n

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

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

theorem ChomskyNormalFormGrammar.DerivesIn.zero_steps_eq {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v : List (Symbol T g.NT)} (huv : g.DerivesIn u v 0) : u = v

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

theorem ChomskyNormalFormGrammar.DerivesIn.trans_produces {T : Type uT} {g : ChomskyNormalFormGrammar 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 ChomskyNormalFormGrammar.DerivesIn.trans {T : Type uT} {g : ChomskyNormalFormGrammar 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 ChomskyNormalFormGrammar.Produces.trans_derivesIn {T : Type uT} {g : ChomskyNormalFormGrammar 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 ChomskyNormalFormGrammar.DerivesIn.tail_of_succ {T : Type uT} {g : ChomskyNormalFormGrammar 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 ChomskyNormalFormGrammar.DerivesIn.head_of_succ {T : Type uT} {g : ChomskyNormalFormGrammar 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 ChomskyNormalFormGrammar.DerivesIn.append_left {T : Type uT} {g : ChomskyNormalFormGrammar 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 ChomskyNormalFormGrammar.DerivesIn.append_right {T : Type uT} {g : ChomskyNormalFormGrammar 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 ChomskyNormalFormGrammar.DerivesIn.append_split {T : Type uT} {g : ChomskyNormalFormGrammar 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 ChomskyNormalFormGrammar.DerivesIn.three_split {T : Type uT} {g : ChomskyNormalFormGrammar 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 ChomskyNormalFormGrammar.DerivesIn.head_induction_on {T : Type uT} {g : ChomskyNormalFormGrammar 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