File CoMoLang.L_Empty

Require Import List Logic.FinFun.

From CoMoLang Require Import Languages Grammars.

In this file, we want to build the empty language over any alphabet.

Section Empty.

Variable Sigma : Set.

Hypothesis Sigma_fin : Finite Sigma.

First of all, we define the empty language.

  Definition P_Empty : list Sigma → Prop := fun _ ⇒ False.
  #[export] Instance L_Empty : Language Sigma.
  Proof.
    split.
    -
      exact P_Empty.
    -
      exact Sigma_fin.
  Defined.

Next step, we define a grammar, which produces exactly the empty language.

  Definition R_Empty {Sigma : Set} : let term := list (sum unit Sigma) in term → term → Prop := fun _ _ ⇒ False.
  #[export, refine] Instance G_Empty : Grammar unit Sigma := { rule := R_Empty; S := tt}.
  Proof.
    -
      ∃ (tt :: nil);
      intros [];
      firstorder.
    -
      exact Sigma_fin.
  Defined.

Now we prove, that our grammar G_Empty indeed produces L_Empty.

  Check grammar_produces.

  Theorem L_equiv_G : grammar_produces G_Empty L_Empty.
  Proof.
    split.
    -

L_Empty ~> L(G_Empty)

induction w; contradiction.
-

L(G_Empty) ~> L_Empty

intros H1.

Some unfolding to make visible, what we want acutally to show.

repeat red in H1;
repeat red.

We want to build a contradiction on the fact, that there exists no rule, so there cannot be a derivation of any word w.

      inversion H1; subst.
      destruct w; discriminate.
      inversion H0; subst.
      inversion H4.
  Qed.

End Empty.