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

Module Chomsky.

  Import Base Lists Definitions Symbols Derivation ElimE Separate Binarize ElimU Inlining.

  Section Chomsky.

    Context {Tt Vt: Type}.
    Context {Tt_eqdec: eq_dec Tt}.
    Context {Vt_eqdec: eq_dec Vt}.

    Context {TtToNat: Tt → nat}.
    Context {VtToNat: Vt → nat}.
    Context {NatToTt: nat → Tt }.
    Context {NatToVt: nat → Vt}.

    Hypothesis Id1: ∀ x, TtToNat (NatToTt x) = x.
    Hypothesis Id2: ∀ x, NatToTt (TtToNat x) = x.
    Hypothesis Id3: ∀ x, VtToNat (NatToVt x) = x.
    Hypothesis Id4: ∀ x, NatToVt (VtToNat x) = x.


    Definition chomsky (G: @grammar Tt Vt) := efree G ∧ uniform G ∧ binary G ∧ unitfree G.
    Definition normalize :=
      elimU
        ∘ elimE
        ∘ (@sep Tt Vt _ _ TtToNat VtToNat NatToVt Id3)
        ∘ (@bin Tt Vt TtToNat VtToNat NatToVt Id3).

    Lemma substG_preservesLength (G: @grammar Tt Vt) s s' :
      binary G → binary (substG G s [s']).

    Lemma binary_sep (G: @grammar Tt Vt) :
      binary G → binary (@sep Tt Vt _ _ TtToNat _ _ Id3 G).

    Lemma binary_elimE (G: @grammar Tt Vt) : binary G → binary (elimE G).

    Lemma binary_unit (G: @grammar Tt Vt) : binary G → binary (elimU G).

    Lemma excluded_free (G: @grammar Tt Vt) : uniform G → uniform (elimE G).

    Lemma excluded_unit (G: @grammar Tt Vt) : uniform G → uniform (elimU G).

    Lemma efree_unit (G: @grammar Tt Vt) : efree G → efree (elimU G).

    Lemma chomsky_normalform (G: @grammar Tt Vt) :
      chomsky (normalize G).

    Lemma bin_dom (G: @grammar Tt Vt):
      dom G <<= dom (@bin Tt Vt TtToNat _ _ Id3 G).

    Lemma language_normalform G A u :
      Vs A el dom G → u ≠ [] → (language G A u ↔ language (normalize G) A u).

  End Chomsky.

End Chomsky.