Library CFG.Separate
Require Export Inlining.
Definition charfree u := ∀ s, s el u → ∃ A, s = Vs A.
Definition uniform G := ∀ A u, R A u el G → ∀ a, Ts a el u → u = [Ts a].
Instance dec_charfree u : dec (charfree u).
Proof.
unfold charfree.
induction u as [| [a | A] u IHu].
- left. intros s H. destruct H.
- right. intros H.
assert (H0 : Ts a el (Ts a :: u)) by auto.
destruct (H (Ts a) H0) as [A H']. inv H'.
- destruct IHu as [IH | IH].
+ left. intros s [H | H] ; [ ∃ A |] ; auto.
+ right. intros H. apply IH.
intros s H0. apply H. auto.
Defined.
Lemma pickChar u :
¬ charfree u → { a | Ts a el u}.
Proof.
intros H.
induction u as [| [a | A] u IHu].
- exfalso. apply H. intros s H0. destruct H0.
- ∃ a. auto.
- assert (H0 : ¬ charfree u). {
intros H0. apply H.
intros s H1. destruct H1 as [H1 | H1] ; [∃ A| ] ; auto. }
destruct (IHu H0) as [a H1]. ∃ a. auto.
Qed.
Lemma pickCharRule G :
{ a | ∃ A u, R A u el G ∧ (Ts a) el u ∧ |u| ≥ 2} + uniform G.
Proof.
induction G as [| [A u] Gr IHGr].
- right. intros A u [].
- destruct IHGr as [[a IH] | IH].
+ left. ∃ a. destruct IH as [A' [u' [H0 [H1 H2]]]].
∃ A', u'. repeat split ; auto.
+ decide (charfree u) as [D | D].
× right. intros A' u' [H0 | H0] a H1 ; eauto.
inv H0. destruct (D (Ts a) H1) as [b T]. inv T.
× { apply pickChar in D. destruct D as [a D].
destruct u as [| [b | B] [| s u]].
- exfalso. destruct D as [].
- right. intros A' u' [H0 | H0] c H1 ; eauto.
inv H0. destruct H1 as [H1 | H1] ; now inv H1.
- left. ∃ a, A, (Ts b :: s :: u). repeat split ; simpl ; auto ; omega.
- exfalso. destruct D as [D | D] ; inv D.
- left. ∃ a, A, (Vs B :: s :: u). repeat split ; simpl ; auto ; omega. }
Qed.
Definition step (G : grammar) : grammar.
destruct (pickCharRule G) as [[a H] | H ].
- destruct (pickFresh G) as [B N].
exact (R B [Ts a] :: substG G (Ts a) [Vs B]).
- exact G.
Defined.
Fixpoint count_chars u :=
match u with
[] ⇒ 0
| Vs A :: ur ⇒ count_chars ur
| Ts t :: ur ⇒ S (count_chars ur)
end.
Fixpoint count_sep G :=
match G with
[] ⇒ 0
| R A u :: Gr ⇒ if decision (|u| < 2) then count_sep Gr
else count_chars u + count_sep Gr
end.
Definition sep G := it step (count_sep G) G.
Definition charfree u := ∀ s, s el u → ∃ A, s = Vs A.
Definition uniform G := ∀ A u, R A u el G → ∀ a, Ts a el u → u = [Ts a].
Instance dec_charfree u : dec (charfree u).
Proof.
unfold charfree.
induction u as [| [a | A] u IHu].
- left. intros s H. destruct H.
- right. intros H.
assert (H0 : Ts a el (Ts a :: u)) by auto.
destruct (H (Ts a) H0) as [A H']. inv H'.
- destruct IHu as [IH | IH].
+ left. intros s [H | H] ; [ ∃ A |] ; auto.
+ right. intros H. apply IH.
intros s H0. apply H. auto.
Defined.
Lemma pickChar u :
¬ charfree u → { a | Ts a el u}.
Proof.
intros H.
induction u as [| [a | A] u IHu].
- exfalso. apply H. intros s H0. destruct H0.
- ∃ a. auto.
- assert (H0 : ¬ charfree u). {
intros H0. apply H.
intros s H1. destruct H1 as [H1 | H1] ; [∃ A| ] ; auto. }
destruct (IHu H0) as [a H1]. ∃ a. auto.
Qed.
Lemma pickCharRule G :
{ a | ∃ A u, R A u el G ∧ (Ts a) el u ∧ |u| ≥ 2} + uniform G.
Proof.
induction G as [| [A u] Gr IHGr].
- right. intros A u [].
- destruct IHGr as [[a IH] | IH].
+ left. ∃ a. destruct IH as [A' [u' [H0 [H1 H2]]]].
∃ A', u'. repeat split ; auto.
+ decide (charfree u) as [D | D].
× right. intros A' u' [H0 | H0] a H1 ; eauto.
inv H0. destruct (D (Ts a) H1) as [b T]. inv T.
× { apply pickChar in D. destruct D as [a D].
destruct u as [| [b | B] [| s u]].
- exfalso. destruct D as [].
- right. intros A' u' [H0 | H0] c H1 ; eauto.
inv H0. destruct H1 as [H1 | H1] ; now inv H1.
- left. ∃ a, A, (Ts b :: s :: u). repeat split ; simpl ; auto ; omega.
- exfalso. destruct D as [D | D] ; inv D.
- left. ∃ a, A, (Vs B :: s :: u). repeat split ; simpl ; auto ; omega. }
Qed.
Definition step (G : grammar) : grammar.
destruct (pickCharRule G) as [[a H] | H ].
- destruct (pickFresh G) as [B N].
exact (R B [Ts a] :: substG G (Ts a) [Vs B]).
- exact G.
Defined.
Fixpoint count_chars u :=
match u with
[] ⇒ 0
| Vs A :: ur ⇒ count_chars ur
| Ts t :: ur ⇒ S (count_chars ur)
end.
Fixpoint count_sep G :=
match G with
[] ⇒ 0
| R A u :: Gr ⇒ if decision (|u| < 2) then count_sep Gr
else count_chars u + count_sep Gr
end.
Definition sep G := it step (count_sep G) G.
Lemma count_sep_split G G' :
count_sep (G ++ G') = count_sep G + count_sep G'.
Proof.
induction G as [| [A u] Gr IHGr] ; simpl ; try decide (| u | < 2) ; auto.
rewrite <- plus_assoc. now f_equal.
Qed.
Lemma count_chars_substL u a B :
count_chars u ≥ count_chars (substL u (Ts a) [Vs B]).
Proof.
induction u as [| [b | A] u] ; simpl ; auto.
decide (Ts b = Ts a) ; simpl ; omega.
Qed.
Lemma count_sep_substL G a B :
count_sep G ≥ count_sep (substG G (Ts a) [Vs B]).
Proof.
induction G as [| [A u] Gr IHGr] ; simpl ; auto.
decide (| u | < 2) as [D | D] ; rewrite substL_length_unit with (x := Ts a) (x' := Vs B) (D := symbol_eq_dec) in D ;
decide (| substL u (Ts a) [Vs B] | < 2) ; try tauto.
cut (count_chars u ≥ count_chars (substL u (Ts a) [Vs B])) ; try omega.
apply count_chars_substL.
Qed.
Lemma count_chars_split u1 u2 :
count_chars (u1 ++ u2) = count_chars u1 + count_chars u2.
Proof.
induction u1 as [| [a | A] u1] ; simpl ; auto.
Qed.
Lemma count_chars_decr B u a :
Ts a el u → count_chars u > count_chars (substL u (Ts a) [Vs B]).
Proof.
intros H0.
apply in_split in H0.
destruct H0 as [u1 [u2 H0]]. rewrite H0.
replace (u1 ++ Ts a :: u2) with (u1 ++ [Ts a] ++ u2) by auto.
repeat rewrite substL_split.
repeat rewrite count_chars_split.
repeat rewrite plus_assoc.
cut (count_chars [Ts a] > count_chars (substL [Ts a] (Ts a) [Vs B])).
- intros H2.
pose (count_chars_substL u1 a B).
pose (count_chars_substL u2 a B). omega.
- simpl. decide (Ts a = Ts a) ; try tauto. auto.
Qed.
Lemma count_sep_decr G A B u a :
R A u el G → Ts a el u → |u| ≥ 2 → count_sep G > count_sep (substG G (Ts a) [Vs B]).
Proof.
intros H U T.
apply in_split in H.
destruct H as [G1 [G2 H]]. rewrite H.
replace (G1 ++ R A u :: G2) with (G1 ++ [R A u] ++ G2) by auto.
do 2 rewrite substG_split.
repeat rewrite count_sep_split.
repeat rewrite plus_assoc.
cut (count_sep [R A u] > count_sep (substG [R A u] (Ts a) [Vs B])).
- intros C. pose (C0 := count_sep_substL G1 a B).
pose (C1 := count_sep_substL G2 a B). omega.
- simpl. decide (| u | < 2) as [D | D] ; try omega.
rewrite substL_length_unit with (x := Ts a) (x' := Vs B) (D := symbol_eq_dec) in D.
decide (| substL u (Ts a) [Vs B] | < 2) ; try tauto.
do 2 rewrite <- plus_n_O.
now apply count_chars_decr.
Qed.
Lemma count_decr G :
step G ≠ G → count_sep G > count_sep (step G).
Proof.
intros St.
unfold step in ×.
destruct (pickCharRule G) as [[a [B [v [H0 [H1 H2]]]]] | H ] ; try tauto.
destruct (pickFresh G) as [C N].
simpl. eapply count_sep_decr ; eauto.
Qed.
Lemma fp_sep G :
FP step (sep G).
Proof.
apply it_fp. intros n.
decide (step (it step n G) = (it step n G)).
- left. auto.
- right. simpl. now apply count_decr in n0.
Qed.
Lemma fp_uniform G :
FP step G → uniform G.
Proof.
intros Ss.
unfold step, FP in Ss.
destruct (pickCharRule G) as [[a [B [v [H0 [H1 H2]]]]] | H ].
- destruct (pickFresh G) as [C N].
destruct G ; inversion Ss.
exfalso. assert (H5 : Vs C el symbs (r :: G)) by (rewrite <- Ss ; simpl ; auto).
specialize (N (Vs C) H5). unfold sless' in N. destruct B as [i] ; omega.
- intros A' u' Ru'. specialize (H A' u' Ru') ; auto.
Qed.
Lemma sep_uniform G :
uniform (sep G).
Proof.
apply fp_uniform, fp_sep.
Qed.
Lemma substG_der_equiv G A u B s :
fresh G (Vs B) → A ≠ B → s ≠ Vs B → terminal u → (der (R B [s] :: (substG G s [Vs B])) A u ↔ der G A u).
Proof.
intros N Do U T.
split ; intros D.
- rewrite <- substG_undo with (G := G) (B := B) (s := s) ; auto.
apply der_G_substG ; auto ; intros H.
+ rewrite substG_dom in H. apply symbs_dom in H.
apply fresh_symbs in N. tauto.
+ destruct H ; tauto.
+ destruct (T (Vs B) H) as [t T']. inv T'.
- rewrite <- substG_undo with (G := G) (B := B) (s := s) in D ; auto.
now apply der_substG_G.
Qed.
Lemma step_der_equiv G A u :
Vs A el dom G → terminal u → (der (step G) A u ↔ der G A u).
Proof.
intros Do T.
unfold step.
destruct (pickCharRule G) as [[a [B [v [H0 [H1 H2]]]]] | H ] ; [| firstorder].
destruct (pickFresh G) as [C N].
apply substG_der_equiv ; auto.
- intros H. inv H. apply symbs_dom in Do.
specialize (N (Vs C) Do). unfold sless' in N. omega.
- intros H5. inv H5.
Qed.
Lemma step_dom G :
dom G <<= dom (step G).
Proof.
unfold step.
destruct (pickCharRule G) as [[a [B [v [H0 [H1 H2]]]]] | H ] ; auto.
destruct (pickFresh G) as [C N].
simpl. rewrite substG_dom. auto.
Qed.
Lemma sep_der_equiv G A u :
Vs A el dom G → terminal u → (der (sep G) A u ↔ der G A u).
Proof.
unfold sep. remember (count_sep G) as n. clear Heqn.
revert G.
induction n ; intros G D T ; simpl ; try tauto.
rewrite step_der_equiv ; auto.
apply it_ind ; auto.
intros G' H0. now apply step_dom.
Qed.
Lemma sep_language G A u :
Vs A el dom G → (language G A u ↔ language (sep G) A u).
Proof.
intros D.
split ; intros [L0 L1] ; split ; try eapply sep_der_equiv ; eauto.
Qed.