Context-Free Lifting

This file lifts context-free grammars across embeddings of nonterminal types and supplies reusable sum-type constructions.

Main declarations

• lift_deri
• sink_deri
• rule_of_rule₁
• rule_of_rule₂

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) : N₀ × List (symbol T N₀) → N × List (symbol T N)

Equations

• lift_rule lift_N r = (lift_N r.1, lift_string lift_N r.2)

structure lifted_grammar (T : Type) : Type 1

• g₀ : CF_grammar T
• g : CF_grammar T
• lift_nt : self.g₀.nt → self.g.nt
• lift_inj : Function.Injective self.lift_nt
• corresponding_rules (r : self.g₀.nt × List (symbol T self.g₀.nt)) : r ∈ self.g₀.rules → lift_rule self.lift_nt r ∈ self.g.rules
• sink_nt : self.g.nt → Option self.g₀.nt
• sink_inj (x y : self.g.nt) : self.sink_nt x = self.sink_nt y → x = y ∨ self.sink_nt x = none
• preimage_of_rules (r : self.g.nt × List (symbol T self.g.nt)) : (r ∈ self.g.rules ∧ ∃ (n₀ : self.g₀.nt), self.lift_nt n₀ = r.1) → ∃ r₀ ∈ self.g₀.rules, lift_rule self.lift_nt r₀ = r
• lift_nt_sink (n₀ : self.g₀.nt) : self.sink_nt (self.lift_nt n₀) = some n₀

theorem lift_deri {T : Type} {lg : lifted_grammar T} {w₁ w₂ : List (symbol T lg.g₀.nt)} (hyp : CF_derives lg.g₀ w₁ w₂) : CF_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 : CF_derives lg.g w₁ w₂) (ok_input : good_string w₁) : CF_derives lg.g₀ (sink_string lg.sink_nt w₁) (sink_string lg.sink_nt w₂) ∧ good_string w₂

theorem lift_string_map_terminal {T : Type} (lg : lifted_grammar T) (w : List T) : lift_string lg.lift_nt (List.map symbol.terminal w) = List.map symbol.terminal w

lift_string preserves terminal-only lists.

theorem sink_string_map_terminal {T : Type} (lg : lifted_grammar T) (w : List T) : sink_string lg.sink_nt (List.map symbol.terminal w) = List.map symbol.terminal w

sink_string preserves terminal-only lists.

theorem lift_string_terminal_inv {T N₀ N : Type} (f : N₀ → N) (u : List (symbol T N₀)) (ts : List T) (h : lift_string f u = List.map symbol.terminal ts) : u = List.map symbol.terminal ts

If lift_string f u is all terminals, then u was already all terminals. Applies to any lift_string (or List.map of a lift_symbol).

def fiveStepTac : Lean.ParserDescr

Equations

• fiveStepTac = Lean.ParserDescr.node `fiveStepTac 1024 (Lean.ParserDescr.nonReservedSymbol "five_steps" false)

def tacticFive_steps : Lean.ParserDescr

Equations

• tacticFive_steps = Lean.ParserDescr.node `tacticFive_steps 1024 (Lean.ParserDescr.nonReservedSymbol "five_steps" false)

def sTN_of_sTN₁ {T : Type} {g₁ g₂ : CF_grammar T} : symbol T g₁.nt → symbol T (Option (g₁.nt ⊕ g₂.nt))

similar to lift_symbol (Option.some ∘ sum.inl)

Equations

• sTN_of_sTN₁ (symbol.terminal st) = symbol.terminal st
• sTN_of_sTN₁ (symbol.nonterminal snt) = symbol.nonterminal (some (Sum.inl snt))

def sTN_of_sTN₂ {T : Type} {g₁ g₂ : CF_grammar T} : symbol T g₂.nt → symbol T (Option (g₁.nt ⊕ g₂.nt))

similar to lift_symbol (Option.some ∘ sum.inr)

Equations

• sTN_of_sTN₂ (symbol.terminal st) = symbol.terminal st
• sTN_of_sTN₂ (symbol.nonterminal snt) = symbol.nonterminal (some (Sum.inr snt))

def lsTN_of_lsTN₁ {T : Type} {g₁ g₂ : CF_grammar T} : List (symbol T g₁.nt) → List (symbol T (Option (g₁.nt ⊕ g₂.nt)))

similar to lift_string (Option.some ∘ sum.inl)

Equations

• lsTN_of_lsTN₁ = List.map sTN_of_sTN₁

def lsTN_of_lsTN₂ {T : Type} {g₁ g₂ : CF_grammar T} : List (symbol T g₂.nt) → List (symbol T (Option (g₁.nt ⊕ g₂.nt)))

similar to lift_string (Option.some ∘ sum.inr)

Equations

• lsTN_of_lsTN₂ = List.map sTN_of_sTN₂

def rule_of_rule₁ {T : Type} {g₁ g₂ : CF_grammar T} (r : g₁.nt × List (symbol T g₁.nt)) : Option (g₁.nt ⊕ g₂.nt) × List (symbol T (Option (g₁.nt ⊕ g₂.nt)))

similar to lift_rule (Option.some ∘ sum.inl)

Equations

• rule_of_rule₁ r = (some (Sum.inl r.1), lsTN_of_lsTN₁ r.2)

def rule_of_rule₂ {T : Type} {g₁ g₂ : CF_grammar T} (r : g₂.nt × List (symbol T g₂.nt)) : Option (g₁.nt ⊕ g₂.nt) × List (symbol T (Option (g₁.nt ⊕ g₂.nt)))

similar to lift_rule (Option.some ∘ sum.inr)

Equations

• rule_of_rule₂ r = (some (Sum.inr r.1), lsTN_of_lsTN₂ r.2)

theorem lsTN_of_lsTN₁_eq_lift_string {T : Type} {g₁ g₂ : CF_grammar T} (u : List (symbol T g₁.nt)) : lsTN_of_lsTN₁ u = lift_string (some ∘ Sum.inl) u

lsTN_of_lsTN₁ agrees with lift_string (some ∘ Sum.inl) pointwise.

theorem lsTN_of_lsTN₂_eq_lift_string {T : Type} {g₁ g₂ : CF_grammar T} (u : List (symbol T g₂.nt)) : lsTN_of_lsTN₂ u = lift_string (some ∘ Sum.inr) u

lsTN_of_lsTN₂ agrees with lift_string (some ∘ Sum.inr) pointwise.

theorem lsTN_of_lsTN₁_terminal_inv {T : Type} {g₁ g₂ : CF_grammar T} (u : List (symbol T g₁.nt)) (ts : List T) (h : lsTN_of_lsTN₁ u = List.map symbol.terminal ts) : u = List.map symbol.terminal ts

If lsTN_of_lsTN₁ u = List.map symbol.terminal ts, then u was all terminals.

theorem lsTN_of_lsTN₂_terminal_inv {T : Type} {g₁ g₂ : CF_grammar T} (v : List (symbol T g₂.nt)) (ts : List T) (h : lsTN_of_lsTN₂ v = List.map symbol.terminal ts) : v = List.map symbol.terminal ts

If lsTN_of_lsTN₂ v = List.map symbol.terminal ts, then v was all terminals.

theorem lsTN_of_lsTN₁_map_terminal {T : Type} {g₁ g₂ : CF_grammar T} (w : List T) : lsTN_of_lsTN₁ (List.map symbol.terminal w) = List.map symbol.terminal w

lsTN_of_lsTN₁ preserves terminal-only lists.

theorem lsTN_of_lsTN₂_map_terminal {T : Type} {g₁ g₂ : CF_grammar T} (w : List T) : lsTN_of_lsTN₂ (List.map symbol.terminal w) = List.map symbol.terminal w

lsTN_of_lsTN₂ preserves terminal-only lists.