Library grammar_ex

Load grammar.

Examples

This file provides examples to get used to the notion of grammar, derivation, and LL(1) conflicts.

Module ABAB.

A simple example grammar, where:
  • S -> A
  • S -> B
  • A -> a a S
  • B -> a b S
  • B -> a b
We encode S, A and B as 0, 1 and 2 respectively.

  Definition a := T 0.
  Definition b := T 1.

  Definition g : grammar :=
    (0, NT 1 :: nil) ::
    (0, NT 2 :: nil) ::
    (1, a :: a :: NT 0 :: nil) ::
    (2, a :: b :: NT 0 :: nil) ::
    (2, a :: b :: nil) ::
    nil.

  Goal deriv g (NT 0 :: nil) (a :: a :: a :: b :: nil).
  Proof.
    apply deriv_NT with (exp := NT 1 :: nil); [auto_In|].
    apply deriv_NT with (exp := a :: a :: NT 0 :: nil); [auto_In|].
    repeat apply deriv_refl.
    apply deriv_NT with (exp := NT 2 :: nil); [auto_In|].
    apply deriv_NT with (exp := a :: b :: nil); [auto_In|].
    repeat apply deriv_refl.
    apply deriv_nil.
  Qed.

End ABAB.

Module Dyck.

We now captue the language of well-parenthesized words over an alphabet featuring parentheses and brackets.
Terminals: Left/Right PARentheses/BRAckets.

  Definition LPAR := T 0.
  Definition RPAR := T 1.
  Definition LBRA := T 2.
  Definition RBRA := T 3.

The grammar features a single non-terminal.

  Definition S := 0.

  Definition g : grammar :=
    (S, nil) ::
    (S, LPAR :: NT S :: RPAR :: NT S :: nil) ::
    (S, LBRA :: NT S :: RBRA :: NT S :: nil) ::
    nil.

  Goal deriv g (NT 0 :: nil) (LPAR :: LBRA :: RBRA :: LBRA :: RBRA :: RPAR :: nil).
  Proof.
  Admitted.

The dyck grammar is LL(1): we verify two representative cases.

  Lemma not_First_nil : forall g a, ~ First g a nil.
  Proof.
  Admitted.

  Lemma not_Nullable_T : forall g a e, ~ Nullable g (T a :: e).
  Proof.
  Admitted.

  Lemma First_T : forall g a a' e, First g a (T a' :: e) -> a = a'.
  Proof.
  Admitted.

  Goal no_conflict g 0 nil (LPAR :: NT 0 :: RPAR :: NT 0 :: nil).
  Proof.
    split; intros.
    + elim (not_First_nil _ _ H).
    + elim (not_First_nil _ _ H).
    + elim (not_Nullable_T _ _ _ H0).
  Qed.

  Goal no_conflict g 0 (LPAR :: NT 0 :: RPAR :: NT 0 :: nil)
                       (LBRA :: NT 0 :: RBRA :: NT 0 :: nil).
  Proof.
  Admitted.

End Dyck.