Langlib

Langlib.Classes.ContextFree.Pumping.CountingSteps

Counting Derivation Steps for CFGs #

This file refines context-free derivations by tracking the number of production steps.

Main declarations #

source
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.

Instances For
    source
    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
    source
    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
    source
    theorem ContextFreeGrammar.DerivesIn.zero_steps {T : Type uT} {g : ContextFreeGrammar T} (w : List (Symbol T g.NT)) :
    g.DerivesIn w w 0
    source
    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
    source
    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
    source
    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)
    source
    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
    source
    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
    source
    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
    source
    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).

    source
    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).

    source
    @[irreducible]
    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₂
    source
    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₃
    source
    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