File CoMoLang.CFG

Require Import List.

From CoMoLang Require Import Languages Grammars.

Context-free grammars (CFG) are grammars, where the left side of a rule X -> Y only consists out of exact one variable.

Class CFG (V Sigma : Set) :=
  {
    CFG_Grammar :> Grammar V Sigma;
    rule_left_side :
      ∀ t1 t2,
        @rule V Sigma CFG_Grammar t1 t2 →
        ∃ (v : V ),
          t1 = (inl v ) :: nil
  }.

A language L is called context-free (cf.), iff there is a CFG, which produces L.

Definition is_cf {Sigma} `(L : Language Sigma) :=
∃ (V : Set) `(G : CFG V Sigma ),
grammar_produces (@CFG_Grammar V Sigma G) L.

Print is_cf.

A trivial helper fact.

Fact left_side_just_vars {V Sigma} `(G : CFG V Sigma) :
  ∀ t1 t2,
    rule t1 t2 →
    just_vars t1.
Proof.
  intros t1 t2 H1.
  destruct (rule_left_side t1 t2 H1) as [v H2].
  subst; easy.
Qed.