Helper lemmas for RE closure under Kleene star

@[reducible, inline]

abbrev StarHelpers.nn (N : Type) : Type

Equations

• StarHelpers.nn N = (N ⊕ Fin 3)

@[reducible, inline]

abbrev StarHelpers.ns (T N : Type) : Type

Equations

• StarHelpers.ns T N = symbol T (StarHelpers.nn N)

def StarHelpers.Z {T N : Type} : ns T N

Equations

• StarHelpers.Z = symbol.nonterminal (Sum.inr 0)

def StarHelpers.H {T N : Type} : ns T N

Equations

• StarHelpers.H = symbol.nonterminal (Sum.inr 1)

def StarHelpers.R {T N : Type} : ns T N

Equations

• StarHelpers.R = symbol.nonterminal (Sum.inr 2)

def StarHelpers.wrap_sym {T N : Type} : symbol T N → ns T N

Equations

• StarHelpers.wrap_sym (symbol.terminal t) = symbol.terminal t
• StarHelpers.wrap_sym (symbol.nonterminal n) = symbol.nonterminal (Sum.inl n)

theorem StarHelpers.wrap_sym_injective {T N : Type} : Function.Injective wrap_sym

theorem StarHelpers.inr_not_in_map_wrap {T N : Type} {l : List (symbol T N)} {i : Fin 3} : symbol.nonterminal (Sum.inr i) ∉ List.map wrap_sym l

symbol.nonterminal (Sum.inr i) does not appear in List.map wrap_sym l.

theorem StarHelpers.inr_not_in_blocks {T N : Type} {x : List (List (symbol T N))} {i : Fin 3} (hi : symbol.nonterminal (Sum.inr i) ≠ H) : symbol.nonterminal (Sum.inr i) ∉ (List.map (fun (x : List (ns T N)) => x ++ [H]) (List.map (List.map wrap_sym) x)).flatten

No Sum.inr i nonterminal (other than H) appears in the flattened block structure.

theorem StarHelpers.Z_not_in_blocks {T N : Type} {x : List (List (symbol T N))} : Z ∉ (List.map (fun (x : List (ns T N)) => x ++ [H]) (List.map (List.map wrap_sym) x)).flatten

theorem StarHelpers.R_not_in_blocks {T N : Type} {x : List (List (symbol T N))} : R ∉ (List.map (fun (x : List (ns T N)) => x ++ [H]) (List.map (List.map wrap_sym) x)).flatten

theorem StarHelpers.H_not_in_wrapped_input {T N : Type} {r₀ : grule T N} : H ∉ List.map wrap_sym r₀.input_L ++ [symbol.nonterminal (Sum.inl r₀.input_N)] ++ List.map wrap_sym r₀.input_R

theorem StarHelpers.match_in_block {T N : Type} {r₀ : grule T N} {x : List (List (symbol T N))} {u v : List (ns T N)} (xne : x ≠ []) (hyp : (List.map (fun (x : List (ns T N)) => x ++ [H]) (List.map (List.map wrap_sym) x)).flatten = u ++ List.map wrap_sym r₀.input_L ++ [symbol.nonterminal (Sum.inl r₀.input_N)] ++ List.map wrap_sym r₀.input_R ++ v) : ∃ (x₁ : List (List (symbol T N))) (xₘ : List (symbol T N)) (x₂ : List (List (symbol T N))) (u₁ : List (symbol T N)) (v₁ : List (symbol T N)), x = x₁ ++ [xₘ] ++ x₂ ∧ xₘ = u₁ ++ r₀.input_L ++ [symbol.nonterminal r₀.input_N] ++ r₀.input_R ++ v₁ ∧ u = (List.map (fun (x : List (ns T N)) => x ++ [H]) (List.map (List.map wrap_sym) x₁)).flatten ++ List.map wrap_sym u₁ ∧ v = List.map wrap_sym v₁ ++ [H] ++ (List.map (fun (x : List (ns T N)) => x ++ [H]) (List.map (List.map wrap_sym) x₂)).flatten

theorem StarHelpers.update_block_in_flatten {T N : Type} {x₁ x₂ : List (List (symbol T N))} {u₁ v₁ : List (symbol T N)} {r₀ : grule T N} : (List.map (fun (x : List (ns T N)) => x ++ [H]) (List.map (List.map wrap_sym) x₁)).flatten ++ List.map wrap_sym u₁ ++ List.map wrap_sym r₀.output_string ++ List.map wrap_sym v₁ ++ [H] ++ (List.map (fun (x : List (ns T N)) => x ++ [H]) (List.map (List.map wrap_sym) x₂)).flatten = (List.map (fun (x : List (ns T N)) => x ++ [H]) (List.map (List.map wrap_sym) (x₁ ++ [u₁ ++ r₀.output_string ++ v₁] ++ x₂))).flatten

theorem StarHelpers.valid_update_block {T : Type} {g : grammar T} {x₁ x₂ : List (List (symbol T g.nt))} {u₁ v₁ : List (symbol T g.nt)} {r₀ : grule T g.nt} (hvalid : ∀ xᵢ ∈ x₁ ++ [u₁ ++ r₀.input_L ++ [symbol.nonterminal r₀.input_N] ++ r₀.input_R ++ v₁] ++ x₂, grammar_derives g [symbol.nonterminal g.initial] xᵢ) (hr₀ : r₀ ∈ g.rules) (xᵢ : List (symbol T g.nt)) : xᵢ ∈ x₁ ++ [u₁ ++ r₀.output_string ++ v₁] ++ x₂ → grammar_derives g [symbol.nonterminal g.initial] xᵢ

theorem StarHelpers.R_only_at_head {T N : Type} {x : List (List (symbol T N))} : R ∉ H :: (List.map (fun (x : List (ns T N)) => x ++ [H]) (List.map (List.map wrap_sym) x)).flatten