Library fl.int.Union
Require Import List.
Require Import fl.cfg.Base fl.cfg.Definitions fl.cfg.Binarize fl.cfg.Chomsky.
Require Import fl.int.Base2 fl.int.DFA fl.int.ChomskyInduction.
Module Union.
Import ListNotations Definitions Derivation Base Base2 ChomskyInduction.
Require Import fl.cfg.Base fl.cfg.Definitions fl.cfg.Binarize fl.cfg.Chomsky.
Require Import fl.int.Base2 fl.int.DFA fl.int.ChomskyInduction.
Module Union.
Import ListNotations Definitions Derivation Base Base2 ChomskyInduction.
Definitions
In this section we define a function that creates a union-grammar out of a list of grammars.
Section Definitions.
Variables Tt Vt: Type.
(* TODO: move? *)
Definition grammar_to_language {Tt Vl : Type} (g : @var Vl × (@grammar Tt Vl)) : language :=
let '(st, gr) := g in fun word ⇒ der gr st (to_phrase word).
Inductive labeled_Vt : Type :=
| start : labeled_Vt
| lV : nat → @var Vt → labeled_Vt.
Definition label_var (label: nat) (v: @var Vt): @var labeled_Vt :=
V (lV label v).
Definition label_symbol (label: nat) (s: @symbol Tt Vt): @symbol Tt labeled_Vt :=
match s with
| Ts t ⇒ Ts t
| Vs v ⇒ Vs (V (lV label v))
end.
Definition label_phrase (label: nat) (p: @phrase Tt Vt): @phrase Tt labeled_Vt :=
map (label_symbol label) p.
Definition label_rule (label: nat) (r : @rule Tt Vt): @rule Tt labeled_Vt :=
let '(R v p) := r in R (V (lV label v)) (label_phrase label p).
Definition label_grammar (label: nat) (g: @grammar Tt Vt): @grammar Tt labeled_Vt:=
map (label_rule label) g.
Definition label_grammar_and_add_start_rule (label: nat) (g : @var Vt × (@grammar Tt Vt)):
@grammar Tt labeled_Vt :=
let '(st, gr) := g in (R (V start) [Vs (V (lV label st))]) :: label_grammar label gr.
Fixpoint label_list_of_grammars (grammars : seq (@var Vt × (@grammar Tt Vt))):
@grammar Tt labeled_Vt :=
match grammars with
| [] ⇒ []
| ((_,gr)::t) ⇒ label_grammar (length t) gr ++ (label_list_of_grammars t)
end.
Fixpoint grammar_union (grammars : seq (@var Vt × (@grammar Tt Vt))): @grammar Tt labeled_Vt :=
match grammars with
| [] ⇒ []
| (g::t) ⇒ label_grammar_and_add_start_rule (length t) g ++ (grammar_union t)
end.
End Definitions.
Section Lemmas.
Variables Tt Vt: Type.
(* TODO: move? *)
Definition grammar_to_language {Tt Vl : Type} (g : @var Vl × (@grammar Tt Vl)) : language :=
let '(st, gr) := g in fun word ⇒ der gr st (to_phrase word).
Inductive labeled_Vt : Type :=
| start : labeled_Vt
| lV : nat → @var Vt → labeled_Vt.
Definition label_var (label: nat) (v: @var Vt): @var labeled_Vt :=
V (lV label v).
Definition label_symbol (label: nat) (s: @symbol Tt Vt): @symbol Tt labeled_Vt :=
match s with
| Ts t ⇒ Ts t
| Vs v ⇒ Vs (V (lV label v))
end.
Definition label_phrase (label: nat) (p: @phrase Tt Vt): @phrase Tt labeled_Vt :=
map (label_symbol label) p.
Definition label_rule (label: nat) (r : @rule Tt Vt): @rule Tt labeled_Vt :=
let '(R v p) := r in R (V (lV label v)) (label_phrase label p).
Definition label_grammar (label: nat) (g: @grammar Tt Vt): @grammar Tt labeled_Vt:=
map (label_rule label) g.
Definition label_grammar_and_add_start_rule (label: nat) (g : @var Vt × (@grammar Tt Vt)):
@grammar Tt labeled_Vt :=
let '(st, gr) := g in (R (V start) [Vs (V (lV label st))]) :: label_grammar label gr.
Fixpoint label_list_of_grammars (grammars : seq (@var Vt × (@grammar Tt Vt))):
@grammar Tt labeled_Vt :=
match grammars with
| [] ⇒ []
| ((_,gr)::t) ⇒ label_grammar (length t) gr ++ (label_list_of_grammars t)
end.
Fixpoint grammar_union (grammars : seq (@var Vt × (@grammar Tt Vt))): @grammar Tt labeled_Vt :=
match grammars with
| [] ⇒ []
| (g::t) ⇒ label_grammar_and_add_start_rule (length t) g ++ (grammar_union t)
end.
End Definitions.
Section Lemmas.
Section Util.
Context {Tt Vt: Type}.
Lemma word_remains_terminal:
∀ word,
@terminal Tt Vt (to_phrase word).
Lemma inner:
∀ (A: Type) (a: A) u v w,
In a v ∨ In a (u ++ w) ↔
In a (u ++ v ++ w).
Lemma app_label_phrase:
∀ (lphrase1 lphrase2: @phrase Tt (labeled_Vt Vt)) (label: nat) (phrase: @phrase Tt Vt),
lphrase1 ++ lphrase2 = label_phrase label phrase →
∃ phrase1 phrase2,
phrase1 ++ phrase2 = phrase ∧
lphrase1 = label_phrase label phrase1 ∧
lphrase2 = label_phrase label phrase2.
Lemma label_phrase_for_word:
∀ (label: nat) (word: word),
@to_phrase Tt (labeled_Vt Vt) word = label_phrase label (to_phrase word).
Lemma label_symbol_is_injective:
∀ (label: nat) (s1 s2: @symbol Tt Vt),
label_symbol label s1 = label_symbol label s2 →
s1 = s2.
Lemma label_app:
∀ (label: nat) (p1 p2: @phrase Tt Vt),
label_phrase label (p1 ++ p2) = label_phrase label p1 ++ label_phrase label p2.
End Util.
Context {Tt Vt: Type}.
Lemma word_remains_terminal:
∀ word,
@terminal Tt Vt (to_phrase word).
Lemma inner:
∀ (A: Type) (a: A) u v w,
In a v ∨ In a (u ++ w) ↔
In a (u ++ v ++ w).
Lemma app_label_phrase:
∀ (lphrase1 lphrase2: @phrase Tt (labeled_Vt Vt)) (label: nat) (phrase: @phrase Tt Vt),
lphrase1 ++ lphrase2 = label_phrase label phrase →
∃ phrase1 phrase2,
phrase1 ++ phrase2 = phrase ∧
lphrase1 = label_phrase label phrase1 ∧
lphrase2 = label_phrase label phrase2.
Lemma label_phrase_for_word:
∀ (label: nat) (word: word),
@to_phrase Tt (labeled_Vt Vt) word = label_phrase label (to_phrase word).
Lemma label_symbol_is_injective:
∀ (label: nat) (s1 s2: @symbol Tt Vt),
label_symbol label s1 = label_symbol label s2 →
s1 = s2.
Lemma label_app:
∀ (label: nat) (p1 p2: @phrase Tt Vt),
label_phrase label (p1 ++ p2) = label_phrase label p1 ++ label_phrase label p2.
End Util.
Forward
In this section we prove that derivability in one grammar from the list implies derivability in the union-grammar.(* Let Tt Vt be types of terminals and nonterminals correspondingly. *)
Variable Tt Vt: Type.
(* For simplicity, let's define some local names. *)
Let der := @der Tt.
Let var := @var Vt.
Let grammar := @grammar Tt Vt.
Section Forward.
Lemma grammar_extention:
∀ {V: Type} grammar1 grammar2 var (phrase: @phrase Tt V),
der grammar2 var phrase →
der (grammar1 ++ grammar2) var phrase.
Lemma der_in_grammar_implies_der_in_union_grammar_1:
∀ st grammar var grammars phrase,
der grammar var phrase →
der (grammar_union ((st, grammar) :: grammars))
(label_var (length grammars) var)
(@label_phrase Tt Vt (length grammars) phrase).
Lemma der_in_grammar_implies_der_in_union_grammar_2:
∀ var grammar grammars word,
grammar_to_language (var, grammar) word →
grammar_to_language (V (start Vt), grammar_union (Tt:=Tt) ((var, grammar) :: grammars)) word.
(* Now we can use two lemmas above to get the proof.
(1) We use induction by (list of) grammars.
(2) "Base" case is trivial.
(3) "Step" case splits into two subcases:
a) Case where we can use der_in_grammar_implies_der_in_union_grammar_2 lemma
b) Case where we can just use inductive hypothesis. *)
Lemma same_union_forward:
∀ (grammars: seq (var × grammar)) word,
language_list_union (map grammar_to_language grammars) word →
grammar_to_language (V (start Vt), grammar_union grammars) word.
End Forward.
Backward
In this section we prove that derivability in the union-grammar implies derivability in one of the grammar from the list.
Section Backward.
(* In this section we prove several obvious properties of the updated grammar. *)
Section GeneralFacts.
Variable grammars: seq (var × grammar).
Lemma der_in_union_simpl_grammar_implies_der_in_union_grammar:
∀ var phrase,
der (label_list_of_grammars grammars) var phrase →
der (grammar_union grammars) var phrase.
Lemma updated_derivation_doesnot_contain_start_symbol:
∀ label var phrase,
der (grammar_union grammars) (V (lV label var)) phrase →
¬ In (Vs (V (start Vt))) phrase.
Lemma derivability_without_start_rules:
∀ var phrase,
var ≠ V (start Vt) →
der (grammar_union grammars) var phrase →
der (label_list_of_grammars grammars) var phrase.
Lemma simpl_updated_derivation_doesnot_contain_start_symbol:
∀ label var phrase,
der (label_list_of_grammars grammars) (V (lV label var)) phrase →
¬ In (Vs (V (start Vt))) phrase.
End GeneralFacts.
(* In this section we prove that the derivability of a word in some _labeled_ grammar
implies that the word belongs to the union-language *)
Section DerivabilityInUnionGrammar.
Lemma start_nonterminal_is_not_derivable_in_labeled_grammar:
∀ grammar label1 label2 var word1 word2,
¬ der (label_grammar label1 grammar)
(V (lV label2 var)) (word1 ++ [Vs (V (start Vt))] ++ word2).
Lemma labels_in_derivation_are_consistent:
∀ (grammar: grammar) label var phrase,
der (label_grammar label grammar) (V (lV label var)) phrase →
∀ label' var', In (Vs (V (lV label' var'))) phrase → label = label'.
Lemma update_grammar_simpl_is_injective:
∀ (grammar: grammar) var label phrase,
der (label_grammar label grammar) (V (lV label var)) (label_phrase label phrase) →
der grammar var phrase.
Lemma derivability_in_grammar_implies_derivability_in_union_grammar:
∀ (grammars: seq (var × grammar)) grammar start label word,
In (start, grammar) grammars →
der (label_grammar label grammar) (V (lV label start)) (to_phrase word) →
language_list_union (map grammar_to_language grammars) word.
End DerivabilityInUnionGrammar.
(* Suppose we have a phrase that we derived in a union-grammar.
In this section we prove that there are only two options (1) either it is the
starting nonterminal, or (2) we can choose a grammar from the union-list in
which it is possible to derive this phrase. *)
Section ChooseGrammarWithCorrectLabel.
Lemma choose_labeled_grammar:
∀ (grammars: seq (var × grammar)) phrase,
der (grammar_union grammars) (V (start Vt)) phrase →
phrase = [Vs (V (start Vt))] ∨
∃ grammar var grammars1 grammars2,
(grammars1 ++ (var, grammar) :: grammars2) = grammars ∧
der (grammar_union grammars) (V (lV (length grammars2) var)) phrase.
End ChooseGrammarWithCorrectLabel.
(* In this section we prove that we can remove all grammars with "wrong" label. In other words,
if we have a labeled nonterminal, it is not possible to derive something with different
label. So, we can simply remove grammars with different labels. *)
Section CutGrammars.
Lemma labels_in_derivation_are_consistent_2:
∀ (grammars: seq (var × grammar)) label var phrase,
der (label_list_of_grammars grammars) (V (lV label var)) phrase →
∀ label' var', In (Vs (V (lV label' var'))) phrase → label = label'.
Lemma cut_head:
∀ grammar grammars label (var: var) phrase,
length grammars ≠ label →
der (label_list_of_grammars (grammar::grammars)) (V (lV label var)) phrase →
der (label_list_of_grammars grammars) (V (lV label var)) phrase.
Lemma label_is_bounded_by_grammar_union_length:
∀ (grammars: seq (var × grammar)) label var phrase,
length grammars ≤ label →
¬ In (R (V (lV label var)) phrase) (label_list_of_grammars grammars).
Lemma cut_tail:
∀ (grammar: grammar) grammars label var v p,
length grammars = label →
der (label_list_of_grammars ((var, grammar)::grammars)) (V (lV label v)) p →
der (label_grammar label grammar) (V (lV label v)) p.
Lemma cut_grammar:
∀ (grammar: grammar) grammars1 grammars2 label var phrase,
length grammars2 = label →
der (label_list_of_grammars (grammars1 ++ [(var,grammar)] ++ grammars2)) (V (lV label var)) phrase →
der (label_grammar label grammar) (V (lV label var)) phrase.
End CutGrammars.
(* Now we can use all the lemmas above to get the proof.
(1) We use choose_labeled_grammar lemma to make step into the correct grammar of the union-grammar
(2) Next, lemma derivability_without_start_rules which states that we can make drop all the
rules that lead from the starting nonterminal to the other grammars
(3) Next, we can use the cut_grammar lemma to get rid of grammars with the wrong label
(4) And finally, we apply derivability_in_grammar_implies_derivability_in_union_grammar lemma
to "unlabel" the resulting grammar. *)
Lemma same_union_backward:
∀ (grammars: seq (var × grammar)) word,
grammar_to_language (V (start Vt), grammar_union grammars) word →
language_list_union (map grammar_to_language grammars) word.
End Backward.
(* In this section we prove several obvious properties of the updated grammar. *)
Section GeneralFacts.
Variable grammars: seq (var × grammar).
Lemma der_in_union_simpl_grammar_implies_der_in_union_grammar:
∀ var phrase,
der (label_list_of_grammars grammars) var phrase →
der (grammar_union grammars) var phrase.
Lemma updated_derivation_doesnot_contain_start_symbol:
∀ label var phrase,
der (grammar_union grammars) (V (lV label var)) phrase →
¬ In (Vs (V (start Vt))) phrase.
Lemma derivability_without_start_rules:
∀ var phrase,
var ≠ V (start Vt) →
der (grammar_union grammars) var phrase →
der (label_list_of_grammars grammars) var phrase.
Lemma simpl_updated_derivation_doesnot_contain_start_symbol:
∀ label var phrase,
der (label_list_of_grammars grammars) (V (lV label var)) phrase →
¬ In (Vs (V (start Vt))) phrase.
End GeneralFacts.
(* In this section we prove that the derivability of a word in some _labeled_ grammar
implies that the word belongs to the union-language *)
Section DerivabilityInUnionGrammar.
Lemma start_nonterminal_is_not_derivable_in_labeled_grammar:
∀ grammar label1 label2 var word1 word2,
¬ der (label_grammar label1 grammar)
(V (lV label2 var)) (word1 ++ [Vs (V (start Vt))] ++ word2).
Lemma labels_in_derivation_are_consistent:
∀ (grammar: grammar) label var phrase,
der (label_grammar label grammar) (V (lV label var)) phrase →
∀ label' var', In (Vs (V (lV label' var'))) phrase → label = label'.
Lemma update_grammar_simpl_is_injective:
∀ (grammar: grammar) var label phrase,
der (label_grammar label grammar) (V (lV label var)) (label_phrase label phrase) →
der grammar var phrase.
Lemma derivability_in_grammar_implies_derivability_in_union_grammar:
∀ (grammars: seq (var × grammar)) grammar start label word,
In (start, grammar) grammars →
der (label_grammar label grammar) (V (lV label start)) (to_phrase word) →
language_list_union (map grammar_to_language grammars) word.
End DerivabilityInUnionGrammar.
(* Suppose we have a phrase that we derived in a union-grammar.
In this section we prove that there are only two options (1) either it is the
starting nonterminal, or (2) we can choose a grammar from the union-list in
which it is possible to derive this phrase. *)
Section ChooseGrammarWithCorrectLabel.
Lemma choose_labeled_grammar:
∀ (grammars: seq (var × grammar)) phrase,
der (grammar_union grammars) (V (start Vt)) phrase →
phrase = [Vs (V (start Vt))] ∨
∃ grammar var grammars1 grammars2,
(grammars1 ++ (var, grammar) :: grammars2) = grammars ∧
der (grammar_union grammars) (V (lV (length grammars2) var)) phrase.
End ChooseGrammarWithCorrectLabel.
(* In this section we prove that we can remove all grammars with "wrong" label. In other words,
if we have a labeled nonterminal, it is not possible to derive something with different
label. So, we can simply remove grammars with different labels. *)
Section CutGrammars.
Lemma labels_in_derivation_are_consistent_2:
∀ (grammars: seq (var × grammar)) label var phrase,
der (label_list_of_grammars grammars) (V (lV label var)) phrase →
∀ label' var', In (Vs (V (lV label' var'))) phrase → label = label'.
Lemma cut_head:
∀ grammar grammars label (var: var) phrase,
length grammars ≠ label →
der (label_list_of_grammars (grammar::grammars)) (V (lV label var)) phrase →
der (label_list_of_grammars grammars) (V (lV label var)) phrase.
Lemma label_is_bounded_by_grammar_union_length:
∀ (grammars: seq (var × grammar)) label var phrase,
length grammars ≤ label →
¬ In (R (V (lV label var)) phrase) (label_list_of_grammars grammars).
Lemma cut_tail:
∀ (grammar: grammar) grammars label var v p,
length grammars = label →
der (label_list_of_grammars ((var, grammar)::grammars)) (V (lV label v)) p →
der (label_grammar label grammar) (V (lV label v)) p.
Lemma cut_grammar:
∀ (grammar: grammar) grammars1 grammars2 label var phrase,
length grammars2 = label →
der (label_list_of_grammars (grammars1 ++ [(var,grammar)] ++ grammars2)) (V (lV label var)) phrase →
der (label_grammar label grammar) (V (lV label var)) phrase.
End CutGrammars.
(* Now we can use all the lemmas above to get the proof.
(1) We use choose_labeled_grammar lemma to make step into the correct grammar of the union-grammar
(2) Next, lemma derivability_without_start_rules which states that we can make drop all the
rules that lead from the starting nonterminal to the other grammars
(3) Next, we can use the cut_grammar lemma to get rid of grammars with the wrong label
(4) And finally, we apply derivability_in_grammar_implies_derivability_in_union_grammar lemma
to "unlabel" the resulting grammar. *)
Lemma same_union_backward:
∀ (grammars: seq (var × grammar)) word,
grammar_to_language (V (start Vt), grammar_union grammars) word →
language_list_union (map grammar_to_language grammars) word.
End Backward.
Section MainTheorem1.
Variable grammars: seq (var × grammar).
Let l1 := language_list_union (map grammar_to_language grammars).
Let l2 := grammar_to_language (V (start Vt), grammar_union grammars).
Theorem correct_union_1:
language_eq l1 l2.
End MainTheorem1.
Section MainTheorem2.
Variable grammars: seq (var × grammar).
Theorem correct_union_2:
∀ word,
Derivation.language (grammar_union grammars) (V (start Vt)) (to_phrase word) ↔
∃ s_l, Derivation.language (snd s_l) (fst s_l) (to_phrase word) ∧ In s_l grammars.
End MainTheorem2.
End Lemmas.
End Union.
Variable grammars: seq (var × grammar).
Let l1 := language_list_union (map grammar_to_language grammars).
Let l2 := grammar_to_language (V (start Vt), grammar_union grammars).
Theorem correct_union_1:
language_eq l1 l2.
End MainTheorem1.
Section MainTheorem2.
Variable grammars: seq (var × grammar).
Theorem correct_union_2:
∀ word,
Derivation.language (grammar_union grammars) (V (start Vt)) (to_phrase word) ↔
∃ s_l, Derivation.language (snd s_l) (fst s_l) (to_phrase word) ∧ In s_l grammars.
End MainTheorem2.
End Lemmas.
End Union.