File CoMoLang.L_an

Require Import List.

From CoMoLang Require Import Languages Grammars CFG RG.

In this file, we have a look on a language, which only contains words of the form a^n.

#[export] Instance L_an : Language unit.

TODO: Improve this language by using any alphabet (and any letter).

Proof.
  split.
  -
    intros; exact True.
  -
    ∃ (tt :: nil); intros []; firstorder.
Defined.

We define a grammar to produce this language.

Inductive R_an : let term := list (unit + unit) in term → term → Prop :=
  | R_an_1 : R_an (inl tt :: nil) (inr tt :: inl tt :: nil)
  | R_an_2 : R_an (inl tt :: nil) nil
      .

Definition R_an' (t : prod (list (unit + unit)) (list (unit + unit))) :=
  let (t1,t2) := t in R_an t1 t2.

#[export,refine] Instance G_an : Grammar unit unit := { rule := R_an; S := tt}.
Proof.
  - ∃ (tt :: nil); intros []; firstorder.
  - ∃ (tt :: nil); intros []; firstorder.
Defined.

G_an is indeed a CFG.

#[export] Instance G_an_cfg : CFG unit unit.
Proof.
econstructor;
destruct 1; ∃ tt; reflexivity.
Defined.

G_an is indeed a RG.

#[export] Instance G_an_rg : RG unit unit.
Proof.
econstructor;
destruct 1; [left; do 2 eexists | right;right]; reflexivity.
Defined.

We show, that our grammar G_an indeed produces L_an.

Theorem L_an_equiv_G_an : grammar_produces G_an L_an.
Proof.
  split.
  -
    induction w as [|[] w IH]; intros H1.
    +
      apply derive_step; apply step_rule; constructor.
    +
      eapply derive_multi.

      apply derive_step; apply step_rule; exact R_an_1.

      assert (inr tt :: inl tt :: nil = (inr tt :: nil ) ++ (inl tt :: nil ) ∧ convert unit (tt :: w) = (inr tt :: nil ) ++ convert unit w) as [H2 H3]. { split; reflexivity. }
      rewrite H2,H3.
      apply derive_derive_r; apply IH; easy.
  -
    easy.
Qed.

In addition, we can show now, that L_an is rg. , because there is a RG, which produces L_an.

Corollary L_an_regulary : is_regular L_an.
Proof.
  repeat red.
  ∃ unit.
  ∃ G_an_rg.
  exact L_an_equiv_G_an.
Qed.