Require Export Dec_Word.

Module ElimE.

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

  Section ElimE.

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

    Inductive nullable (G : @grammar Tt Vt) (s : symbol) : Prop :=
    | Null A u : s = Vs A → R A u el G → (∀ s', s' el u → nullable G s') → nullable G s.
    Hint Constructors nullable.

    Lemma derE_nullable (G : grammar) (A : var) (u : phrase) :
      der G A u → (∀ s, s el u → nullable G s) → nullable G (Vs A).

    Hint Constructors der.
    Lemma nullable_derE (G : grammar) (s : symbol) :
      nullable G s → ∃ A, s = Vs A ∧ der G A [].
    Ltac dupapply H1 lemma H2 := pose (H2:= H1) ; apply lemma in H2.

    Lemma nullable_derE_equi (G : grammar) (s : symbol) :
      (∃ A, s = Vs A ∧ der G A []) ↔ nullable G s.

    Global Instance nullable_dec G s : dec (nullable G s).

    Definition efree G := ∀ A u, (@R Tt Vt) A u el G → u ≠ [].

    Fixpoint closure (p : symbol → Prop) {pdec : ∀ x, dec (p x)} (G : @grammar Tt Vt) :=
      match G with
          [] ⇒ []
        | R A u :: Gr ⇒
          let
            u' := @slists _ p _ u
          in let
            G' := map (R A) u'
          in G' ++ closure Gr
      end.

    Section EClosure.
      Variable G : @grammar Tt Vt.

      Definition eclosure G:= closure (nullable G) G.
      Definition eclosed G := ∀ A u, R A u el G → ∀ v, @slist _ (nullable G) _ v u → R A v el G.

      Lemma closure_slist A v (p : symbol → Prop) {pdec : ∀ s, dec (p s)} :
        R A v el closure p G → ∃ u, R A u el G ∧ slist v u.

      Lemma slist_closure A v (p : symbol → Prop) {pdec : ∀ s, dec (p s)} :
        (∃ u, R A u el G ∧ slist v u) → R A v el closure p G.

      Lemma slist_closure_equiv A v (p : symbol → Prop) {pdec : ∀ s, dec (p s)} :
        R A v el closure p G ↔ ∃ u, R A u el G ∧ slist v u.

      Lemma nullable_eclosure s :
        nullable (eclosure G) s ↔ nullable G s.

      Lemma eclosed_eclosure : eclosed (eclosure G).

      Hint Constructors derT.
      Lemma derT_slist u v :
        @slist _ (nullable G) _ v u → derT G u v.

      Lemma eclosure_der u v :
        derT (eclosure G) u v → derT G u v.

      Lemma der_eclosure_equiv u v :
        derT G u v ↔ derT (eclosure G) u v.

    End EClosure.

    Section DelE.
      Variable G : @grammar Tt Vt.


      Definition delE (G: @grammar Tt Vt) :=
        filter (fun r ⇒ match r with R A u ⇒ u ≠ [] end) G.

      Lemma delE_efree : efree (delE G).

      Lemma delE_preserveG A u :
        R A u el G → u ≠ [] → R A u el delE G.

      Hint Constructors derL.
      Lemma delE_rules A u :
        R A u el (delE G) → R A u el G.
      Hint Constructors slist.
      Lemma der_G_delE A u v :
        eclosed G → der G A u → @slist _ (nullable G) _ v u → v ≠ [] → der (delE G) A v.

      Lemma delE_der_equiv A u :
        eclosed G → (der G A u ∧ u ≠ [] ↔ der (delE G) A u).

    End DelE.

    Definition elimE G := delE (eclosure G).

    Lemma efree_elimE G :
      efree (elimE G).

    Lemma elimE_language G A u :
      u ≠ [] → (language G A u ↔ language (elimE G) A u).

  End ElimE.

End ElimE.