Require Export Lists.
Require Export Symbols.

Module Derivation.

  Import Base Lists Definitions Symbols ListNotations.

  Section DerivabilityAndLanguages.

    Context {Tt Vt: Type}.

    Inductive der (G : grammar) (A : var) : list (@symbol Tt Vt) → Prop :=
    | vDer : der G A [Vs A]
    | rDer l : (R A l) el G → der G A l
    | replN B u w v : der G A (u ++ [Vs B] ++ w) → der G B v → der G A (u ++ v ++ w).
    Hint Constructors der.

    Definition terminal (u : (@phrase Tt Vt)) : Prop :=
      ∀ s, s el u → ∃ t, s = Ts t.

    Lemma terminal_split u v :
      terminal (u ++ v) → terminal u ∧ terminal v.

    Definition language (G : grammar) (A : var) (u : phrase) : Prop :=
      der G A u ∧ terminal u.

  (*End DerivabilityAndLanguages.

  (** * Alternative characterizations of derivability *)
  Section AlternativeCharacterizationsOfDerivability. *)

    (* Context {Tt Vt: Type}. *)

    Inductive derL (G : grammar) (A : var) : list (@symbol Tt Vt) → Prop :=
    | sDer : derL G A [Vs A]
    | gDer B u v w : (R B v) el G → derL G A (u ++ [Vs B] ++ w) → derL G A (u ++ v ++ w).
    Hint Constructors derL.

    Inductive derT (G : grammar) : list symbol → list (@symbol Tt Vt) → Prop :=
    | derTRefl u : derT G u u
    | derTRule A u : R A u el G → derT G [Vs A] u
    | derTTrans u v w x y : derT G x (u ++ y ++ w) → derT G y v → derT G x (u++v++w).
    Hint Constructors derT.

    Inductive derf (G : grammar) : phrase → (@phrase Tt Vt) → Prop :=
    | fRefl u : derf G u u
    | fRule A u v : R A u el G → derf G u v → derf G [Vs A] v
    | fCons s u v w : derf G [s] v → derf G u w → derf G (s :: u) (v ++ w).
    Hint Constructors derf.

    Inductive derI (G : @grammar Tt Vt) : phrase → phrase → Prop :=
    | derIRefl u : derI G u u
    | derIRule A u v w : R A v el G → derI G (u ++ [Vs A] ++ w) (u ++ v ++ w)
    | derITrans u v w : derI G u v → derI G v w → derI G u w.
    Hint Constructors derI.

  (*End AlternativeCharacterizationsOfDerivability.

  (** ** Linear equivalences *)
  Section LinearEquivalences. *)

    (*Context {Tt Vt: Type}. *)

    Lemma derL_der_equiv (G : @grammar Tt Vt) (A : var) (u : list symbol) :
      der G A u ↔ derL G A u.

    Lemma derT_der_equiv (G : grammar) (A : var) (u : list symbol) :
      der G A u ↔ derT G [Vs A] u.

    Lemma derf_concat G u1 u2 v1 v2 :
      derf G u1 v1 → derf G u2 v2 → derf G (u1 ++ u2) (v1 ++ v2).

    Lemma derf_split G u u1 u2 v :
      derf G u v → u = u1 ++ u2 → ∃ v1 v2, v = v1 ++ v2 ∧ derf G u1 v1 ∧ derf G u2 v2.

    Lemma derf_trans G u v w :
      derf G u v → derf G v w → derf G u w.

    Lemma derf_derT G u v :
      derf G u v → derT G u v.

    Lemma derT_derI (G: @grammar Tt Vt) u v :
      derT G u v → derI G u v.

    Lemma derI_derf G u v :
      derI G u v → derf G u v.

    Lemma derf_der_equiv G A u :
      derf G [Vs A] u ↔ der G A u.

    Lemma derT_trans (G : grammar) (u v w : list symbol) :
      derT G u v → derT G v w → derT G u w.

    Lemma derT_concat G u u' v v' :
      derT G u v → derT G u' v' → derT G (u ++ u') (v ++ v').

    Lemma der_subset G1 G2 A u :
      G1 <<= G2 → der G1 A u → der G2 A u.

    Lemma der_equiv_G G1 G2 A u :
      G1 === G2 → (der G1 A u ↔ der G2 A u).

    Lemma symbs_der G A u :
      ¬ Vs A el symbs G → der G A u → u = [Vs A].

  End DerivabilityAndLanguages.

End Derivation.