Langlib.Automata.Pushdown.Basics.CountingStepsLeftmost

inductive ContextFreeGrammar.DerivesLeftmostIn {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.DerivesLeftmostIn 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.DerivesLeftmostIn w w 0
tail {T : Type uT} {g : ContextFreeGrammar T} (u v w : List (Symbol T g.NT)) (n : ℕ) : g.DerivesLeftmostIn u v n → g.ProducesLeftmost v w → g.DerivesLeftmostIn u w n.succ

Instances For

source

theorem ContextFreeGrammar.derivesLeftmost_iff_derivesLeftmostIn {T : Type uT} (g : ContextFreeGrammar T) (v w : List (Symbol T g.NT)) :

g.DerivesLeftmost v w ↔ ∃ (n : ℕ), g.DerivesLeftmostIn v w n

source

theorem ContextFreeGrammar.mem_language_iff_derivesLeftmostIn {T : Type uT} (g : ContextFreeGrammar T) (w : List T) :

w ∈ g.language ↔ ∃ (n : ℕ), g.DerivesLeftmostIn [Symbol.nonterminal g.initial] (List.map Symbol.terminal w) n

source

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

g.DerivesLeftmostIn w w 0

source

theorem ContextFreeGrammar.DerivesLeftmostIn.zero {T : Type uT} {g : ContextFreeGrammar T} {w v : List (Symbol T g.NT)} (h : g.DerivesLeftmostIn w v 0) :

v = w

source

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

g.DerivesLeftmostIn v w 1

source

theorem ContextFreeGrammar.DerivesLeftmostIn.trans_producesLeftmost {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {u v w : List (Symbol T g.NT)} (huv : g.DerivesLeftmostIn u v n) (hvw : g.ProducesLeftmost v w) :

g.DerivesLeftmostIn u w n.succ

source

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

g.DerivesLeftmostIn u w (n + m)

source

theorem ContextFreeGrammar.ProducesLeftmost.trans_derivesLeftmostIn {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {u v w : List (Symbol T g.NT)} (huv : g.ProducesLeftmost u v) (hvw : g.DerivesLeftmostIn v w n) :

g.DerivesLeftmostIn u w n.succ

source

theorem ContextFreeGrammar.DerivesLeftmostIn.tail_of_succ {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {u w : List (Symbol T g.NT)} (huw : g.DerivesLeftmostIn u w n.succ) :

∃ (v : List (Symbol T g.NT)), g.DerivesLeftmostIn u v n ∧ g.ProducesLeftmost v w

source

theorem ContextFreeGrammar.DerivesLeftmostIn.head_of_succ {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {u w : List (Symbol T g.NT)} (huw : g.DerivesLeftmostIn u w n.succ) :

∃ (v : List (Symbol T g.NT)), g.ProducesLeftmost u v ∧ g.DerivesLeftmostIn v w n

source

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

g.DerivesLeftmostIn (List.map Symbol.terminal p ++ v) (List.map Symbol.terminal p ++ w) n

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

source

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

g.DerivesLeftmostIn (v ++ p) (w ++ p) n

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

source

theorem ContextFreeGrammar.DerivesLeftmostIn.empty {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {v : List (Symbol T g.NT)} (h : g.DerivesLeftmostIn [] v n) :

v = []

source

theorem ContextFreeGrammar.DerivesLeftmostIn.terminal {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {v : List (Symbol T g.NT)} {x : List T} (h : g.DerivesLeftmostIn (List.map Symbol.terminal x) v n) :

v = List.map Symbol.terminal x

source

theorem ContextFreeGrammar.derivesLeftmostIn_cons {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {x : Symbol T g.NT} {v u : List (Symbol T g.NT)} (h : g.DerivesLeftmostIn (x :: v) u n) :

(∃ (u' : List (Symbol T g.NT)), u = u' ++ v ∧ g.DerivesLeftmostIn [x] u' n) ∨ ∃ (w₁ : List T) (u₂ : List (Symbol T g.NT)) (m₁ : ℕ) (m₂ : ℕ), m₁ ≤ n ∧ m₂ ≤ n ∧ u = List.map Symbol.terminal w₁ ++ u₂ ∧ g.DerivesLeftmostIn [x] (List.map Symbol.terminal w₁) m₁ ∧ g.DerivesLeftmostIn v u₂ m₂

source

theorem ContextFreeGrammar.derivesLeftmostIn_cons' {T : Type uT} {g : ContextFreeGrammar T} {n : ℕ} {x : Symbol T g.NT} {v : List (Symbol T g.NT)} {u : List T} (h : g.DerivesLeftmostIn (x :: v) (List.map Symbol.terminal u) n) :

∃ (w₁ : List T) (w₂ : List T) (m₁ : ℕ) (m₂ : ℕ), m₁ ≤ n ∧ m₂ ≤ n ∧ u = w₁ ++ w₂ ∧ g.DerivesLeftmostIn [x] (List.map Symbol.terminal w₁) m₁ ∧ g.DerivesLeftmostIn v (List.map Symbol.terminal w₂) m₂