Unrestricted Lifting

This file lifts unrestricted grammars across embeddings of nonterminal types.

Main declarations

• lift_deri_
• sink_deri_

def lift_symbol_ {T N₀ N : Type} (lift_N : N₀ → N) : symbol T N₀ → symbol T N

Equations

• lift_symbol_ lift_N (symbol.terminal t) = symbol.terminal t
• lift_symbol_ lift_N (symbol.nonterminal n) = symbol.nonterminal (lift_N n)

def sink_symbol_ {T N₀ N : Type} (sink_N : N → Option N₀) : symbol T N → Option (symbol T N₀)

Equations

• sink_symbol_ sink_N (symbol.terminal t) = some (symbol.terminal t)
• sink_symbol_ sink_N (symbol.nonterminal n) = Option.map symbol.nonterminal (sink_N n)

def lift_string_ {T N₀ N : Type} (lift_N : N₀ → N) : List (symbol T N₀) → List (symbol T N)

Equations

• lift_string_ lift_N = List.map (lift_symbol_ lift_N)

def sink_string_ {T N₀ N : Type} (sink_N : N → Option N₀) : List (symbol T N) → List (symbol T N₀)

Equations

• sink_string_ sink_N = List.filterMap (sink_symbol_ sink_N)

def lift_rule_ {T N₀ N : Type} (lift_N : N₀ → N) : grule T N₀ → grule T N

Equations

• lift_rule_ lift_N r = { input_L := lift_string_ lift_N r.input_L, input_N := lift_N r.input_N, input_R := lift_string_ lift_N r.input_R, output_string := lift_string_ lift_N r.output_string }

theorem sink_string_map_terminal_ {T N₀ N : Type} (sink_N : N → Option N₀) (w : List T) : sink_string_ sink_N (List.map symbol.terminal w) = List.map symbol.terminal w

sink_string_ preserves terminal-only lists.

theorem lift_string_map_terminal_ {T N₀ N : Type} (lift_N : N₀ → N) (w : List T) : lift_string_ lift_N (List.map symbol.terminal w) = List.map symbol.terminal w

lift_string_ preserves terminal-only lists.

structure lifted_grammar_ (T : Type) : Type 1

• g₀ : grammar T
• g : grammar T
• lift_nt : self.g₀.nt → self.g.nt
• sink_nt : self.g.nt → Option self.g₀.nt
• lift_inj : Function.Injective self.lift_nt
• sink_inj (x y : self.g.nt) : self.sink_nt x = self.sink_nt y → x = y ∨ self.sink_nt x = none
• lift_nt_sink (n₀ : self.g₀.nt) : self.sink_nt (self.lift_nt n₀) = some n₀
• corresponding_rules (r : grule T self.g₀.nt) : r ∈ self.g₀.rules → lift_rule_ self.lift_nt r ∈ self.g.rules
• preimage_of_rules (r : grule T self.g.nt) : (r ∈ self.g.rules ∧ ∃ (n₀ : self.g₀.nt), self.lift_nt n₀ = r.input_N) → ∃ r₀ ∈ self.g₀.rules, lift_rule_ self.lift_nt r₀ = r

theorem lift_deri_ {T : Type} (lg : lifted_grammar_ T) {w₁ w₂ : List (symbol T lg.g₀.nt)} (hyp : grammar_derives lg.g₀ w₁ w₂) : grammar_derives lg.g (lift_string_ lg.lift_nt w₁) (lift_string_ lg.lift_nt w₂)

def good_letter_ {T : Type} {lg : lifted_grammar_ T} : symbol T lg.g.nt → Prop

Equations

• good_letter_ (symbol.terminal _t) = True
• good_letter_ (symbol.nonterminal n) = ∃ (n₀ : lg.g₀.nt), lg.sink_nt n = some n₀

def good_string_ {T : Type} {lg : lifted_grammar_ T} (s : List (symbol T lg.g.nt)) : Prop

Equations

• good_string_ s = ∀ a ∈ s, good_letter_ a

theorem sink_deri_ {T : Type} (lg : lifted_grammar_ T) {w₁ w₂ : List (symbol T lg.g.nt)} (hyp : grammar_derives lg.g w₁ w₂) (ok_input : good_string_ w₁) : grammar_derives lg.g₀ (sink_string_ lg.sink_nt w₁) (sink_string_ lg.sink_nt w₂)