Require Export Definitions Derivation Symbols.

Module Dec_Empty.

  Import Base Lists Definitions Derivation Symbols.

  Section Dec_Empty.

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

    Variable G : @grammar Tt Vt.
    Hint Constructors derf.

    Inductive productive (G : @grammar Tt Vt) : symbol → Prop :=
    | TProd (a : ter) : productive G (Ts a)
    | VProd A u : R A u el G → (∀ s, s el u → productive G s) → productive G (Vs A).
    Hint Constructors productive.

    Lemma derf_productive u v :
      derf G u v → (∀ s, s el v → productive G s) → ∀ s, s el u → productive G s.

    Lemma productive_derf s :
      productive G s → ∃ x, derf G [s] x ∧ terminal x.

    Lemma productive_derWord_equi A :
      (∃ w, der G A w ∧ terminal w) ↔ productive G (Vs A).

    Definition step (M : list (@symbol Tt Vt)) s :=
      (∃ a, s = @Ts Tt Vt a) ∨
      ∃ A u, s = Vs A ∧
             R A u el G ∧
             ∀ s', s' el u → s' el M.

    Global Instance step_dec M s : dec (step M s).


    Definition P : list (@symbol Tt Vt) :=
      FCI.C (step := step) (symbs G).

    Lemma productive_P s :
      s el symbs G → productive G s → s el P.

    Lemma P_productive s :
      s el P → productive G s.

    Lemma P_productive_equiv s :
      s el symbs G → (s el P ↔ productive G s).

  End Dec_Empty.

  Section DecidabilityOfEmptiness.

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

    Global Instance productive_dec : ∀ (G: @grammar Tt Vt) s, dec (productive G s).

    Global Instance exists_dec : ∀ G A, dec (∃ u, @language Tt Vt G A u).

  End DecidabilityOfEmptiness.

End Dec_Empty.