Require Export Basics Separation Binarize ElimE ElimU.
Local Open Scope program_scope.

Definition chomsky G := efree G ∧ uniform G ∧ binary G ∧ unitfree G.
Definition normalize := elimU ∘ elimE ∘ sep ∘ bin.

Lemma substG_preservesLength G s s' :
  binary G → binary (substG G s [s']).
Proof.
  intros H. induction G as [| [A u] G IHG] ; simpl ; auto.
  intros B v [E | E].
  - inv E. rewrite <- substL_length_unit ; eauto.
  - eapply IHG ; eauto.
    intros B' v' E'. eapply H ; eauto.
Qed.

Lemma binary_sep G : binary G → binary (sep G).
Proof.
  intros H.
  unfold sep.
  apply it_ind ; auto.
  intros G' Bi.
  unfold Separation.step.
  destruct (pickCharRule G') as [[a [B [v [H0 [H1 H2]]]]] | H0 ] ; auto.
  destruct (pickFresh G') as [C N].
  cut (binary (substG G' (Ts a) [Vs C])) ; auto using substG_preservesLength.
  intros Bin A u E. destruct E ; [inv H3 | ] ; eauto.
Qed.

Lemma binary_elimE G : binary G → binary (elimE G).
Proof.
  intros H A u H0.
  apply delE_rules, closure_slist in H0.
  destruct H0 as [u' [H0 H1]].
  apply slist_length in H1.
  specialize (H A u' H0). omega.
Qed.

Lemma binary_unit G : binary G → binary (elimU G).
Proof.
  intros H A u H0.
  apply rule_ranG, ran_elimU_G, ranG_rule in H0.
  destruct H0 as [B H0].
  apply (H B u H0).
Qed.

Lemma excluded_free G : uniform G → uniform (elimE G).
Proof.
  intros H A u H0 a E.
  apply delE_rules in H0.
  apply closure_slist in H0.
  destruct H0 as [u' [H1 H2]].
  assert (H4 : Ts a el u') by (apply slist_subsumes in H2 ; auto).
  specialize (H A u' H1 a H4).
  subst. inv H2.
  - inv H6. destruct E.
  - now inv H3.
Qed.

Lemma excluded_unit G : uniform G → uniform (elimU G).
Proof.
  intros H A u Ru.
  apply rule_ranG, ran_elimU_G, ranG_rule in Ru.
  destruct Ru as [B H0].
  apply (H B u H0).
Qed.

Lemma efree_unit G : efree G → efree (elimU G).
Proof.
  intros H A u Ru.
  apply rule_ranG, ran_elimU_G, ranG_rule in Ru.
  destruct Ru as [B H0].
  apply (H B u H0).
Qed.

Lemma chomsky_normalform G :
  chomsky (normalize G).
Proof.
  repeat split.
  - apply efree_unit, efree_elimE.
  - apply excluded_unit, excluded_free, sep_uniform.
  - apply binary_unit, binary_elimE, binary_sep, bin_binary.
  - apply unitfree_elimU.
Qed.

Lemma bin_dom G :
  dom G <<= dom (bin G).
Proof.
  unfold bin.
  apply it_ind ; auto.
  intros G' H.
  setoid_transitivity (dom G') ; auto.
  apply Binarize.step_dom.
Qed.

Lemma language_normalform G A u :
  Vs A el dom G → u ≠ [] → (language G A u ↔ language (normalize G) A u).
Proof.
  intros Do U.
  unfold normalize.
  rewrite bin_language ; auto.
  rewrite sep_language ; try now apply bin_dom.
  rewrite elimE_language ; auto.
  now rewrite unit_language.
Qed.