Require Export Derivation.

Module ElimU.

  Import Base Lists Definitions Symbols Derivation.

  Section ElimU.

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

    Fixpoint domV (G: @grammar Tt Vt) : list var :=
      match G with
          [] ⇒ []
        | R A u :: Gr ⇒ A :: domV Gr
      end.

    Lemma dom_domV (G: @grammar Tt Vt) A :
      A el (domV G) ↔ Vs A el (dom G).

    Lemma rule_domVG G A u :
      R A u el G → A el domV G.

    Lemma domVG_rule G A :
      A el (domV G) → ∃ u, R A u el G.

    Definition unitfree (G: @grammar Tt Vt) := ∀ A, ¬ ∃ B, R A [Vs B] el G.

    Section UnitRules.
      Variable G : @grammar Tt Vt.

      Definition rules (u : list var) (v : list phrase) := product (@R Tt Vt) 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.

      Global Instance step_dec' G' M A u : dec (∃ B, (@R Tt Vt) A [Vs B] el G' ∧ (@R Tt Vt) B u el M).
      Global Instance step_dec M s : dec (step M s).
      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).

      Lemma unitfree_elimU :
        unitfree elimU.

      Lemma elimU_corr A u :
        R A u el G → (¬ ∃ B, u = [Vs B]) → R A u el elimU.

      Lemma ran_elimU_G u :
        u el ran elimU → u el ran G.

      Lemma elimU_corr2 A B u :
        R A [Vs B] el G → R B u el elimU → R A u el elimU.

      (* TODO: del *)
      Hint Constructors derf.

      Lemma elimU_corr3' :
        inclp elimU (fun i ⇒ match i with R A u ⇒ derf G [Vs A] u end).

      Lemma elimU_corr3 A u :
        R A u el elimU → derf G [Vs A] u.

      Lemma derfG_derfelimU u v :
        terminal v → derf G u v → derf elimU u v.

      Lemma derfelimU_derfG u v :
        derf elimU u v → derf G u v.

      Lemma elimU_der_equiv u v :
        terminal v → (derf G u v ↔ derf elimU u v).

      Lemma unit_language A u :
        language G A u ↔ language elimU A u.

    End UnitRules.

  End ElimU.

End ElimU.