Require Export Separate.

Module Binarize.

  Import Base Definitions Symbols Derivation Inlining.

  Section Binarize.

    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.

    Fixpoint step G G' :=
      match G' with
          [] ⇒ []
        | R A [] :: Gr ⇒ R A [] :: step G Gr
        | R A [s0] :: Gr ⇒ R A [s0] :: step G Gr
        | R A [s0 ; s1] :: Gr ⇒ R A [s0 ; s1] :: step G Gr
        | R A (s0 :: ur) :: Gr ⇒
          let (B, H) := @pickFresh _ _ TtToNat VtToNat NatToVt Id3 G
          in R A [s0 ; Vs B] :: @R Tt Vt B ur :: Gr
      end.

    Definition step' G := step G G.

    Fixpoint count_bin (G: @grammar Tt Vt) :=
      match G with
          [] ⇒ 0
        | R A u :: Gr ⇒ if decision ((|u|) ≤ 2) then count_bin Gr else |u| + count_bin Gr
      end.

    Definition bin G := it step' (count_bin G) G.

    Definition binary G := ∀ A u, @R Tt Vt A u el G → (|u|) ≤ 2.

    Lemma count_decr G G' :
      step G' G ≠ G → count_bin G > count_bin (step G' G).

    Lemma fp_bin G :
      FP step' (bin G).

    Lemma fp_binary G :
      FP step' G → binary G.

    Lemma bin_binary G :
      binary (bin G).

    Lemma step_or G G' :
      step G' G = G ∨ ∃ A Gr B u s, G === R A (s :: u) :: Gr ∧ step G' G === R A [s ; Vs B] :: R B u :: Gr ∧ ¬ Vs B el symbs G'.

    Lemma step_der_equiv G A u :
      terminal u → (Vs A) el dom G → (der G A u ↔ der (step G G) A u).

    Lemma step_dom G G' :
      dom G <<= dom (step G' G).

    Lemma bin_der_equiv G A u :
      terminal u → (Vs A) el dom G → (der G A u ↔ der (bin G) A u).

    Lemma bin_language G A u :
      Vs A el dom G → (language G A u ↔ language (bin G) A u).

  End Binarize.

End Binarize.