File CoMoLang.L_TnFn

Require Import List.
From CoMoLang Require Import Languages Grammars CFG.

Now, we have a look at a language, where all words look like a^n b^n. We use an alphabet, which only contains a and b (encoded as boolean values true and false). We will see, that this language is contextfree.
Definition TnFn := fun w ⇒ ∃ n, w = (repeat true n) ++ repeat false n.
#[export,refine] Instance L_TnFn : Language bool := { Pred := TnFn }.
Proof.
  ∃ (true :: false :: nil).
  intros []; firstorder.
Defined.

Next step: Create a grammar, which produces L_TnFn.
Inductive R_TnFn : let term := list (sum unit bool) in term → term → Prop :=
  
First rule: tt -> true tt false
  | R_TnFn_1 : R_TnFn ((inl tt) :: nil) ((inr true) :: (inl tt) :: (inr false) :: nil)
  
Second rule: tt -> nil
  | R_TnFn_2 : R_TnFn ((inl tt) :: nil) nil
      .

Note the use of inl (for variables) and inr (and letters) in the above grammar. As we only need one variable for this grammar, we used unit type for encoding and bool for the letters.
One could rewrite this grammar in a more human readable way: S -> aSb | nil

#[export,refine] Instance G_TnFn : Grammar unit bool := {rule := R_TnFn; S := tt}.
Proof.
  -
    ∃ (tt :: nil); intros []; firstorder.
  -
    ∃ (true :: false :: nil); intros []; firstorder.
Defined.

G_TnFn is obviously a contextfree grammar, so we proof it.
#[export,refine] Instance G_TnFn_cfg : CFG unit bool := { CFG_Grammar := G_TnFn }.
Proof.
  destruct 1; eexists; reflexivity.
Defined.

Here is one example for computing a derivation of the word "true false".
Example bsp_TnFn_1 : derivable G_TnFn ((inr true) :: (inr false) :: nil).
Proof.
  red.
  apply dtrans with (t2 := ((inr true) :: nil) ++ ((inl tt) :: nil) ++ ((inr false) :: nil)).

  apply derive_step.
  apply step_rule.
  constructor.

  assert (H1 : inr unit true :: inr false :: nil = (inr true :: nil) ++ nil ++ (inr false :: nil)).
  reflexivity.
  rewrite H1.
  constructor.
  constructor.
Qed.

Print bsp_TnFn_1.

The actual equivalence proof needs a helper lemma, which states, what it means for a term to be derivable by R_TnFn.
Lemma w_charac :
  ∀ (w : list (sum unit bool)),
    derivable G_TnFn w →
    
Form 1: w = true^n tt false^n
    (∃ n,
      w = (repeat (inr true) n) ++ (inl tt :: nil) ++ (repeat (inr false) n)) ∨
    
Form 2: w = true^n false^n
    ∃ n,
      w = (repeat (inr true) n) ++ (repeat (inr false) n).
Proof.
  intros w w_Derivable.

  red in w_Derivable.
  remember (start G_TnFn) as t1 eqn:H2.

  Print derive.
  induction w_Derivable as [t3|t3 t4 t5 H_Multi IH H_Step].
  -
IA
    subst;
    left;
    ∃ 0;
    reflexivity.
  -
IS
    subst.
    specialize (IH (eq_refl _)).
    destruct IH as [[n IH]|[n IH]].
Case analysis: w could be of form 1 or form 2.
    +
Case 1: w = true^n tt false^n
      Print step.
      destruct H_Step as [t6 t7 t7' t8 H6].
Now, we can analyse, which rules could be applied.
      destruct H6.
      ×
tt -> true tt false
        left.
w' will be of form 1.
        ∃ (Datatypes.S n).

        clear H_Multi.

Now, the proof is just about list properties.
        apply app_eq_app in IH as [l1 [[H7 H8]|[H7 H8]]];
            apply app_eq_app in H8 as [l2 [[H9 HA]|[H9 HA]]]; subst.
        --
           symmetry in H9.
           apply app_eq_unit in H9 as [[HB HC]|[HB HC]]; subst.
           ++
              injection HA; intros HD; subst; cbn.
              clear HA.
              remember (inl tt :: inr false :: repeat (inr false) n) as r eqn:H1.
              assert (H2 : inr true :: r = (inr true :: nil) ++ r). reflexivity.
              rewrite H2.
              rewrite app_comm_cons.
              rewrite app_assoc.
              f_equal.
              clear H1 H2 r.
              symmetry.
              rewrite repeat_cons.
              rewrite app_nil_r.
              reflexivity.
           ++
              cbn in HA.
              induction n; discriminate.
        --
           exfalso.
           generalize dependent t8;
           generalize dependent l2;
           induction n as [|n IH];
               intros [|h1 t1] [|h2 t2] H1;
                   try discriminate;
                   injection H1;
                   intros H2 H3;
                   eapply IH;
                   rewrite H2;
                   reflexivity.
        --
           symmetry in H9.
           apply app_eq_unit in H9 as [[HB HC]|[HB HC]]; subst.
           ++
              rewrite app_nil_r in H7; subst.
              injection HA; intros HD; subst; cbn.
              clear HA.
              remember (inl tt :: inr false :: repeat (inr false) n) as r eqn:H1.
              assert (H2 : inr true :: r = (inr true :: nil) ++ r). reflexivity.
              rewrite H2.
              rewrite app_comm_cons.
              rewrite app_assoc.
              f_equal.
              clear H1 H2 r.
              symmetry.
              rewrite repeat_cons.
              reflexivity.
           ++
              cbn in HA; subst.
              exfalso.

              generalize dependent t6.
              induction n as [|n IH]; intros [|h t] H1; try discriminate.
              injection H1; intros H2 H3; subst; clear H1.
              eapply IH; rewrite H2; reflexivity.
        --
           exfalso.
           generalize dependent l2;
           generalize dependent t6;
           induction n as [|n IH];
           intros [|h1 t1] [|h2 t2] H1;
           try easy;
           injection H1;
           intros H2 H3;
           subst;
           clear H1;
           eapply IH;
           rewrite H2;
           reflexivity.

      ×
tt -> true false
        right.
w' will be of form 2.
        ∃ n.
        clear H_Multi.

The rest of this proof is just about list properties.
        apply app_eq_app in IH as [l1 [[H1 H2]|[H1 H2]]]; subst.
        --
           apply app_eq_app in H2 as [l2 [[H3 H4]|[H3 H4]]]; subst.
           ++
              symmetry in H3;
              apply app_eq_unit in H3 as [[H5 H6]|[H5 H6]]; subst.
              **
                 injection H4; intros H7; subst;
                 rewrite app_nil_r,app_nil_l; reflexivity.
              **
                 exfalso.
                 cbn in H4.
                 generalize dependent t8;
                 induction n; discriminate.
           ++
              exfalso;
              generalize dependent t8;
              generalize dependent l2;
              induction n as [|n IH]; intros [|h1 t1] [|h2 t2] H1; try discriminate;
                  injection H1; intros H2 H3; subst; eapply IH; rewrite H2; reflexivity.
        --
           apply app_eq_app in H2 as [l2 [[H3 H4]|[H3 H4]]]; subst.
           ++
              symmetry in H3;
              apply app_eq_unit in H3 as [[H5 H6]|[H5 H6]]; subst.
              **
                 injection H4; intros H7; cbn in *; rewrite app_nil_r in *; subst; reflexivity.
              **
                 exfalso.
                 apply app_eq_app in H4 as [l3 [[H8 H9]|[H8 H9]]]; cbn in H8; subst.
                 ---
                     generalize dependent t6;
                     induction n as [|n IH]; intros [|h6 t6] HB; try discriminate; eapply IH; injection HB; intros H2; rewrite H2; reflexivity.
                 ---
                     discriminate.
           ++
              exfalso;
              generalize dependent t6;
              generalize dependent l2;
              induction n as [|n IH];
              intros [|h1 t1] [|h2 t2] H1;
                  try discriminate;
                  eapply IH;
                  injection H1; intros H2; rewrite H2; reflexivity.

    +
Case 2: w = true^n false^n
      clear H_Multi.

Because there are no variables in w, we get a contradiction in H_Step.
      exfalso.

      destruct H_Step as [t1 t2 t2' t3 H_Rule]; subst.

First, we characterize the left side of all rules.
      assert (H7 : t2 = (inl tt :: nil)). { destruct H_Rule; reflexivity. }
      clear H_Rule t2'.
      subst.

      assert (H8 : ¬ just_chars (t1 ++ (inl tt :: nil) ++ t3)).
      {
        intros H9;
        apply app_just_chars in H9 as [H9 HA];
        apply app_just_chars in HA as [];
        contradiction.
      }

      apply H8; rewrite IH; apply app_just_chars.
      clear t1 t3 IH H8.
      split; induction n; easy.
Qed.

Now we can prove the actual equivalence.
Theorem L_equiv_G : grammar_produces G_TnFn L_TnFn.
Proof.
  split.
Two directions need to be proven: L_TnFn ~> L(G_TnFn) und L(G_TnFn) ~> L_TnFn.
  -
L_TnFn ~> L(G_TnFn)
    intros [n *]; subst.
    induction n as [|n IH].
    +
      apply derive_step;
      apply step_rule;
      constructor.
    +
      eapply derive_multi.

      apply derive_step;
      apply step_rule;
      exact R_TnFn_1.

      cbn in ×.

Rewriting of lists
      assert (H1 : inr true :: inl tt :: inr false :: nil = (inr true :: nil) ++ (inl tt :: nil) ++ inr false :: nil). reflexivity.
      rewrite H1; clear H1.

      assert (H2 : (inr true :: map (fun x : bool ⇒ inr x) (repeat true n ++ false :: repeat false n)) = (inr true :: nil) ++ (convert unit (repeat true n ++ repeat false n)) ++ (inr false :: nil)).
      {
        cbn.
        f_equal.
        rewrite repeat_cons.
        unfold convert.
        do 3 rewrite map_app.
        rewrite app_assoc.
        reflexivity.
        }
      rewrite H2; clear H2.

      apply derive_derive.
      exact IH.
  -
L(G_TnFn) ~> L_TnFn
    intros H1.

    repeat red;
    repeat red in H1.

Case analysis based on w, using our helper lemma w_charac.
    destruct (w_charac (convert unit w) H1) as [[n H2]|[n H2]].
    +
w has form 1: contradiction, because w cannot contain variables.
      exfalso.

      remember (convert unit w) as t1 eqn:H3;
      remember (repeat (inr true) n ++ (inl tt :: nil) ++ repeat (inr false) n) as t2 eqn:H4.
      assert (H5 : ¬ just_chars t2).
      {
        subst; intros H6;
        apply app_just_chars in H6 as [H6 H7];
        apply app_just_chars in H7 as [H7 H8];
        contradiction.
        }

      apply H5.
      rewrite <- H2.
      subst.
      apply convert_just_chars.
    +
w has form 2: That's possible, so we know how w looks like.
      ∃ n.
      eapply convert_inj.
      rewrite H2.
      unfold convert.
      rewrite map_app.
      clear w H1 H2.
      assert (H1 : ∀ A (f : bool → A) (b : bool), repeat (f b) n = map f (repeat b n)).
      {
        induction n as [|n IH].
        -
          easy.
        -
          intros.
          cbn.
          rewrite IH.
          reflexivity.
        }
      f_equal; apply H1.
Qed.

Now we are in a position to prove, that L_TnFn is indeed contextfree.
Corollary L_TnFn_cfg : is_cf L_TnFn.
Proof.
  do 2 eexists;
  exact L_equiv_G.
Qed.