Data-carrying normal-form indexed parse certificates

IndexedGrammar.NFYield is intentionally proposition-valued. Aho's marked simulation must, however, follow individual pushed flag occurrences through one chosen parse. Proof irrelevance means that this information cannot soundly be indexed by an NFYield proof itself, so this file introduces the parallel Type-valued certificate NFParse.

Every NFYield proposition has a nonempty NFParse type, and every NFParse erases back to an NFYield proof. We then define whether one root-stack occurrence is consumed in that concrete parse and prove that an occurrence which is not consumed can be erased throughout the tree.

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

A data-carrying version of NFYield. Its constructors have exactly the four normal-form rule shapes, but the result lives in Type so later algorithms may inspect the chosen tree.

• 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]) (left : g.NFParse B σ u) (right : g.NFParse C σ v) : g.NFParse 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]) (rest : g.NFParse B ρ w) : g.NFParse 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)]) (rest : g.NFParse B (f :: σ) w) : g.NFParse 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.NFParse A σ [a]

def IndexedGrammar.NFParse.toNFYield {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} : ∀ (a : g.NFParse A σ w), g.NFYield A σ w

Forget the data-carrying tree and retain the proposition-valued certificate.

Equations

• ⋯ = ⋯

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

Every data-carrying normal-form parse has a nonempty terminal yield.

theorem IndexedGrammar.NFParse.nonempty_of_nfyield {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (h : g.NFYield A σ w) : Nonempty (g.NFParse A σ w)

Every proposition-valued normal-form parse has a data-carrying representative.

noncomputable def IndexedGrammar.NFParse.ofNFYield {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (h : g.NFYield A σ w) : g.NFParse A σ w

Choose a concrete data-carrying representative of an NFYield proof.

Equations

• IndexedGrammar.NFParse.ofNFYield h = Classical.choice ⋯

theorem IndexedGrammar.NFParse.nonempty_iff_nfyield {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} : Nonempty (g.NFParse A σ w) ↔ g.NFYield A σ w

The data-carrying and proposition-valued certificate presentations are equivalent.

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

At the initial nonterminal, concrete parse trees characterize normal-form generation.

def IndexedGrammar.NFParse.ConsumesAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (p : g.NFParse A σ w) (k : ℕ) : Prop

ConsumesAt p k says that some pop in the concrete parse p consumes the occurrence initially at root-stack position k (positions start at zero).

Equations

• (IndexedGrammar.NFParse.binary hr hlhs hc hrhs left right).ConsumesAt k = (left.ConsumesAt k ∨ right.ConsumesAt k)
• (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest).ConsumesAt k = (k = 0 ∨ rest.ConsumesAt (k - 1))
• (IndexedGrammar.NFParse.push hr hlhs hc hrhs rest).ConsumesAt k = rest.ConsumesAt (k + 1)
• (IndexedGrammar.NFParse.terminal hr hlhs hc hrhs).ConsumesAt k = False

@[simp]

theorem IndexedGrammar.NFParse.consumesAt_binary_iff {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]) (left : g.NFParse B σ u) (right : g.NFParse C σ v) (k : ℕ) : (binary hr hlhs hc hrhs left right).ConsumesAt k ↔ left.ConsumesAt k ∨ right.ConsumesAt k

@[simp]

theorem IndexedGrammar.NFParse.consumesAt_pop_zero {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]) (rest : g.NFParse B ρ w) : (pop hr hlhs hc hrhs rest).ConsumesAt 0

@[simp]

theorem IndexedGrammar.NFParse.consumesAt_pop_succ_iff {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]) (rest : g.NFParse B ρ w) (k : ℕ) : (pop hr hlhs hc hrhs rest).ConsumesAt (k + 1) ↔ rest.ConsumesAt k

@[simp]

theorem IndexedGrammar.NFParse.consumesAt_push_iff {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)]) (rest : g.NFParse B (f :: σ) w) (k : ℕ) : (push hr hlhs hc hrhs rest).ConsumesAt k ↔ rest.ConsumesAt (k + 1)

@[simp]

theorem IndexedGrammar.NFParse.not_consumesAt_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]) (k : ℕ) : ¬(terminal hr hlhs hc hrhs).ConsumesAt k

def IndexedGrammar.NFParse.eraseIdxOfNotConsumesAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (p : g.NFParse A σ w) (k : ℕ) (unused : ¬p.ConsumesAt k) : g.NFParse A (σ.eraseIdx k) w

Erase an inherited occurrence which is never consumed in a concrete parse.

Equations

• One or more equations did not get rendered due to their size.
• (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest).eraseIdxOfNotConsumesAt 0 unused_3 = ⋯.elim
• (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest).eraseIdxOfNotConsumesAt k_2.succ unused_3 = IndexedGrammar.NFParse.pop hr hlhs hc hrhs (rest.eraseIdxOfNotConsumesAt k_2 ⋯)
• (IndexedGrammar.NFParse.push hr hlhs hc hrhs rest).eraseIdxOfNotConsumesAt k unused_2 = IndexedGrammar.NFParse.push hr hlhs hc hrhs (rest.eraseIdxOfNotConsumesAt (k + 1) unused_2)
• (IndexedGrammar.NFParse.terminal hr hlhs hc hrhs).eraseIdxOfNotConsumesAt k unused_2 = IndexedGrammar.NFParse.terminal hr hlhs hc hrhs

theorem IndexedGrammar.NFParse.nfyield_eraseIdx_of_not_consumesAt {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (p : g.NFParse A σ w) (k : ℕ) (unused : ¬p.ConsumesAt k) : g.NFYield A (σ.eraseIdx k) w

Proposition-level corollary of eraseIdxOfNotConsumesAt.

Productive-node accounting

def IndexedGrammar.NFParse.terminalCount {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} : g.NFParse A σ w → ℕ

The number of terminal leaves in a concrete normal-form parse.

Equations

• (IndexedGrammar.NFParse.binary hr hlhs hc hrhs left right).terminalCount = left.terminalCount + right.terminalCount
• (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest).terminalCount = rest.terminalCount
• (IndexedGrammar.NFParse.push hr hlhs hc hrhs rest).terminalCount = rest.terminalCount
• (IndexedGrammar.NFParse.terminal hr hlhs hc hrhs).terminalCount = 1

def IndexedGrammar.NFParse.binaryCount {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} : g.NFParse A σ w → ℕ

The number of binary nodes in a concrete normal-form parse.

Equations

• (IndexedGrammar.NFParse.binary hr hlhs hc hrhs left right).binaryCount = left.binaryCount + right.binaryCount + 1
• (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest).binaryCount = rest.binaryCount
• (IndexedGrammar.NFParse.push hr hlhs hc hrhs rest).binaryCount = rest.binaryCount
• (IndexedGrammar.NFParse.terminal hr hlhs hc hrhs).binaryCount = 0

def IndexedGrammar.NFParse.productiveCount {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (p : g.NFParse A σ w) : ℕ

Productive events are binary expansions and terminal emissions.

Equations

• p.productiveCount = p.binaryCount + p.terminalCount

@[simp]

theorem IndexedGrammar.NFParse.terminalCount_eq_yield_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (p : g.NFParse A σ w) : p.terminalCount = w.length

Terminal leaves count the length of the yield exactly.

theorem IndexedGrammar.NFParse.binaryCount_add_one_eq_terminalCount {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (p : g.NFParse A σ w) : p.binaryCount + 1 = p.terminalCount

A nonempty full binary parse has one fewer binary nodes than terminal leaves.

theorem IndexedGrammar.NFParse.productiveCount_le_twice_yield_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} {w : List T} (p : g.NFParse A σ w) : p.productiveCount ≤ 2 * w.length

The number of productive events is at most twice the terminal yield length.