Require Export Inlining.

Module Separate.

  Import Base Lists Definitions Derivation Symbols (* Dec_Empty*) Inlining.

  Section Separate.

    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 charfree u := ∀ s, s el u → ∃ A, s = @Vs Tt Vt A.
    Definition uniform G := ∀ A u, R A u el G → ∀ a, @Ts Tt Vt a el u → u = [Ts a].

    Global Instance dec_charfree u : dec (charfree u).

    Lemma pickChar u :
      ¬ charfree u → { a | Ts a el u}.

    Lemma pickCharRule G :
      { a | ∃ A u, R A u el G ∧ (Ts a) el u ∧ |u| ≥ 2} + uniform G.
    Definition step (G : @grammar Tt Vt) : @grammar Tt Vt.
    Defined.

    Fixpoint count_chars (u: @phrase Tt Vt) :=
      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'.

    Lemma count_chars_substL u a B :
      count_chars u ≥ count_chars (substL u (Ts a) [Vs B]).

    Lemma count_sep_substL G a B :
      count_sep G ≥ count_sep (substG G (Ts a) [Vs B]).

    Lemma count_chars_split u1 u2 :
      count_chars (u1 ++ u2) = count_chars u1 + count_chars u2.

    Lemma count_chars_decr B u a :
      Ts a el u → count_chars u > count_chars (substL u (Ts a) [Vs B]).

    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]).

    Lemma count_decr G :
      step G ≠ G → count_sep G > count_sep (step G).

    Lemma fp_sep G :
      FP step (sep G).

    Lemma fp_uniform G :
      FP step G → uniform G.

    Lemma sep_uniform G :
      uniform (sep G).

    Lemma substG_der_equiv G A u B s :
      @fresh Tt Vt TtToNat VtToNat 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).

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

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

    Lemma sep_der_equiv G A u :
      Vs A el dom G → terminal u → (der (sep G) A u ↔ der G A u).

    Lemma sep_language G A u :
      Vs A el dom G → (language G A u ↔ language (sep G) A u).

  End Separate.

End Separate.