Parse certificates for indexed normal form

This file gives a depth-first certificate relation for singleton terminal derivations from a normal-form indexed grammar. The constructors mirror the four normal-form rule shapes and are proved equivalent to the existing counted derivation semantics.

inductive IndexedGrammar.NFYield {T : Type} (g : IndexedGrammar T) : g.nt → List g.flag → List T → Prop

A structural certificate that one indexed nonterminal with a concrete stack yields a terminal word using normal-form rule shapes.

• binary {T : Type} {g : IndexedGrammar T} {A B C : g.nt} {σ : List g.flag} {u v : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]) (hleft : g.NFYield B σ u) (hright : g.NFYield C σ v) : g.NFYield A σ (u ++ v)
• pop {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} {ρ : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = some f) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none]) (hrest : g.NFYield B ρ w) : g.NFYield A (f :: ρ) w
• push {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} {σ : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]) (hrest : g.NFYield B (f :: σ) w) : g.NFYield A σ w
• terminal {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {a : T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.terminal a]) : g.NFYield A σ [a]

theorem IndexedGrammar.NFYield.yield_length_pos {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (h : g.NFYield A σ w) : 0 < w.length

Every normal-form parse certificate has a nonempty terminal yield.

theorem IndexedGrammar.NFYield.transforms_binary_of_rule {T : Type} {g : IndexedGrammar T} {A B C : g.nt} {σ : List g.flag} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]) : g.Transforms [ISym.indexed A σ] [ISym.indexed B σ, ISym.indexed C σ]

theorem IndexedGrammar.NFYield.transforms_pop_of_rule {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} {ρ : List g.flag} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = some f) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none]) : g.Transforms [ISym.indexed A (f :: ρ)] [ISym.indexed B ρ]

theorem IndexedGrammar.NFYield.transforms_push_of_rule {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} {σ : List g.flag} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]) : g.Transforms [ISym.indexed A σ] [ISym.indexed B (f :: σ)]

theorem IndexedGrammar.NFYield.transforms_terminal_of_rule {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {a : T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.terminal a]) : g.Transforms [ISym.indexed A σ] [ISym.terminal a]

theorem IndexedGrammar.NFYield.exists_derivesIn {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (h : g.NFYield A σ w) : ∃ (n : ℕ), g.DerivesIn n [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w)

A parse certificate composes to a counted indexed-grammar derivation.

theorem IndexedGrammar.NFYield.of_derivesIn_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {n : ℕ} {A : g.nt} {σ : List g.flag} {w : List T} (hder : g.DerivesIn n [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w)) : g.NFYield A σ w

Every counted singleton terminal derivation in normal form has a parse certificate.

theorem IndexedGrammar.NFYield.iff_exists_derivesIn_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {A : g.nt} {σ : List g.flag} {w : List T} : g.NFYield A σ w ↔ ∃ (n : ℕ), g.DerivesIn n [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w)

Counted singleton terminal derivability in normal form is equivalent to existence of a parse certificate.

theorem IndexedGrammar.NFYield.generates_iff_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) {w : List T} : g.Generates w ↔ g.NFYield g.initial [] w