Finite nonterminal and flag support for indexed grammars

Indexed grammars store their rules in a finite list. Even if the ambient nonterminal and flag types are infinite, every derivation from the initial symbol only uses nonterminals and flags mentioned by the initial symbol or by the rules. This file restricts an indexed grammar to those finite supports while preserving its language.

Syntactic supports

def IndexedGrammar.rhsSymbolNTs {T N F : Type} : IRhsSymbol T N F → List N

Nonterminals mentioned by a right-hand-side symbol.

Equations

• IndexedGrammar.rhsSymbolNTs (IRhsSymbol.terminal a) = []
• IndexedGrammar.rhsSymbolNTs (IRhsSymbol.nonterminal n a) = [n]

def IndexedGrammar.ruleNTs {T N F : Type} (r : IRule T N F) : List N

Nonterminals mentioned by a rule, including its left-hand side.

Equations

• IndexedGrammar.ruleNTs r = r.lhs :: List.flatMap IndexedGrammar.rhsSymbolNTs r.rhs

def IndexedGrammar.rhsSymbolFlags {T N F : Type} : IRhsSymbol T N F → List F

Flags mentioned by a right-hand-side symbol as pushed flags.

Equations

• IndexedGrammar.rhsSymbolFlags (IRhsSymbol.terminal a) = []
• IndexedGrammar.rhsSymbolFlags (IRhsSymbol.nonterminal a none) = []
• IndexedGrammar.rhsSymbolFlags (IRhsSymbol.nonterminal a (some f)) = [f]

def IndexedGrammar.ruleFlags {T N F : Type} (r : IRule T N F) : List F

Flags mentioned by a rule, including consumed and pushed flags.

Equations

• IndexedGrammar.ruleFlags r = r.consume.toList ++ List.flatMap IndexedGrammar.rhsSymbolFlags r.rhs

def IndexedGrammar.usedNTs {T : Type} (g : IndexedGrammar T) : Finset g.nt

The finite set of nonterminals used by an indexed grammar.

Equations

• g.usedNTs = (g.initial :: List.flatMap IndexedGrammar.ruleNTs g.rules).toFinset

def IndexedGrammar.usedFlags {T : Type} (g : IndexedGrammar T) : Finset g.flag

The finite set of flags used by an indexed grammar.

Equations

• g.usedFlags = (List.flatMap IndexedGrammar.ruleFlags g.rules).toFinset

theorem IndexedGrammar.initial_mem_usedNTs {T : Type} (g : IndexedGrammar T) : g.initial ∈ g.usedNTs

theorem IndexedGrammar.rhs_nonterminal_mem_ruleNTs {T N F : Type} {r : IRule T N F} {n : N} {push : Option F} (h : IRhsSymbol.nonterminal n push ∈ r.rhs) : n ∈ ruleNTs r

theorem IndexedGrammar.lhs_mem_ruleNTs {T N F : Type} (r : IRule T N F) : r.lhs ∈ ruleNTs r

theorem IndexedGrammar.ruleNT_mem_usedNTs {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) {n : g.nt} (hn : n ∈ ruleNTs r) : n ∈ g.usedNTs

theorem IndexedGrammar.rule_lhs_mem_usedNTs {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) : r.lhs ∈ g.usedNTs

theorem IndexedGrammar.rule_rhs_nt_mem_usedNTs {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) {n : g.nt} {push : Option g.flag} (h : IRhsSymbol.nonterminal n push ∈ r.rhs) : n ∈ g.usedNTs

theorem IndexedGrammar.consume_mem_ruleFlags {T N F : Type} {r : IRule T N F} {f : F} (h : r.consume = some f) : f ∈ ruleFlags r

theorem IndexedGrammar.rhs_push_mem_ruleFlags {T N F : Type} {r : IRule T N F} {n : N} {f : F} (h : IRhsSymbol.nonterminal n (some f) ∈ r.rhs) : f ∈ ruleFlags r

theorem IndexedGrammar.ruleFlag_mem_usedFlags {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) {f : g.flag} (hf : f ∈ ruleFlags r) : f ∈ g.usedFlags

theorem IndexedGrammar.rule_consume_mem_usedFlags {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) {f : g.flag} (h : r.consume = some f) : f ∈ g.usedFlags

theorem IndexedGrammar.rule_consume_mem_usedFlags_of_mem {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) {f : g.flag} (h : f ∈ r.consume) : f ∈ g.usedFlags

theorem IndexedGrammar.rule_rhs_push_mem_usedFlags {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) {n : g.nt} {f : g.flag} (h : IRhsSymbol.nonterminal n (some f) ∈ r.rhs) : f ∈ g.usedFlags

Restricted grammar

@[reducible, inline]

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

The subtype of nonterminals used by g.

Equations

• g.UsedNT = { n : g.nt // n ∈ g.usedNTs }

@[reducible, inline]

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

The subtype of flags used by g.

Equations

• g.UsedFlag = { f : g.flag // f ∈ g.usedFlags }

instance IndexedGrammar.usedNT_fintype {T : Type} (g : IndexedGrammar T) : Fintype g.UsedNT

Equations

• g.usedNT_fintype = Fintype.subtype g.usedNTs ⋯

instance IndexedGrammar.usedFlag_fintype {T : Type} (g : IndexedGrammar T) : Fintype g.UsedFlag

Equations

• g.usedFlag_fintype = Fintype.subtype g.usedFlags ⋯

def IndexedGrammar.restrictConsume {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) : Option g.UsedFlag

Equations

• g.restrictConsume r hr = Option.map (fun (f : { x : g.flag // r.consume = some x }) => ⟨↑f, ⋯⟩) r.consume.attach

def IndexedGrammar.restrictPush {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) {n : g.nt} (push : Option g.flag) (hs : IRhsSymbol.nonterminal n push ∈ r.rhs) : Option g.UsedFlag

Equations

• g.restrictPush r hr none hs_2 = none
• g.restrictPush r hr (some f) hs_2 = some ⟨f, ⋯⟩

def IndexedGrammar.restrictRhsSymbol {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) (s : IRhsSymbol T g.nt g.flag) (hs : s ∈ r.rhs) : IRhsSymbol T g.UsedNT g.UsedFlag

Equations

• g.restrictRhsSymbol r hr (IRhsSymbol.terminal t) hs_2 = IRhsSymbol.terminal t
• g.restrictRhsSymbol r hr (IRhsSymbol.nonterminal n push) hs_2 = IRhsSymbol.nonterminal ⟨n, ⋯⟩ (g.restrictPush r hr push hs_2)

def IndexedGrammar.restrictRhs {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) : List (IRhsSymbol T g.UsedNT g.UsedFlag)

Equations

• g.restrictRhs r hr = List.map (fun (s : { x : IRhsSymbol T g.nt g.flag // x ∈ r.rhs }) => g.restrictRhsSymbol r hr ↑s ⋯) r.rhs.attach

def IndexedGrammar.restrictRule {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) : IRule T g.UsedNT g.UsedFlag

Equations

• g.restrictRule r hr = { lhs := ⟨r.lhs, ⋯⟩, consume := g.restrictConsume r hr, rhs := g.restrictRhs r hr }

def IndexedGrammar.toFiniteSupport {T : Type} (g : IndexedGrammar T) : IndexedGrammar T

The indexed grammar restricted to the finite nonterminal and flag supports used by g.

Equations

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

instance IndexedGrammar.toFiniteSupport_nt_fintype {T : Type} (g : IndexedGrammar T) : Fintype g.toFiniteSupport.nt

Equations

• g.toFiniteSupport_nt_fintype = g.usedNT_fintype

instance IndexedGrammar.toFiniteSupport_flag_fintype {T : Type} (g : IndexedGrammar T) : Fintype g.toFiniteSupport.flag

Equations

• g.toFiniteSupport_flag_fintype = g.usedFlag_fintype

Embedding restricted syntax back into g

def IndexedGrammar.embedFlag {T : Type} (g : IndexedGrammar T) : g.UsedFlag → g.flag

Equations

• g.embedFlag = Subtype.val

def IndexedGrammar.embedRhsSymbol {T : Type} (g : IndexedGrammar T) : IRhsSymbol T g.UsedNT g.UsedFlag → IRhsSymbol T g.nt g.flag

Equations

• g.embedRhsSymbol (IRhsSymbol.terminal t) = IRhsSymbol.terminal t
• g.embedRhsSymbol (IRhsSymbol.nonterminal n push) = IRhsSymbol.nonterminal (↑n) (Option.map Subtype.val push)

def IndexedGrammar.embedISym {T : Type} (g : IndexedGrammar T) : g.toFiniteSupport.ISym → g.ISym

Equations

• g.embedISym (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• g.embedISym (IndexedGrammar.ISym.indexed n σ) = IndexedGrammar.ISym.indexed (↑n) (List.map Subtype.val σ)

theorem IndexedGrammar.restrictConsume_val {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) : Option.map Subtype.val (g.restrictConsume r hr) = r.consume

theorem IndexedGrammar.restrictPush_val {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) {n : g.nt} (push : Option g.flag) (hs : IRhsSymbol.nonterminal n push ∈ r.rhs) : Option.map Subtype.val (g.restrictPush r hr push hs) = push

theorem IndexedGrammar.embed_restrictRhsSymbol {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) (s : IRhsSymbol T g.nt g.flag) (hs : s ∈ r.rhs) : g.embedRhsSymbol (g.restrictRhsSymbol r hr s hs) = s

theorem IndexedGrammar.embed_restrictRhs {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) : List.map g.embedRhsSymbol (g.restrictRhs r hr) = r.rhs

theorem IndexedGrammar.embedRhsSymbol_injective {T : Type} (g : IndexedGrammar T) : Function.Injective g.embedRhsSymbol

theorem IndexedGrammar.expandRhs_embed {T : Type} (g : IndexedGrammar T) (rhs : List (IRhsSymbol T g.UsedNT g.UsedFlag)) (σ : List g.UsedFlag) : List.map g.embedISym (g.toFiniteSupport.expandRhs rhs σ) = g.expandRhs (List.map g.embedRhsSymbol rhs) (List.map Subtype.val σ)

theorem IndexedGrammar.expandRhs_restrict {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) (σ : List g.UsedFlag) : List.map g.embedISym (g.toFiniteSupport.expandRhs (g.restrictRule r hr).rhs σ) = g.expandRhs r.rhs (List.map Subtype.val σ)

theorem IndexedGrammar.restrictRule_mem_toFiniteSupport {T : Type} (g : IndexedGrammar T) {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) : g.restrictRule r hr ∈ g.toFiniteSupport.rules

theorem IndexedGrammar.mem_toFiniteSupport_rules {T : Type} (g : IndexedGrammar T) {r' : IRule T g.toFiniteSupport.nt g.toFiniteSupport.flag} (hr' : r' ∈ g.toFiniteSupport.rules) : ∃ (r : IRule T g.nt g.flag) (hr : r ∈ g.rules), r' = g.restrictRule r hr

theorem IndexedGrammar.restrictRule_flagsSeparated {T : Type} (g : IndexedGrammar T) {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hsep : IRule.FlagsSeparated r) : IRule.FlagsSeparated (g.restrictRule r hr)

theorem IndexedGrammar.toFiniteSupport_flagsSeparated {T : Type} (g : IndexedGrammar T) (hfs : g.FlagsSeparated) : g.toFiniteSupport.FlagsSeparated

Finite-support sentential forms

def IndexedGrammar.stackSupported {T : Type} (g : IndexedGrammar T) (σ : List g.flag) : Prop

Equations

• g.stackSupported σ = ∀ f ∈ σ, f ∈ g.usedFlags

def IndexedGrammar.symSupported {T : Type} (g : IndexedGrammar T) : g.ISym → Prop

Equations

• g.symSupported (IndexedGrammar.ISym.terminal a) = True
• g.symSupported (IndexedGrammar.ISym.indexed n σ) = (n ∈ g.usedNTs ∧ g.stackSupported σ)

def IndexedGrammar.sententialSupported {T : Type} (g : IndexedGrammar T) (w : List g.ISym) : Prop

Equations

• g.sententialSupported w = ∀ s ∈ w, g.symSupported s

theorem IndexedGrammar.stackSupported_tail {T : Type} {g : IndexedGrammar T} {f : g.flag} {σ : List g.flag} (h : g.stackSupported (f :: σ)) : g.stackSupported σ

theorem IndexedGrammar.stackSupported_cons {T : Type} {g : IndexedGrammar T} {f : g.flag} {σ : List g.flag} (hf : f ∈ g.usedFlags) (hσ : g.stackSupported σ) : g.stackSupported (f :: σ)

theorem IndexedGrammar.sententialSupported_initial {T : Type} (g : IndexedGrammar T) : g.sententialSupported [ISym.indexed g.initial []]

theorem IndexedGrammar.expandRhs_supported {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) {σ : List g.flag} (hσ : g.stackSupported σ) : g.sententialSupported (g.expandRhs r.rhs σ)

theorem IndexedGrammar.transforms_supported {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (h : g.Transforms w₁ w₂) (hsupp : g.sententialSupported w₁) : g.sententialSupported w₂

theorem IndexedGrammar.derives_supported {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (h : g.Derives w₁ w₂) (hsupp : g.sententialSupported w₁) : g.sententialSupported w₂

Restricting supported sentential forms

def IndexedGrammar.restrictStack {T : Type} (g : IndexedGrammar T) (σ : List g.flag) (hσ : g.stackSupported σ) : List g.UsedFlag

Equations

• g.restrictStack σ hσ = List.map (fun (f : { x : g.flag // x ∈ σ }) => ⟨↑f, ⋯⟩) σ.attach

def IndexedGrammar.restrictISym {T : Type} (g : IndexedGrammar T) (s : g.ISym) (hs : g.symSupported s) : g.toFiniteSupport.ISym

Equations

• g.restrictISym (IndexedGrammar.ISym.terminal t) hs_2 = IndexedGrammar.ISym.terminal t
• g.restrictISym (IndexedGrammar.ISym.indexed n σ) hs_2 = IndexedGrammar.ISym.indexed ⟨n, ⋯⟩ (g.restrictStack σ ⋯)

def IndexedGrammar.restrictSF {T : Type} (g : IndexedGrammar T) (w : List g.ISym) (hw : g.sententialSupported w) : List g.toFiniteSupport.ISym

Equations

• g.restrictSF w hw = List.map (fun (s : { x : g.ISym // x ∈ w }) => g.restrictISym ↑s ⋯) w.attach

theorem IndexedGrammar.map_val_restrictStack {T : Type} (g : IndexedGrammar T) (σ : List g.flag) (hσ : g.stackSupported σ) : List.map Subtype.val (g.restrictStack σ hσ) = σ

theorem IndexedGrammar.unattach_restrictStack {T : Type} (g : IndexedGrammar T) (σ : List g.flag) (hσ : g.stackSupported σ) : (g.restrictStack σ hσ).unattach = σ

theorem IndexedGrammar.embed_restrictISym {T : Type} (g : IndexedGrammar T) (s : g.ISym) (hs : g.symSupported s) : g.embedISym (g.restrictISym s hs) = s

theorem IndexedGrammar.embed_restrictSF {T : Type} (g : IndexedGrammar T) (w : List g.ISym) (hw : g.sententialSupported w) : List.map g.embedISym (g.restrictSF w hw) = w

theorem IndexedGrammar.embedISym_injective {T : Type} (g : IndexedGrammar T) : Function.Injective g.embedISym

theorem IndexedGrammar.restrictSF_terminal {T : Type} (g : IndexedGrammar T) (w : List T) (hw : g.sententialSupported (List.map ISym.terminal w)) : g.restrictSF (List.map ISym.terminal w) hw = List.map ISym.terminal w

theorem IndexedGrammar.restrictSF_initial {T : Type} (g : IndexedGrammar T) : g.restrictSF [ISym.indexed g.initial []] ⋯ = [ISym.indexed ⟨g.initial, ⋯⟩ []]

Derivation correspondence

theorem IndexedGrammar.transforms_embed {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.toFiniteSupport.ISym} (h : g.toFiniteSupport.Transforms w₁ w₂) : g.Transforms (List.map g.embedISym w₁) (List.map g.embedISym w₂)

theorem IndexedGrammar.derives_embed {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.toFiniteSupport.ISym} (h : g.toFiniteSupport.Derives w₁ w₂) : g.Derives (List.map g.embedISym w₁) (List.map g.embedISym w₂)

theorem IndexedGrammar.transforms_restrict {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (h : g.Transforms w₁ w₂) (hsupp : g.sententialSupported w₁) : g.toFiniteSupport.Transforms (g.restrictSF w₁ hsupp) (g.restrictSF w₂ ⋯)

theorem IndexedGrammar.derives_restrict {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (h : g.Derives w₁ w₂) (hsupp : g.sententialSupported w₁) : g.toFiniteSupport.Derives (g.restrictSF w₁ hsupp) (g.restrictSF w₂ ⋯)

Language equality

theorem IndexedGrammar.toFiniteSupport_language {T : Type} (g : IndexedGrammar T) : g.toFiniteSupport.Language = g.Language

theorem IndexedGrammar.exists_finiteSupport {T : Type} (g : IndexedGrammar T) : ∃ (g' : IndexedGrammar T) (x : Fintype g'.nt) (x : Fintype g'.flag), g'.Language = g.Language

Every indexed grammar has an equivalent grammar whose nonterminal and flag types are finite.

Preservation of normal form

theorem IndexedGrammar.restrictRule_isNF {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hNF : IRule.IsNF r g.initial) : IRule.IsNF (g.restrictRule r hr) ⟨g.initial, ⋯⟩

theorem IndexedGrammar.toFiniteSupport_isNormalForm {T : Type} {g : IndexedGrammar T} [DecidableEq g.nt] (hNF : g.IsNormalForm) : g.toFiniteSupport.IsNormalForm