File CoMoLang.Grammars

Require Import List Logic.FinFun.

Set Implicit Arguments.

From CoMoLang Require Import Languages.

A Grammar G = (V,Sigma,rule,S) is a 4-tuple, constisting of

a finite set of variables V
a finite alphabet Sigma
a relation rule to make clear, how this grammar constructs terms
a starting variable S.

Class Grammar (V Sigma : Set) := {
  rule : let term := list (sum V Sigma) in term → term → Prop;
  S : V;
  V_fin : Finite V;
  Sigma_fin : Finite Sigma;
  }
.

Some properties and definitions around grammars.

Section gramm.

  Variables V Sigma : Set.

  Context `(G : Grammar V Sigma).

  Definition word := list Sigma.
  Definition char := sum V Sigma.
  Definition term := list char.

We want to indicate, if a term consists just out of variables.

  Fixpoint just_vars (t : term) : Prop :=
    match t with
    | nil ⇒ True
    | c :: t' ⇒ if c then just_vars t' else False
    end.

Same for just chars.

  Fixpoint just_chars (t : term) : Prop :=
    match t with
    | nil ⇒ True
    | c :: t' ⇒ if c then False else just_chars t'
    end.

Some helper lemmas for list appending.

  Lemma app_just_vars :
    ∀ t1 t2,
    just_vars (t1 ++ t2) ↔ just_vars t1 ∧ just_vars t2.
  Proof.
    induction t1 as [|h1 t1 IH];
        split;
          try easy;
          destruct h1;
            try easy;
            apply IH.
  Qed.

  Lemma app_just_chars :
    ∀ t1 t2,
      just_chars (t1 ++ t2) ↔ just_chars t1 ∧ just_chars t2.
  Proof.
    induction t1 as [|h1 t1 IH];
        split;
          try easy;
          destruct h1;
            try easy;
            apply IH.
  Qed.

Because we are only interested in words, which can be produced by a grammar, we need a convert-function.

Definition convert (w : word) : term := map (fun x ⇒ inr x) w.

Of course, convert is injective.

  Fact convert_inj :
    ∀ w v,
      convert w = convert v →
      w = v.
  Proof.
    induction w as [|? ? IH]; intros [|] H1; try easy.
    injection H1; intros; subst.
    f_equal; apply IH; assumption.
  Qed.

convert produces just chars.

  Lemma convert_just_chars :
    ∀ w,
      just_chars (convert w).
  Proof.
    induction w as [|c w' IH].
    -
      reflexivity.
    -
      exact IH.
  Defined.

If we have a term consisting just out of chars, we can convert it to a word.

  Definition convert_rev (t : term) : just_chars t → word.
  Proof.
    intros H1.
    induction t as [|c t' IH].
    -
      exact nil.
    -
      cbn in ×.
      destruct c as [v|b].
      +
        contradiction.
      +
        apply cons; [exact b | apply IH; exact H1].
  Defined.

We want to see, that convert acts, like we expect it to.

  Corollary convert_inj_inv :
    ∀ w,
      convert_rev (convert w) (convert_just_chars w) = w.
  Proof.
    induction w as [|c w' IH].
    -
      reflexivity.
    -
      simpl; rewrite IH; reflexivity.
  Qed.

We want to know, how we can construct words with a grammar. First, we need a step-relation, which shows, how to use the rule-relation. It can be interpreted as a context-closure for rule.

  Inductive step : term → term → Prop :=
    | srule :
        ∀ t1 t2 t2' t3,
          rule t2 t2' →
          step (t1 ++ t2 ++ t3) (t1 ++ t2' ++ t3)
  .

Some helper lemmas to use the relation more efficient.

  Lemma step_rule :
    ∀ t t',
      rule t t' →
      step t t'.
  Proof.
    intros t t' ?;
    rewrite <- (app_nil_l t), <- (app_nil_l t');
    rewrite <- (app_nil_r t), <- (app_nil_r t');
    constructor; assumption.
  Qed.

  Lemma step_rule_l :
    ∀ t1 t1' t2,
      rule t1 t1' →
        step (t1 ++ t2) (t1' ++ t2).
  Proof.
    intros;
    rewrite <- (app_nil_l (t1 ++ t2)), <- (app_nil_l (t1' ++ t2));
    constructor; assumption.
  Qed.

  Lemma step_rule_r :
    ∀ t1 t2 t2',
      rule t2 t2' →
      step (t1 ++ t2) (t1 ++ t2').
  Proof.
    intros;
    rewrite <- (app_nil_r t2), <- (app_nil_r t2');
    constructor; assumption.
  Qed.

  Lemma step_step :
    ∀ t1 t2 t2' t3,
      step t2 t2' →
      step (t1 ++ t2 ++ t3) (t1 ++ t2' ++ t3).
  Proof.
    induction 1 as [t4 t5 t5' t6 H1].
    assert (H2 : ∀ t, t1 ++ (t4 ++ t ++ t6) ++ t3 = (t1 ++ t4) ++ t ++ (t6 ++ t3)).
    {
      intro; repeat rewrite app_assoc; f_equal.
      }
    repeat rewrite H2.
    constructor; assumption.
  Qed.

  Lemma step_step_l :
    ∀ t1 t1' t2,
      step t1 t1' →
      step (t1 ++ t2) (t1' ++ t2).
  Proof.
    intros;
    rewrite <- (app_nil_l (t1 ++ t2)), <- (app_nil_l (t1' ++ t2));
    apply step_step; assumption.
  Qed.

  Lemma step_step_r :
    ∀ t1 t2 t2',
      step t2 t2' →
      step (t1 ++ t2) (t1 ++ t2').
  Proof.
    intros;
    rewrite <- (app_nil_r t2), <- (app_nil_r t2');
    apply step_step; assumption.
  Qed.

The next step is the reflexive and transitive closure of step: derive.

  Inductive derive : term → term → Prop :=
    | drefl :
        ∀ t,
          derive t t
    | dtrans :
        ∀ t1 t2 t3,
          derive t1 t2 →
          step t2 t3 →
          derive t1 t3
  .

Again some helper lemmas.

  Lemma derive_step :
    ∀ t t',
      step t t' →
      derive t t'.
  Proof.
    intros t t' ?;
    rewrite <- (app_nil_l t), <- (app_nil_l t');
    rewrite <- (app_nil_r t), <- (app_nil_r t').
    econstructor; [
    constructor |
    apply step_step; assumption].
  Qed.

  Lemma derive_step_l :
    ∀ t1 t1' t2,
      step t1 t1' →
      derive (t1 ++ t2) (t1' ++ t2).
  Proof.
    intros.
    eapply dtrans.

    apply drefl.

    apply step_step_l;
    assumption.
  Qed.

  Lemma derive_step_r :
    ∀ t1 t2 t2',
      step t2 t2' →
      derive (t1 ++ t2) (t1 ++ t2').
  Proof.
    intros.
    eapply dtrans.

    apply drefl.

    apply step_step_r;
    assumption.
  Qed.

  Lemma derive_derive :
    ∀ t1 t2 t2' t3,
      derive t2 t2' →
      derive (t1 ++ t2 ++ t3) (t1 ++ t2' ++ t3).
  Proof.
    induction 1.
    -
      constructor.
    -
      eapply dtrans;
      [ eassumption |
      apply step_step;
      assumption].
  Qed.

  Lemma derive_derive_l :
    ∀ t1 t1' t2,
      derive t1 t1' →
      derive (t1 ++ t2) (t1' ++ t2).
  Proof.
    intros;
    rewrite <- (app_nil_l (t1 ++ t2)), <- (app_nil_l (t1' ++ t2));
    apply derive_derive; assumption.
  Qed.

  Lemma derive_derive_r :
    ∀ t1 t2 t2',
      derive t2 t2' →
      derive (t1 ++ t2) (t1 ++ t2').
  Proof.
    intros;
    rewrite <- (app_nil_r t2), <- (app_nil_r t2');
    apply derive_derive; assumption.
  Qed.

  Lemma derive_derive_cons :
    ∀ c t2 t2',
      derive t2 t2' →
      derive (c :: t2) (c :: t2').
  Proof.
    assert (H1 : ∀ A (l : list A) (a : A), a :: l = (a :: nil ) ++ l).
    { reflexivity. }
    intros ? t2 t2' ?;
    rewrite (H1 _ t2), (H1 _ t2');
    apply derive_derive_r; assumption.
  Qed.

  Lemma step_derive_trans :
    ∀ t1 t2 t3,
      step t1 t2 →
      derive t2 t3 →
      derive t1 t3.
  Proof.
    intros × H1 H2; generalize dependent t1.
    induction H2 as [t4|t4 t5 t6 H1 IH H2]; intros t1 H3.
    -
      apply derive_step; assumption.
    -
      eauto using derive.
  Qed.

  Lemma derive_multi :
    ∀ t1 t2 t3,
      derive t1 t2 →
      derive t2 t3 →
      derive t1 t3.
  Proof.
    induction 1 as [t4|t4 t5 t6 H1 IH H2].
    -
      trivial.
    -
      eauto using step_derive_trans.
  Qed.

We need a term representing the start variable.

Definition start : term := (inl S ) :: nil.

A term is derivable, if it can be derived by starting with the start variable.

Definition derivable : term → Prop := fun t ⇒ derive start t.

We want to formalise the language produced by a grammar.

  Definition L_G_Pred := fun w ⇒ derivable (convert w).
  #[export] Instance L_G : Language Sigma.
  Proof.
    split.
    -
      exact L_G_Pred.
    -
      destruct G as [? ? ? Sigma_fin].
      exact Sigma_fin.
  Defined.

A grammar G produces a Languages L, iff L_G = L

Definition grammar_produces `(L : Language Sigma) := language_equiv L L_G.
End gramm.