Flag Separation for Indexed Grammars

This file constructs a flag-separation transformation for indexed grammars.

This is Step 4 of Aho's Normal Form theorem.

def IndexedGrammar.hasPush {T : Type} (g : IndexedGrammar T) : IRhsSymbol T g.nt g.flag → Bool

Does this RHS symbol have a flag push?

Equations

• g.hasPush (IRhsSymbol.nonterminal a (some val)) = true
• g.hasPush x✝ = false

def IndexedGrammar.fsLiftRhsSym {T : Type} (g : IndexedGrammar T) : IRhsSymbol T g.nt g.flag → IRhsSymbol T (g.nt ⊕ ℕ × ℕ) g.flag

Lift an RHS symbol to the new nonterminal type, keeping flags.

Equations

• g.fsLiftRhsSym (IRhsSymbol.terminal t) = IRhsSymbol.terminal t
• g.fsLiftRhsSym (IRhsSymbol.nonterminal n f) = IRhsSymbol.nonterminal (Sum.inl n) f

def IndexedGrammar.fsReplaceRhsSym {T : Type} (g : IndexedGrammar T) (ruleIdx posIdx : ℕ) : IRhsSymbol T g.nt g.flag → IRhsSymbol T (g.nt ⊕ ℕ × ℕ) g.flag

Replace a pushed nonterminal with a fresh intermediate (no push).

Equations

• g.fsReplaceRhsSym ruleIdx posIdx (IRhsSymbol.terminal t) = IRhsSymbol.terminal t
• g.fsReplaceRhsSym ruleIdx posIdx (IRhsSymbol.nonterminal n none) = IRhsSymbol.nonterminal (Sum.inl n) none
• g.fsReplaceRhsSym ruleIdx posIdx (IRhsSymbol.nonterminal a (some val)) = IRhsSymbol.nonterminal (Sum.inr (ruleIdx, posIdx)) none

def IndexedGrammar.fsStripPushRhsSym {T : Type} (g : IndexedGrammar T) : IRhsSymbol T g.nt g.flag → IRhsSymbol T (g.nt ⊕ ℕ × ℕ) g.flag

Strip flag push from an RHS symbol in the lifted type.

Equations

• g.fsStripPushRhsSym (IRhsSymbol.terminal t) = IRhsSymbol.terminal t
• g.fsStripPushRhsSym (IRhsSymbol.nonterminal n f) = IRhsSymbol.nonterminal (Sum.inl n) none

def IndexedGrammar.fsSingleRule {T : Type} (g : IndexedGrammar T) (i : ℕ) (r : IRule T g.nt g.flag) : List (IRule T (g.nt ⊕ ℕ × ℕ) g.flag)

Transform a single rule at index i into flag-separated rules.

Note: The consume check is done first (before the terminal check) to ensure that rules with consume = some and terminal RHS are properly separated. This is required for flagSeparate_flagsSeparated to hold.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev IndexedGrammar.flagSeparate {T : Type} (g : IndexedGrammar T) : IndexedGrammar T

The flag-separated grammar.

Equations

• One or more equations did not get rendered due to their size.

Properties

def IndexedGrammar.fsLiftISym {T : Type} (g : IndexedGrammar T) : g.ISym → g.flagSeparate.ISym

Lift a sentential-form symbol.

Equations

• g.fsLiftISym (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• g.fsLiftISym (IndexedGrammar.ISym.indexed n σ) = IndexedGrammar.ISym.indexed (Sum.inl n) σ

def IndexedGrammar.fsProjISym {T : Type} (g : IndexedGrammar T) : g.flagSeparate.ISym → g.ISym

Project a sentential-form symbol.

Equations

• g.fsProjISym (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• g.fsProjISym (IndexedGrammar.ISym.indexed (Sum.inl n) σ) = IndexedGrammar.ISym.indexed n σ
• g.fsProjISym (IndexedGrammar.ISym.indexed (Sum.inr val) σ) = IndexedGrammar.ISym.indexed g.initial σ

theorem IndexedGrammar.fsSingleRule_rhs_ne_nil {T : Type} (g : IndexedGrammar T) (i : ℕ) (r : IRule T g.nt g.flag) (hr : r.rhs ≠ []) (r' : IRule T (g.nt ⊕ ℕ × ℕ) g.flag) (hr' : r' ∈ g.fsSingleRule i r) : r'.rhs ≠ []

theorem IndexedGrammar.flagSeparate_noEpsilon {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') : g.flagSeparate.NoEpsilon'

theorem IndexedGrammar.fsReplaceRhsSym_nonterminal {T : Type} (g : IndexedGrammar T) (ri pi : ℕ) (n : g.nt) (f : Option g.flag) : ∃ (n' : g.nt ⊕ ℕ × ℕ) (f' : Option g.flag), g.fsReplaceRhsSym ri pi (IRhsSymbol.nonterminal n f) = IRhsSymbol.nonterminal n' f'

theorem IndexedGrammar.fsStripPushRhsSym_nonterminal {T : Type} (g : IndexedGrammar T) (n : g.nt) (f : Option g.flag) : ∃ (n' : g.nt ⊕ ℕ × ℕ), g.fsStripPushRhsSym (IRhsSymbol.nonterminal n f) = IRhsSymbol.nonterminal n' none

theorem IndexedGrammar.fsLiftRhsSym_nonterminal {T : Type} (g : IndexedGrammar T) (n : g.nt) (f : Option g.flag) : ∃ (n' : g.nt ⊕ ℕ × ℕ) (f' : Option g.flag), g.fsLiftRhsSym (IRhsSymbol.nonterminal n f) = IRhsSymbol.nonterminal n' f'

theorem IndexedGrammar.fsLiftRhsSym_terminal {T : Type} (g : IndexedGrammar T) (t : T) : g.fsLiftRhsSym (IRhsSymbol.terminal t) = IRhsSymbol.terminal t

theorem IndexedGrammar.fsReplaceRhsSym_map_all_nt {T : Type} (g : IndexedGrammar T) (ri : ℕ) (l : List (IRhsSymbol T g.nt g.flag)) (h : ∀ s ∈ l, ∃ (n : g.nt) (f : Option g.flag), s = IRhsSymbol.nonterminal n f) (s : IRhsSymbol T (g.nt ⊕ ℕ × ℕ) g.flag) : s ∈ List.map (fun (x : IRhsSymbol T g.nt g.flag × ℕ) => match x with | (s, j) => g.fsReplaceRhsSym ri j s) l.zipIdx → ∃ (n : g.nt ⊕ ℕ × ℕ) (f : Option g.flag), s = IRhsSymbol.nonterminal n f

theorem IndexedGrammar.fsLiftRhsSym_map_all_nt {T : Type} (g : IndexedGrammar T) (l : List (IRhsSymbol T g.nt g.flag)) (h : ∀ s ∈ l, ∃ (n : g.nt) (f : Option g.flag), s = IRhsSymbol.nonterminal n f) (s : IRhsSymbol T (g.nt ⊕ ℕ × ℕ) g.flag) : s ∈ List.map g.fsLiftRhsSym l → ∃ (n : g.nt ⊕ ℕ × ℕ) (f : Option g.flag), s = IRhsSymbol.nonterminal n f

theorem IndexedGrammar.fsStripPushRhsSym_map_all_nt {T : Type} (g : IndexedGrammar T) (l : List (IRhsSymbol T g.nt g.flag)) (h : ∀ s ∈ l, ∃ (n : g.nt) (f : Option g.flag), s = IRhsSymbol.nonterminal n f) (s : IRhsSymbol T (g.nt ⊕ ℕ × ℕ) g.flag) : s ∈ List.map g.fsStripPushRhsSym l → ∃ (n : g.nt ⊕ ℕ × ℕ) (f : Option g.flag), s = IRhsSymbol.nonterminal n f

theorem IndexedGrammar.hti_all_nt_of_not_terminal_cond {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hti : (∃ (a : T), r.rhs = [IRhsSymbol.terminal a]) ∨ ∀ s ∈ r.rhs, ∃ (n : g.nt) (f : Option g.flag), s = IRhsSymbol.nonterminal n f) (h : ¬((r.rhs.any fun (s : IRhsSymbol T g.nt g.flag) => match s with | IRhsSymbol.terminal a => true | x => false) && r.rhs.length == 1) = true) (s : IRhsSymbol T g.nt g.flag) : s ∈ r.rhs → ∃ (n : g.nt) (f : Option g.flag), s = IRhsSymbol.nonterminal n f

theorem IndexedGrammar.fsSingleRule_terminalsIsolated {T : Type} (g : IndexedGrammar T) (i : ℕ) (r : IRule T g.nt g.flag) (hti : (∃ (a : T), r.rhs = [IRhsSymbol.terminal a]) ∨ ∀ s ∈ r.rhs, ∃ (n : g.nt) (f : Option g.flag), s = IRhsSymbol.nonterminal n f) (r' : IRule T (g.nt ⊕ ℕ × ℕ) g.flag) (hr' : r' ∈ g.fsSingleRule i r) : (∃ (a : T), r'.rhs = [IRhsSymbol.terminal a]) ∨ ∀ s ∈ r'.rhs, ∃ (n : g.nt ⊕ ℕ × ℕ) (f : Option g.flag), s = IRhsSymbol.nonterminal n f

theorem IndexedGrammar.flagSeparate_terminalsIsolated {T : Type} (g : IndexedGrammar T) (hti : g.TerminalsIsolated) : g.flagSeparate.TerminalsIsolated

theorem IndexedGrammar.fsSingleRule_flagsSeparated {T : Type} (g : IndexedGrammar T) (i : ℕ) (r : IRule T g.nt g.flag) (hti : (∃ (a : T), r.rhs = [IRhsSymbol.terminal a]) ∨ ∀ s ∈ r.rhs, ∃ (n : g.nt) (f : Option g.flag), s = IRhsSymbol.nonterminal n f) (r' : IRule T (g.nt ⊕ ℕ × ℕ) g.flag) (hr' : r' ∈ g.fsSingleRule i r) : IRule.FlagsSeparated r'

theorem IndexedGrammar.flagSeparate_flagsSeparated {T : Type} (g : IndexedGrammar T) (hti : g.TerminalsIsolated) : g.flagSeparate.FlagsSeparated

theorem IndexedGrammar.fsSingleRule_startNotOnRhs {T : Type} (g : IndexedGrammar T) (i : ℕ) (r : IRule T g.nt g.flag) (hfresh : ∀ s ∈ r.rhs, match s with | IRhsSymbol.nonterminal n a => n ≠ g.initial | IRhsSymbol.terminal a => True) (r' : IRule T (g.nt ⊕ ℕ × ℕ) g.flag) (hr' : r' ∈ g.fsSingleRule i r) (s : IRhsSymbol T (g.nt ⊕ ℕ × ℕ) g.flag) : s ∈ r'.rhs → match s with | IRhsSymbol.nonterminal n a => n ≠ Sum.inl g.initial | IRhsSymbol.terminal a => True

theorem IndexedGrammar.flagSeparate_startNotOnRhs {T : Type} (g : IndexedGrammar T) (hfresh : g.StartNotOnRhs') : g.flagSeparate.StartNotOnRhs'

theorem IndexedGrammar.fsLiftISym_expandRhs {T : Type} (g : IndexedGrammar T) (rhs : List (IRhsSymbol T g.nt g.flag)) (σ : List g.flag) : List.map g.fsLiftISym (g.expandRhs rhs σ) = g.flagSeparate.expandRhs (List.map g.fsLiftRhsSym rhs) σ

theorem IndexedGrammar.fsLiftISym_map_terminal {T : Type} (g : IndexedGrammar T) (w : List T) : List.map g.fsLiftISym (List.map ISym.terminal w) = List.map ISym.terminal w

theorem IndexedGrammar.fsSingleRule_mem_flagSeparate {T : Type} (g : IndexedGrammar T) {r : IRule T g.nt g.flag} {i : ℕ} (hr : (r, i) ∈ g.rules.zipIdx) (r' : IRule T (g.nt ⊕ ℕ × ℕ) g.flag) (hr' : r' ∈ g.fsSingleRule i r) : r' ∈ g.flagSeparate.rules

theorem IndexedGrammar.resolveIntermediates {T : Type} (g : IndexedGrammar T) (rhs : List (IRhsSymbol T g.nt g.flag)) (i offset : ℕ) (hri : ∀ (s : IRhsSymbol T g.nt g.flag) (j : ℕ), (s, j) ∈ rhs.zipIdx → g.hasPush s = true → { lhs := Sum.inr (i, j + offset), consume := none, rhs := [match s with | IRhsSymbol.nonterminal n (some f) => IRhsSymbol.nonterminal (Sum.inl n) (some f) | x => IRhsSymbol.nonterminal (Sum.inl g.initial) none] } ∈ g.flagSeparate.rules) (σ : List g.flag) : g.flagSeparate.Derives (g.flagSeparate.expandRhs (List.map (fun (x : IRhsSymbol T g.nt g.flag × ℕ) => match x with | (s, j) => g.fsReplaceRhsSym i (j + offset) s) rhs.zipIdx) σ) (g.flagSeparate.expandRhs (List.map g.fsLiftRhsSym rhs) σ)

theorem IndexedGrammar.fsStripPushRhsSym_eq_fsLiftRhsSym_of_noPush {T : Type} (g : IndexedGrammar T) (rhs : List (IRhsSymbol T g.nt g.flag)) (hnp : rhs.any g.hasPush = false) : List.map g.fsStripPushRhsSym rhs = List.map g.fsLiftRhsSym rhs

When hasPush is false, fsStripPushRhsSym agrees with fsLiftRhsSym on the list.

theorem IndexedGrammar.fsLift_rule_simulation {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (i : ℕ) (hri : (r, i) ∈ g.rules.zipIdx) (σ : List g.flag) : g.flagSeparate.Derives [ISym.indexed (Sum.inl r.lhs) (match r.consume with | none => σ | some f => f :: σ)] (g.flagSeparate.expandRhs (List.map g.fsLiftRhsSym r.rhs) σ)

Simulation of a single rule: from the nonterminal with appropriate stack, flagSeparate can derive the lifted expansion.

theorem IndexedGrammar.fsLift_transforms {T : Type} (g : IndexedGrammar T) {u v : List g.ISym} (h : g.Transforms u v) : g.flagSeparate.Derives (List.map g.fsLiftISym u) (List.map g.fsLiftISym v)

theorem IndexedGrammar.fsLift_derives {T : Type} (g : IndexedGrammar T) {u v : List g.ISym} (h : g.Derives u v) : g.flagSeparate.Derives (List.map g.fsLiftISym u) (List.map g.fsLiftISym v)

theorem IndexedGrammar.flagSeparate_language_forward {T : Type} (g : IndexedGrammar T) {w : List T} (h : g.Generates w) : g.flagSeparate.Generates w

noncomputable def IndexedGrammar.fsUnsepIntermediate {T : Type} (g : IndexedGrammar T) (idx : ℕ × ℕ) (σ : List g.flag) : List g.ISym

Equations

• One or more equations did not get rendered due to their size.

noncomputable def IndexedGrammar.fsUnsepSym {T : Type} (g : IndexedGrammar T) : g.flagSeparate.ISym → List g.ISym

Equations

• g.fsUnsepSym (IndexedGrammar.ISym.terminal t) = [IndexedGrammar.ISym.terminal t]
• g.fsUnsepSym (IndexedGrammar.ISym.indexed (Sum.inl n) σ) = [IndexedGrammar.ISym.indexed n σ]
• g.fsUnsepSym (IndexedGrammar.ISym.indexed (Sum.inr val) σ) = g.fsUnsepIntermediate val σ

noncomputable def IndexedGrammar.fsUnsepSF {T : Type} (g : IndexedGrammar T) (w : List g.flagSeparate.ISym) : List g.ISym

Equations

• g.fsUnsepSF w = List.flatMap g.fsUnsepSym w

theorem IndexedGrammar.flagSeparate_language_backward {T : Type} (g : IndexedGrammar T) {w : List T} (h : g.flagSeparate.Generates w) : g.Generates w

theorem IndexedGrammar.flagSeparate_generates_iff {T : Type} (g : IndexedGrammar T) (w : List T) : g.flagSeparate.Generates w ↔ g.Generates w

theorem IndexedGrammar.exists_flagsSeparated_all {T : Type} (g : IndexedGrammar T) (hti : g.TerminalsIsolated) : ∃ (g' : IndexedGrammar T), g'.TerminalsIsolated ∧ g'.FlagsSeparated ∧ (g.StartNotOnRhs' → g'.StartNotOnRhs') ∧ ∀ (w : List T), g'.Generates w ↔ g.Generates w

theorem IndexedGrammar.exists_flagsSeparated {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') (hti : g.TerminalsIsolated) : ∃ (g' : IndexedGrammar T), g'.NoEpsilon' ∧ g'.TerminalsIsolated ∧ g'.FlagsSeparated ∧ (g.StartNotOnRhs' → g'.StartNotOnRhs') ∧ ∀ (w : List T), g'.Generates w ↔ g.Generates w

theorem IndexedGrammar.exists_flagsSeparated' {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') (hti : g.TerminalsIsolated) : ∃ (g' : IndexedGrammar T), g'.NoEpsilon' ∧ g'.TerminalsIsolated ∧ g'.FlagsSeparated ∧ (g.StartNotOnRhs' → g'.StartNotOnRhs') ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g.Generates w)