RE Closure Under Concatenation

This file constructs an unrestricted grammar for the concatenation of two recursively enumerable languages.

Proof idea: take the two unrestricted grammars, tag their nonterminals so they cannot interfere, and add a fresh start rule that emits the lifted left start symbol followed by the lifted right start symbol. The forward and backward lemmas show that derivations in the combined grammar are exactly a left derivation followed by a right derivation, hence the generated language is L₁ * L₂.

Main declarations

• big_grammar
• in_big_of_in_concatenated
• in_concatenated_of_in_big
• RE_of_RE_c_RE

def nnn (T N₁ N₂ : Type) : Type

Equations

• nnn T N₁ N₂ = (Option (N₁ ⊕ N₂) ⊕ T ⊕ T)

@[reducible, inline]

abbrev nst (T N₁ N₂ : Type) : Type

Equations

• nst T N₁ N₂ = symbol T (nnn T N₁ N₂)

def wrap_symbol₁ {T N₁ : Type} (N₂ : Type) : symbol T N₁ → nst T N₁ N₂

Equations

• wrap_symbol₁ N₂ (symbol.terminal t) = symbol.nonterminal (Sum.inr (Sum.inl t))
• wrap_symbol₁ N₂ (symbol.nonterminal n) = symbol.nonterminal (Sum.inl (some (Sum.inl n)))

def wrap_symbol₂ {T N₂ : Type} (N₁ : Type) : symbol T N₂ → nst T N₁ N₂

Equations

• wrap_symbol₂ N₁ (symbol.terminal t) = symbol.nonterminal (Sum.inr (Sum.inr t))
• wrap_symbol₂ N₁ (symbol.nonterminal n) = symbol.nonterminal (Sum.inl (some (Sum.inr n)))

def wrap_grule₁ {T N₁ : Type} (N₂ : Type) (r : grule T N₁) : grule T (nnn T N₁ N₂)

Equations

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

def wrap_grule₂ {T N₂ : Type} (N₁ : Type) (r : grule T N₂) : grule T (nnn T N₁ N₂)

Equations

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

def rules_for_terminals₁ {T : Type} (N₂ : Type) (g : grammar T) : List (grule T (nnn T g.nt N₂))

Equations

• rules_for_terminals₁ N₂ g = List.map (fun (t : T) => { input_L := [], input_N := Sum.inr (Sum.inl t), input_R := [], output_string := [symbol.terminal t] }) (all_used_terminals g)

def rules_for_terminals₂ {T : Type} (N₁ : Type) (g : grammar T) : List (grule T (nnn T N₁ g.nt))

Equations

• rules_for_terminals₂ N₁ g = List.map (fun (t : T) => { input_L := [], input_N := Sum.inr (Sum.inr t), input_R := [], output_string := [symbol.terminal t] }) (all_used_terminals g)

def big_grammar {T : Type} (g₁ g₂ : grammar T) : grammar T

Equations

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

theorem grammar_generates_only_legit_terminals {T : Type} {g : grammar T} {w : List (symbol T g.nt)} (ass : grammar_derives g [symbol.nonterminal g.initial] w) {s : symbol T g.nt} (symbol_derived : s ∈ w) : (∃ r ∈ g.rules, s ∈ r.output_string) ∨ s = symbol.nonterminal g.initial

theorem first_transformation {T : Type} {g₁ g₂ : grammar T} : grammar_transforms (big_grammar g₁ g₂) [symbol.nonterminal (big_grammar g₁ g₂).initial] [symbol.nonterminal (Sum.inl (some (Sum.inl g₁.initial))), symbol.nonterminal (Sum.inl (some (Sum.inr g₂.initial)))]

theorem substitute_terminals {T : Type} {g₁ g₂ : grammar T} {side : T → T ⊕ T} {w : List T} (rule_for_each_terminal : ∀ t ∈ w, { input_L := [], input_N := Sum.inr (side t), input_R := [], output_string := [symbol.terminal t] } ∈ rules_for_terminals₁ g₂.nt g₁ ++ rules_for_terminals₂ g₁.nt g₂) : grammar_derives (big_grammar g₁ g₂) (List.map (symbol.nonterminal ∘ Sum.inr ∘ side) w) (List.map symbol.terminal w)

theorem in_big_of_in_concatenated {T : Type} {g₁ g₂ : grammar T} {w : List T} (ass : w ∈ grammar_language g₁ * grammar_language g₂) : w ∈ grammar_language (big_grammar g₁ g₂)

def corresponding_symbols {T N₁ N₂ : Type} : nst T N₁ N₂ → nst T N₁ N₂ → Prop

Equations

• corresponding_symbols (symbol.terminal t) (symbol.terminal t') = (t = t')
• corresponding_symbols (symbol.nonterminal (Sum.inr (Sum.inl a))) (symbol.nonterminal (Sum.inr (Sum.inl a'))) = (a = a')
• corresponding_symbols (symbol.nonterminal (Sum.inr (Sum.inr a))) (symbol.nonterminal (Sum.inr (Sum.inr a'))) = (a = a')
• corresponding_symbols (symbol.nonterminal (Sum.inr (Sum.inl a))) (symbol.terminal t) = (t = a)
• corresponding_symbols (symbol.nonterminal (Sum.inr (Sum.inr a))) (symbol.terminal t) = (t = a)
• corresponding_symbols (symbol.nonterminal (Sum.inl (some (Sum.inl n)))) (symbol.nonterminal (Sum.inl (some (Sum.inl n')))) = (n = n')
• corresponding_symbols (symbol.nonterminal (Sum.inl (some (Sum.inr n)))) (symbol.nonterminal (Sum.inl (some (Sum.inr n')))) = (n = n')
• corresponding_symbols (symbol.nonterminal (Sum.inl none)) (symbol.nonterminal (Sum.inl none)) = True
• corresponding_symbols x✝¹ x✝ = False

theorem corresponding_symbols_self {T N₁ N₂ : Type} (s : nst T N₁ N₂) : corresponding_symbols s s

theorem corresponding_symbols_never₁ {T N₁ N₂ : Type} {s₁ : symbol T N₁} {s₂ : symbol T N₂} : ¬corresponding_symbols (wrap_symbol₁ N₂ s₁) (wrap_symbol₂ N₁ s₂)

theorem corresponding_symbols_never₂ {T N₁ N₂ : Type} {s₁ : symbol T N₁} {s₂ : symbol T N₂} : ¬corresponding_symbols (wrap_symbol₂ N₁ s₂) (wrap_symbol₁ N₂ s₁)

def corresponding_strings {T N₁ N₂ : Type} : List (nst T N₁ N₂) → List (nst T N₁ N₂) → Prop

Equations

• corresponding_strings = List.Forall₂ corresponding_symbols

theorem corresponding_strings_self {T N₁ N₂ : Type} {x : List (nst T N₁ N₂)} : corresponding_strings x x

theorem corresponding_strings_singleton {T N₁ N₂ : Type} {s₁ s₂ : nst T N₁ N₂} (ass : corresponding_symbols s₁ s₂) : corresponding_strings [s₁] [s₂]

theorem corresponding_strings_append {T N₁ N₂ : Type} {x₁ x₂ y₁ y₂ : List (nst T N₁ N₂)} (ass₁ : corresponding_strings x₁ y₁) (ass₂ : corresponding_strings x₂ y₂) : corresponding_strings (x₁ ++ x₂) (y₁ ++ y₂)

theorem corresponding_strings_length {T N₁ N₂ : Type} {x y : List (nst T N₁ N₂)} (ass : corresponding_strings x y) : x.length = y.length

theorem corresponding_strings_of_reverse {T N₁ N₂ : Type} {x y : List (nst T N₁ N₂)} (ass : corresponding_strings x.reverse y.reverse) : corresponding_strings x y

theorem corresponding_strings_take {T N₁ N₂ : Type} {x y : List (nst T N₁ N₂)} (n : ℕ) (ass : corresponding_strings x y) : corresponding_strings (List.take n x) (List.take n y)

theorem corresponding_strings_drop {T N₁ N₂ : Type} {x y : List (nst T N₁ N₂)} (n : ℕ) (ass : corresponding_strings x y) : corresponding_strings (List.drop n x) (List.drop n y)

theorem corresponding_strings_split {T N₁ N₂ : Type} {x y : List (nst T N₁ N₂)} (n : ℕ) (ass : corresponding_strings x y) : corresponding_strings (List.take n x) (List.take n y) ∧ corresponding_strings (List.drop n x) (List.drop n y)

def unwrap_symbol₁ {T N₁ N₂ : Type} : nst T N₁ N₂ → Option (symbol T N₁)

Equations

• unwrap_symbol₁ (symbol.terminal t) = some (symbol.terminal t)
• unwrap_symbol₁ (symbol.nonterminal (Sum.inr (Sum.inl a))) = some (symbol.terminal a)
• unwrap_symbol₁ (symbol.nonterminal (Sum.inr (Sum.inr _a))) = none
• unwrap_symbol₁ (symbol.nonterminal (Sum.inl (some (Sum.inl n)))) = some (symbol.nonterminal n)
• unwrap_symbol₁ (symbol.nonterminal (Sum.inl (some (Sum.inr _n)))) = none
• unwrap_symbol₁ (symbol.nonterminal (Sum.inl none)) = none

def unwrap_symbol₂ {T N₁ N₂ : Type} : nst T N₁ N₂ → Option (symbol T N₂)

Equations

• unwrap_symbol₂ (symbol.terminal t) = some (symbol.terminal t)
• unwrap_symbol₂ (symbol.nonterminal (Sum.inr (Sum.inl a))) = none
• unwrap_symbol₂ (symbol.nonterminal (Sum.inr (Sum.inr _a))) = some (symbol.terminal _a)
• unwrap_symbol₂ (symbol.nonterminal (Sum.inl (some (Sum.inl n)))) = none
• unwrap_symbol₂ (symbol.nonterminal (Sum.inl (some (Sum.inr _n)))) = some (symbol.nonterminal _n)
• unwrap_symbol₂ (symbol.nonterminal (Sum.inl none)) = none

theorem unwrap_wrap₁_symbol {T N₁ N₂ : Type} : unwrap_symbol₁ ∘ wrap_symbol₁ N₂ = some

theorem unwrap_wrap₂_symbol {T N₁ N₂ : Type} : unwrap_symbol₂ ∘ wrap_symbol₂ N₁ = some

theorem unwrap_wrap₁_string {T N₁ N₂ : Type} {w : List (symbol T N₁)} : List.filterMap unwrap_symbol₁ (List.map (wrap_symbol₁ N₂) w) = w

theorem unwrap_wrap₂_string {T N₁ N₂ : Type} {w : List (symbol T N₂)} : List.filterMap unwrap_symbol₂ (List.map (wrap_symbol₂ N₁) w) = w

theorem unwrap_eq_some_of_corresponding_symbols₁ {T N₁ N₂ : Type} {s₁ : symbol T N₁} {s : nst T N₁ N₂} (ass : corresponding_symbols (wrap_symbol₁ N₂ s₁) s) : unwrap_symbol₁ s = some s₁

theorem unwrap_eq_some_of_corresponding_symbols₂ {T N₁ N₂ : Type} {s₂ : symbol T N₂} {s : nst T N₁ N₂} (ass : corresponding_symbols (wrap_symbol₂ N₁ s₂) s) : unwrap_symbol₂ s = some s₂

theorem map_unwrap_eq_map_some_of_corresponding_strings₁ {T N₁ N₂ : Type} {v : List (symbol T N₁)} {w : List (nst T N₁ N₂)} : corresponding_strings (List.map (wrap_symbol₁ N₂) v) w → List.map unwrap_symbol₁ w = List.map some v

theorem map_unwrap_eq_map_some_of_corresponding_strings₂ {T N₁ N₂ : Type} {v : List (symbol T N₂)} {w : List (nst T N₁ N₂)} : corresponding_strings (List.map (wrap_symbol₂ N₁) v) w → List.map unwrap_symbol₂ w = List.map some v

theorem filter_map_unwrap_of_corresponding_strings₁ {T N₁ N₂ : Type} {v : List (symbol T N₁)} {w : List (nst T N₁ N₂)} (ass : corresponding_strings (List.map (wrap_symbol₁ N₂) v) w) : List.filterMap unwrap_symbol₁ w = v

theorem filter_map_unwrap_of_corresponding_strings₂ {T N₁ N₂ : Type} {v : List (symbol T N₂)} {w : List (nst T N₁ N₂)} (ass : corresponding_strings (List.map (wrap_symbol₂ N₁) v) w) : List.filterMap unwrap_symbol₂ w = v

theorem corresponding_string_after_wrap_unwrap_self₁ {T N₁ N₂ : Type} {w : List (nst T N₁ N₂)} (ass : ∃ (z : List (symbol T N₁)), corresponding_strings (List.map (wrap_symbol₁ N₂) z) w) : corresponding_strings (List.map (wrap_symbol₁ N₂) (List.filterMap unwrap_symbol₁ w)) w

theorem corresponding_string_after_wrap_unwrap_self₂ {T N₁ N₂ : Type} {w : List (nst T N₁ N₂)} (ass : ∃ (z : List (symbol T N₂)), corresponding_strings (List.map (wrap_symbol₂ N₁) z) w) : corresponding_strings (List.map (wrap_symbol₂ N₁) (List.filterMap unwrap_symbol₂ w)) w

theorem unwrap₁_of_wrap₂_eq_none {T N₁ N₂ : Type} (s : symbol T N₂) : unwrap_symbol₁ (wrap_symbol₂ N₁ s) = none

theorem unwrap₂_of_wrap₁_eq_none {T N₁ N₂ : Type} (s : symbol T N₁) : unwrap_symbol₂ (wrap_symbol₁ N₂ s) = none

theorem filterMap_unwrap₁_map_wrap₂ {T N₁ N₂ : Type} (w : List (symbol T N₂)) : List.filterMap unwrap_symbol₁ (List.map (wrap_symbol₂ N₁) w) = []

theorem filterMap_unwrap₂_map_wrap₁ {T N₁ N₂ : Type} (w : List (symbol T N₁)) : List.filterMap unwrap_symbol₂ (List.map (wrap_symbol₁ N₂) w) = []

theorem forall₂_append_split {α β : Type} {R : α → β → Prop} {l₁ l₂ : List α} {m : List β} (h : List.Forall₂ R (l₁ ++ l₂) m) : ∃ (m₁ : List β) (m₂ : List β), m = m₁ ++ m₂ ∧ List.Forall₂ R l₁ m₁ ∧ List.Forall₂ R l₂ m₂

theorem no_wrap₂_corr_sum_inl_inl {T N₁ N₂ : Type} {n₁ : N₁} {s₂ : symbol T N₂} : ¬corresponding_symbols (wrap_symbol₂ N₁ s₂) (symbol.nonterminal (Sum.inl (some (Sum.inl n₁))))

theorem no_wrap₁_corr_sum_inl_inr {T N₁ N₂ : Type} {n₂ : N₂} {s₁ : symbol T N₁} : ¬corresponding_symbols (wrap_symbol₁ N₂ s₁) (symbol.nonterminal (Sum.inl (some (Sum.inr n₂))))

theorem x_from_take_filterMap {T N₁ N₂ : Type} {x : List (symbol T N₁)} {y : List (symbol T N₂)} {a : List (nst T N₁ N₂)} (h : corresponding_strings (List.map (wrap_symbol₁ N₂) x ++ List.map (wrap_symbol₂ N₁) y) a) : List.filterMap unwrap_symbol₁ (List.take x.length a) = x

theorem y_from_drop_filterMap {T N₁ N₂ : Type} {x : List (symbol T N₁)} {y : List (symbol T N₂)} {a : List (nst T N₁ N₂)} (h : corresponding_strings (List.map (wrap_symbol₁ N₂) x ++ List.map (wrap_symbol₂ N₁) y) a) : List.filterMap unwrap_symbol₂ (List.drop x.length a) = y

theorem rule_in_first_half {T N₁ N₂ : Type} {x : List (symbol T N₁)} {y : List (symbol T N₂)} {a u v : List (nst T N₁ N₂)} {r₁ : grule T N₁} (ih_concat : corresponding_strings (List.map (wrap_symbol₁ N₂) x ++ List.map (wrap_symbol₂ N₁) y) a) (bef : a = u ++ List.map (wrap_symbol₁ N₂) r₁.input_L ++ [symbol.nonterminal (Sum.inl (some (Sum.inl r₁.input_N)))] ++ List.map (wrap_symbol₁ N₂) r₁.input_R ++ v) : u.length + r₁.input_L.length + 1 + r₁.input_R.length ≤ x.length

theorem rule_in_second_half {T N₁ N₂ : Type} {x : List (symbol T N₁)} {y : List (symbol T N₂)} {a u v : List (nst T N₁ N₂)} {r₂ : grule T N₂} (ih_concat : corresponding_strings (List.map (wrap_symbol₁ N₂) x ++ List.map (wrap_symbol₂ N₁) y) a) (bef : a = u ++ List.map (wrap_symbol₂ N₁) r₂.input_L ++ [symbol.nonterminal (Sum.inl (some (Sum.inr r₂.input_N)))] ++ List.map (wrap_symbol₂ N₁) r₂.input_R ++ v) : x.length ≤ u.length

theorem take_of_append_five {α : Type} {u L : List α} {n : α} {R v : List α} {m : ℕ} (h_le : u.length + L.length + 1 + R.length ≤ m) : List.take m (u ++ L ++ [n] ++ R ++ v) = u ++ L ++ [n] ++ R ++ List.take (m - (u.length + L.length + 1 + R.length)) v

theorem drop_of_append_five {α : Type} {u L : List α} {n : α} {R v : List α} {m : ℕ} (h_le : u.length + L.length + 1 + R.length ≤ m) (_h_le2 : m ≤ u.length + L.length + 1 + R.length + v.length) : List.drop m (u ++ L ++ [n] ++ R ++ v) = List.drop (m - (u.length + L.length + 1 + R.length)) v

theorem induction_step_for_lifted_rule_from_g₁ {T : Type} {g₁ g₂ : grammar T} {a b u v : List (nst T g₁.nt g₂.nt)} {x : List (symbol T g₁.nt)} {y : List (symbol T g₂.nt)} {r : grule T (nnn T g₁.nt g₂.nt)} (rin : r ∈ List.map (wrap_grule₁ g₂.nt) g₁.rules) (bef : a = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v) (aft : b = u ++ r.output_string ++ v) (ih_x : grammar_derives g₁ [symbol.nonterminal g₁.initial] x) (ih_y : grammar_derives g₂ [symbol.nonterminal g₂.initial] y) (ih_concat : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) a) : ∃ (x' : List (symbol T g₁.nt)), grammar_derives g₁ [symbol.nonterminal g₁.initial] x' ∧ grammar_derives g₂ [symbol.nonterminal g₂.initial] y ∧ corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x' ++ List.map (wrap_symbol₂ g₁.nt) y) b

theorem induction_step_for_lifted_rule_from_g₂ {T : Type} {g₁ g₂ : grammar T} {a b u v : List (nst T g₁.nt g₂.nt)} {x : List (symbol T g₁.nt)} {y : List (symbol T g₂.nt)} {r : grule T (nnn T g₁.nt g₂.nt)} (rin : r ∈ List.map (wrap_grule₂ g₁.nt) g₂.rules) (bef : a = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v) (aft : b = u ++ r.output_string ++ v) (ih_x : grammar_derives g₁ [symbol.nonterminal g₁.initial] x) (ih_y : grammar_derives g₂ [symbol.nonterminal g₂.initial] y) (ih_concat : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) a) : ∃ (y' : List (symbol T g₂.nt)), grammar_derives g₁ [symbol.nonterminal g₁.initial] x ∧ grammar_derives g₂ [symbol.nonterminal g₂.initial] y' ∧ corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y') b

theorem no_none_in_wrapped₁ {T N₁ N₂ : Type} (s : symbol T N₁) : wrap_symbol₁ N₂ s ≠ symbol.nonterminal (Sum.inl none)

theorem no_none_in_wrapped₂ {T N₁ N₂ : Type} (s : symbol T N₂) : wrap_symbol₂ N₁ s ≠ symbol.nonterminal (Sum.inl none)

theorem induction_step_for_terminal_rule₁ {T : Type} {g₁ g₂ : grammar T} {a b u v : List (nst T g₁.nt g₂.nt)} {x : List (symbol T g₁.nt)} {y : List (symbol T g₂.nt)} {t : T} (ht : t ∈ all_used_terminals g₁) (bef : a = u ++ [symbol.nonterminal (Sum.inr (Sum.inl t))] ++ v) (aft : b = u ++ [symbol.terminal t] ++ v) (ih_concat : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) a) : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) b

theorem induction_step_for_terminal_rule₂ {T : Type} {g₁ g₂ : grammar T} {a b u v : List (nst T g₁.nt g₂.nt)} {x : List (symbol T g₁.nt)} {y : List (symbol T g₂.nt)} {t : T} (_ht : t ∈ all_used_terminals g₂) (bef : a = u ++ [symbol.nonterminal (Sum.inr (Sum.inr t))] ++ v) (aft : b = u ++ [symbol.terminal t] ++ v) (ih_concat : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) a) : corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) b

theorem big_induction {T : Type} {g₁ g₂ : grammar T} {w : List (nst T g₁.nt g₂.nt)} (ass : grammar_derives (big_grammar g₁ g₂) [symbol.nonterminal (Sum.inl (some (Sum.inl g₁.initial))), symbol.nonterminal (Sum.inl (some (Sum.inr g₂.initial)))] w) : ∃ (x : List (symbol T g₁.nt)) (y : List (symbol T g₂.nt)), grammar_derives g₁ [symbol.nonterminal g₁.initial] x ∧ grammar_derives g₂ [symbol.nonterminal g₂.initial] y ∧ corresponding_strings (List.map (wrap_symbol₁ g₂.nt) x ++ List.map (wrap_symbol₂ g₁.nt) y) w

theorem in_concatenated_of_in_big {T : Type} {g₁ g₂ : grammar T} {w : List T} (ass : w ∈ grammar_language (big_grammar g₁ g₂)) : w ∈ grammar_language g₁ * grammar_language g₂

theorem RE_of_RE_c_RE {T : Type} (L₁ L₂ : Language T) : is_RE L₁ ∧ is_RE L₂ → is_RE (L₁ * L₂)

theorem RE_closedUnderConcatenation {T : Type} : ClosedUnderConcatenation is_RE

The class of recursively enumerable languages is closed under concatenation.