Library CFG.ElimU
alternative definiton of Domain, with other type than dom
Fixpoint domV G : list var :=
match G with
[] ⇒ []
| R A u :: Gr ⇒ A :: domV Gr
end.
Lemma dom_domV G A :
A el (domV G) ↔ Vs A el (dom G).
Proof.
induction G as [| [B u] Gr] ; simpl ; [tauto|].
rewrite IHGr. split ; intros [H | H] ; try inv H ; auto.
Qed.
Lemma rule_domVG G A u :
R A u el G → A el domV G.
Proof.
rewrite dom_domV.
apply rule_domG.
Qed.
Lemma domVG_rule G A :
A el (domV G) → ∃ u, R A u el G.
Proof.
intros H.
apply dom_domV, domG_rule in H.
destruct H as [A' [u [H0 H1]]].
∃ u. now inv H0.
Qed.
match G with
[] ⇒ []
| R A u :: Gr ⇒ A :: domV Gr
end.
Lemma dom_domV G A :
A el (domV G) ↔ Vs A el (dom G).
Proof.
induction G as [| [B u] Gr] ; simpl ; [tauto|].
rewrite IHGr. split ; intros [H | H] ; try inv H ; auto.
Qed.
Lemma rule_domVG G A u :
R A u el G → A el domV G.
Proof.
rewrite dom_domV.
apply rule_domG.
Qed.
Lemma domVG_rule G A :
A el (domV G) → ∃ u, R A u el G.
Proof.
intros H.
apply dom_domV, domG_rule in H.
destruct H as [A' [u [H0 H1]]].
∃ u. now inv H0.
Qed.
Definition unitfree G := ∀ A, ¬ ∃ B, R A [Vs B] el G.
Section UnitRules.
Variable G : grammar.
Definition rules (u : list var) (v : list phrase) := product R u v.
Definition N : grammar := rules (domV G) (ran G).
Definition step M s :=
match s with
R A u ⇒ (¬ (∃ B, u = [Vs B]) ∧ R A u el G)
∨ (∃ B, R A [Vs B] el G ∧ R B u el M)
end.
Instance step_dec' G' M A u : dec (∃ B, R A [Vs B] el G' ∧ R B u el M).
Proof.
induction M as [| [C w] Mr IHMr].
- right. intros [B [H0 []]].
- destruct IHMr as [IH | IH].
+ left. destruct IH as [B [H0 H1]].
∃ B. split ; auto.
+ decide (R A [Vs C] el G' ∧ w = u) as [D | D].
× left. ∃ C. destruct D as [D0 D1]. rewrite D1. split ; auto.
× right. intros [B [H0 [H1 | H1]]].
{ apply D. inv H1. auto. }
{ apply IH. ∃ B. split ; auto. }
Defined.
Instance step_dec M s : dec (step M s).
Proof.
destruct s as [A u].
simpl. induction G as [| [B v] Gr IHGr].
- right. intros [[H0 H1] | [B [H1 H2]]] ; try now inv H1.
- destruct IHGr as [IH | IH].
+ left. destruct IH as [[IH0 IH1] | [C [IH0 IH1]]].
× left. split ; auto.
× right. ∃ C. split ; auto.
+ decide (R A u = R B v ∧ ¬ (∃ C, u = [Vs C])) as [D | D].
× left. destruct D as [H0 H1].
left. inv H0. split ; auto.
× decide (∃ B0 : var, R A [Vs B0] el R B v :: Gr ∧ R B0 u el M) as [D0 | D0].
{ left. now right. }
{ right. intros [[H0 [H1 | H1]] | H0] ; try inv H1 ; try split ; auto. }
Defined.
Definition elimU : grammar :=
FCI.C (step := step) N.
Lemma unitfree_elimU' :
inclp elimU (fun i ⇒ match i with R A u ⇒ ¬ ∃ B, u = [Vs B] end).
Proof.
apply FCI.ind.
intros M [A u] Icl VG S.
destruct S as [[S0 S1] | [C [S0 S1]]] ; [|specialize (Icl (R C u) S1) ; simpl] ; auto.
Qed.
Lemma unitfree_elimU :
unitfree elimU.
Proof.
intros A [B H]. apply (unitfree_elimU' H). now (∃ B).
Qed.
Lemma elimU_corr A u :
R A u el G → (¬ ∃ B, u = [Vs B]) → R A u el elimU.
Proof.
intros H0 H1.
apply FCI.closure.
- apply prod_corr. ∃ A, u.
repeat split ; eauto using rule_domVG, rule_ranG.
- left. split ; auto.
Qed.
Lemma ran_elimU_G u :
u el ran elimU → u el ran G.
Proof.
intros H.
apply ranG_rule in H. destruct H as [A H].
unfold elimU in H. apply FCI.incl, prod_corr in H.
destruct H as [? [? [H0 [_ ?]]]]. now inv H0.
Qed.
Lemma elimU_corr2 A B u :
R A [Vs B] el G → R B u el elimU → R A u el elimU.
Proof.
intros H0 H1.
apply FCI.closure.
- apply prod_corr.
∃ A, u. repeat split ; auto.
+ eapply rule_domVG ; eauto.
+ apply rule_ranG in H1. now apply ran_elimU_G in H1.
- simpl. right. ∃ B. split ; auto.
Qed.
R A u el G → (¬ ∃ B, u = [Vs B]) → R A u el elimU.
Proof.
intros H0 H1.
apply FCI.closure.
- apply prod_corr. ∃ A, u.
repeat split ; eauto using rule_domVG, rule_ranG.
- left. split ; auto.
Qed.
Lemma ran_elimU_G u :
u el ran elimU → u el ran G.
Proof.
intros H.
apply ranG_rule in H. destruct H as [A H].
unfold elimU in H. apply FCI.incl, prod_corr in H.
destruct H as [? [? [H0 [_ ?]]]]. now inv H0.
Qed.
Lemma elimU_corr2 A B u :
R A [Vs B] el G → R B u el elimU → R A u el elimU.
Proof.
intros H0 H1.
apply FCI.closure.
- apply prod_corr.
∃ A, u. repeat split ; auto.
+ eapply rule_domVG ; eauto.
+ apply rule_ranG in H1. now apply ran_elimU_G in H1.
- simpl. right. ∃ B. split ; auto.
Qed.
rules in elimU can be simulated by a derivation
Lemma elimU_corr3' :
inclp elimU (fun i ⇒ match i with R A u ⇒ derf G [Vs A] u end).
Proof.
unfold elimU. apply FCI.ind.
intros M [A u] Icl V S.
destruct S as [[S0 S1] | [B [S0 S1]]] ; [|specialize (Icl (R B u) S1)] ; eauto.
Qed.
Lemma elimU_corr3 A u :
R A u el elimU → derf G [Vs A] u.
Proof. intros elimU. exact (elimU_corr3' elimU). Qed.
inclp elimU (fun i ⇒ match i with R A u ⇒ derf G [Vs A] u end).
Proof.
unfold elimU. apply FCI.ind.
intros M [A u] Icl V S.
destruct S as [[S0 S1] | [B [S0 S1]]] ; [|specialize (Icl (R B u) S1)] ; eauto.
Qed.
Lemma elimU_corr3 A u :
R A u el elimU → derf G [Vs A] u.
Proof. intros elimU. exact (elimU_corr3' elimU). Qed.
completeness of derivability
Lemma derfG_derfelimU u v :
terminal v → derf G u v → derf elimU u v.
Proof.
intros T D.
induction D as [| A u v H H0 IHD|] ; auto.
- specialize (IHD T).
decide (∃ B, u = [Vs B]) as [D | D].
+ destruct D as [B U'].
assert (H1 : ∃ v', R B v' el elimU ∧ derf elimU v' v). {
induction IHD as [| | ? ? ? ? IH0 IHD0 IH1 IHD1] ; subst.
- assert (H1 : Vs B el [Vs B]) by auto.
destruct (T (Vs B) H1) as [t T']. inv T'.
- ∃ u. split ; inv U' ; auto.
- inv U'. inv IH1. rewrite app_nil_r in ×. apply IHD0 ; auto. }
destruct H1 as [v' [H1 H2]]. subst.
apply (elimU_corr2 H) in H1 ; eauto.
+ apply elimU_corr in H ; eauto.
- apply terminal_split in T.
destruct T as [T0 T1]. eauto.
Qed.
terminal v → derf G u v → derf elimU u v.
Proof.
intros T D.
induction D as [| A u v H H0 IHD|] ; auto.
- specialize (IHD T).
decide (∃ B, u = [Vs B]) as [D | D].
+ destruct D as [B U'].
assert (H1 : ∃ v', R B v' el elimU ∧ derf elimU v' v). {
induction IHD as [| | ? ? ? ? IH0 IHD0 IH1 IHD1] ; subst.
- assert (H1 : Vs B el [Vs B]) by auto.
destruct (T (Vs B) H1) as [t T']. inv T'.
- ∃ u. split ; inv U' ; auto.
- inv U'. inv IH1. rewrite app_nil_r in ×. apply IHD0 ; auto. }
destruct H1 as [v' [H1 H2]]. subst.
apply (elimU_corr2 H) in H1 ; eauto.
+ apply elimU_corr in H ; eauto.
- apply terminal_split in T.
destruct T as [T0 T1]. eauto.
Qed.
soundness of derivability
Lemma derfelimU_derfG u v :
derf elimU u v → derf G u v.
Proof.
induction 1 ; eauto using elimU_corr3, derf_trans.
Qed.
Lemma elimU_der_equiv u v :
terminal v → (derf G u v ↔ derf elimU u v).
Proof.
intros H. split ; auto using derfelimU_derfG, derfG_derfelimU.
Qed.
Lemma unit_language A u :
language G A u ↔ language elimU A u.
Proof.
split ; intros [L0 L1] ; split ; auto ; apply derf_der_equiv ; apply derf_der_equiv in L0 ; [rewrite <- elimU_der_equiv | rewrite elimU_der_equiv] ; auto.
Qed.
End UnitRules.
derf elimU u v → derf G u v.
Proof.
induction 1 ; eauto using elimU_corr3, derf_trans.
Qed.
Lemma elimU_der_equiv u v :
terminal v → (derf G u v ↔ derf elimU u v).
Proof.
intros H. split ; auto using derfelimU_derfG, derfG_derfelimU.
Qed.
Lemma unit_language A u :
language G A u ↔ language elimU A u.
Proof.
split ; intros [L0 L1] ; split ; auto ; apply derf_der_equiv ; apply derf_der_equiv in L0 ; [rewrite <- elimU_der_equiv | rewrite elimU_der_equiv] ; auto.
Qed.
End UnitRules.