Require Import PCP.Definitions Post_CFG.

(** * CFP to CFI *)

Section Palindrome.

  Variable Sigma : list symbol.

  Notation StartG := (fresh Sigma).
  
  Definition palin_G : cfg :=
    (StartG, (StartG, []) ::
                          flat_map (fun g => [ (StartG, [g]);  (StartG, [g; StartG; g]) ]) Sigma).

  Lemma notInZero  (x: nat) A :
    not (x el A) <-> count A x = 0.
  Proof.
(* Goal: iff (not (@In nat x A)) (@eq nat (count A x) O) *)
    split; induction A.
    -  reflexivity.
    - intros H. cbn in *. destruct (Nat.eqb_spec x a).
(* Goal: and (@eq (list nat) (@rev nat z) z) (le (count z (fresh Sigma)) (Datatypes.S O)) *)
      + exfalso. apply H. left. congruence.
(* Goal: and (@eq (list nat) (@rev nat z) z) (le (count z (fresh Sigma)) (Datatypes.S O)) *)
      + apply IHA. intros F. apply H. now right.
    - tauto.
    - cbn. destruct (Nat.eqb_spec x a).
(* Goal: and (@eq (list nat) (@rev nat z) z) (le (count z (fresh Sigma)) (Datatypes.S O)) *)
      + subst a. omega.
(* Goal: and (@eq (list nat) (@rev nat z) z) (le (count z (fresh Sigma)) (Datatypes.S O)) *)
      + intros H [E | E].
        * now symmetry in E.
(* Goal: False *)
        * tauto.
  Qed.

  Lemma G_left x : 
    rewt palin_G [StartG] x -> rev x = x /\ count x StartG <= 1.
  Proof.
(* Goal: forall _ : rewt palin_G (@cons nat (fresh Sigma) (@nil nat)) x, and (@eq (list nat) (@rev nat x) x) (le (count x (fresh Sigma)) (Datatypes.S O)) *)
    induction 1.
    - cbn. rewrite (Nat.eqb_refl StartG). intuition.
    - destruct IHrewt as [IH Eq].
(* Goal: and (@eq (list nat) (@rev nat z) z) (le (count z (fresh Sigma)) (Datatypes.S O)) *)
      + inv H0. cbn in H1. destruct H1.
        * inv H0. rewrite <- !countSplit in *. autorewrite with list in *. cbn in *. split; try omega.
          rewrite Nat.eqb_refl in *.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
          assert (count x StartG = 0) as H1 % notInZero by omega.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
          assert (count y0 StartG = 0) as H2 % notInZero by omega.
          eapply list_prefix_inv in IH as [<- _]; try rewrite <- in_rev; eauto.
(* Goal: @eq (list nat) (@app nat (@rev nat y0) (@cons nat x0 (@cons nat (fresh Sigma) (@cons nat x0 (@rev nat (@rev nat y0)))))) (@app nat (@rev nat y0) (@cons nat x0 (@cons nat (fresh Sigma) (@cons nat x0 y0)))) *)
(* Goal: le (Init.Nat.add (count x (fresh Sigma)) (Init.Nat.add (if Nat.eqb (fresh Sigma) x0 then Datatypes.S (Datatypes.S (if Nat.eqb (fresh Sigma) x0 then Datatypes.S O else O)) else Datatypes.S (if Nat.eqb (fresh Sigma) x0 then Datatypes.S O else O)) (count y0 (fresh Sigma)))) (Datatypes.S O) *)
          now rewrite rev_involutive.
        * eapply in_flat_map in H0 as (? & ? & [ | [ | [] ]]).
          -- inv H1. rewrite <- !countSplit in *. autorewrite with list in *. cbn in *. 
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
             rewrite Nat.eqb_refl in *. split; try omega.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
             assert (count x StartG = 0) as H1 % notInZero by omega.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
             assert (count y0 StartG = 0) as H2 % notInZero by omega.
             eapply list_prefix_inv in IH as [ <- _]; try rewrite <- in_rev; eauto.
(* Goal: @eq (list nat) (@app nat (@rev nat y0) (@cons nat x0 (@cons nat (fresh Sigma) (@cons nat x0 (@rev nat (@rev nat y0)))))) (@app nat (@rev nat y0) (@cons nat x0 (@cons nat (fresh Sigma) (@cons nat x0 y0)))) *)
(* Goal: le (Init.Nat.add (count x (fresh Sigma)) (Init.Nat.add (if Nat.eqb (fresh Sigma) x0 then Datatypes.S (Datatypes.S (if Nat.eqb (fresh Sigma) x0 then Datatypes.S O else O)) else Datatypes.S (if Nat.eqb (fresh Sigma) x0 then Datatypes.S O else O)) (count y0 (fresh Sigma)))) (Datatypes.S O) *)
             now rewrite rev_involutive.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
             destruct _; omega. 
          -- inv H1. rewrite <- !countSplit in *. autorewrite with list in *. cbn in *.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
             rewrite Nat.eqb_refl in *. split; try omega.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
             assert (count x StartG = 0) as H1 % notInZero by omega.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
             assert (count y0 StartG = 0) as H2 % notInZero by omega.
             eapply list_prefix_inv in IH as [<- _]; try rewrite <- in_rev; eauto.
(* Goal: @eq (list nat) (@app nat (@rev nat y0) (@cons nat x0 (@cons nat (fresh Sigma) (@cons nat x0 (@rev nat (@rev nat y0)))))) (@app nat (@rev nat y0) (@cons nat x0 (@cons nat (fresh Sigma) (@cons nat x0 y0)))) *)
(* Goal: le (Init.Nat.add (count x (fresh Sigma)) (Init.Nat.add (if Nat.eqb (fresh Sigma) x0 then Datatypes.S (Datatypes.S (if Nat.eqb (fresh Sigma) x0 then Datatypes.S O else O)) else Datatypes.S (if Nat.eqb (fresh Sigma) x0 then Datatypes.S O else O)) (count y0 (fresh Sigma)))) (Datatypes.S O) *)
             now rewrite rev_involutive.
(* Goal: le (Init.Nat.add (count x (fresh Sigma)) (Init.Nat.add (if Nat.eqb (fresh Sigma) x0 then Datatypes.S (Datatypes.S (if Nat.eqb (fresh Sigma) x0 then Datatypes.S O else O)) else Datatypes.S (if Nat.eqb (fresh Sigma) x0 then Datatypes.S O else O)) (count y0 (fresh Sigma)))) (Datatypes.S O) *)
             destruct (Nat.eqb_spec StartG x0). subst. edestruct fresh_spec; eauto.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
             omega.
  Qed.

  Lemma listI : forall (A : Type) (P : list A -> Prop), P [] -> (forall x, P [x]) -> (forall (x : A) (y : A) (l : list A), P l -> P (x :: l ++ [y])) -> forall l : list A, P l.
  Proof.
(* Goal: forall (x : A) (l : list A) (_ : forall _ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a l))), P y, P (@cons A a l)) (_ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a (@app A l (@cons A x (@nil A)))))), P y), P (@cons A a (@app A l (@cons A x (@nil A)))) *)
    intros. pattern l. revert l. apply size_induction with (f := @length _). intros.
(* Goal: P x *)
    destruct x.
    - auto.
    - revert H2. pattern x. revert x. apply rev_ind. auto.
(* Goal: lt (@length A l) (@length A (@cons A a (@app A l (@cons A x (@nil A))))) *)
      intros. apply H1. apply H3. cbn. rewrite app_length. omega.
  Qed.

  Lemma rev_palin x : x <<= StartG :: Sigma ->
    x = rev x -> count x StartG <= 1 -> rewt palin_G [StartG] x.
  Proof.
(* Goal: forall (x : A) (l : list A) (_ : forall _ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a l))), P y, P (@cons A a l)) (_ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a (@app A l (@cons A x (@nil A)))))), P y), P (@cons A a (@app A l (@cons A x (@nil A)))) *)
    pattern x. revert x. apply listI; intros.
    - rewrite rewrite_sing. reflexivity. now left.
    - destruct (Nat.eqb_spec x StartG).
(* Goal: forall _ : not (@In nat x (@nil nat)), @eq nat (count (@nil nat) x) O *)
      subst. reflexivity. rewrite rewrite_sing. reflexivity. right. eapply in_flat_map.
(* Goal: @eq nat a x *)
      exists x. split. assert (x el StartG :: Sigma) by firstorder. destruct H2; eauto. congruence.
(* Goal: or (@eq nat a x) (@In nat x A) *)
      now left.
    - cbn in H1. autorewrite with  list in *. inv H1.
      cbn in H2. rewrite <- countSplit in H2.
(* Goal: le (Init.Nat.add (count x (fresh Sigma)) (Init.Nat.add (Datatypes.S (Datatypes.S (Datatypes.S O))) (count y0 (fresh Sigma)))) (Datatypes.S O) *)
(* Goal: le (Init.Nat.add (count x (fresh Sigma)) (Init.Nat.add (Datatypes.S O) (count y0 (fresh Sigma)))) (Datatypes.S O) *)
      destruct (Nat.eqb_spec StartG y); subst.
(* Goal: and (@eq (list nat) (@app nat (@rev nat y0) (@app nat (@rev nat (@cons nat x0 (@cons nat (fresh Sigma) (@cons nat x0 (@nil nat))))) (@rev nat x))) (@app nat x (@app nat (@cons nat x0 (@cons nat (fresh Sigma) (@cons nat x0 (@nil nat)))) y0))) (le (Init.Nat.add (count x (fresh Sigma)) (Init.Nat.add (count (@cons nat x0 (@cons nat (fresh Sigma) (@cons nat x0 (@nil nat)))) (fresh Sigma)) (count y0 (fresh Sigma)))) (Datatypes.S O)) *)
      + cbn in *. rewrite (Nat.eqb_refl) in *. omega.
(* Goal: and (@eq (list nat) (@rev nat z) z) (le (count z (fresh Sigma)) (Datatypes.S O)) *)
      + rewrite rewrite_sing with (x := [y] ++ [StartG] ++ [y]).
        rewrite H.
(* Goal: forall _ : not (@In nat x (@nil nat)), @eq nat (count (@nil nat) x) O *)
        * cbn. reflexivity.
        * eauto.
        * now eapply app_inv_tail in H5.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
        * cbn in *; omega.
(* Goal: lt (@length A l) (@length A (@cons A a (@app A l (@cons A x (@nil A))))) *)
        * right. eapply in_flat_map. cbn. firstorder.
  Qed.

  Lemma Start_fresh x :
    x <<= Sigma -> ~ StartG el x.
  Proof.
(* Goal: forall _ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a (@nil A)))), P y, P (@cons A a (@nil A)) *)
(* Goal: forall (x : A) (l : list A) (_ : forall _ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a l))), P y, P (@cons A a l)) (_ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a (@app A l (@cons A x (@nil A)))))), P y), P (@cons A a (@app A l (@cons A x (@nil A)))) *)
    intros ? ?. edestruct fresh_spec with (l := Sigma); eauto.
  Qed.
  
  Lemma G_char x : x <<= Sigma ->
    x = rev x <-> L palin_G x.
  Proof.
    intros Hx. split.
    - intros H. split.
(* Goal: and (@eq (list nat) (@rev nat z) z) (le (count z (fresh Sigma)) (Datatypes.S O)) *)
      + eapply rev_palin in H; eauto.
(* Goal: lt (@length A l) (Datatypes.S (Init.Nat.add (@length A l) (@length A (@cons A x (@nil A))))) *)
        enough (count x StartG = 0) by omega.
        eapply notInZero. eauto using Start_fresh.
(* Goal: and (@eq (list nat) (@rev nat z) z) (le (count z (fresh Sigma)) (Datatypes.S O)) *)
      + intros [y Hy].
(* Goal: and (@eq (list nat) (@rev nat (@app nat x (@app nat v y0))) (@app nat x (@app nat v y0))) (le (count (@app nat x (@app nat v y0)) (fresh Sigma)) (Datatypes.S O)) *)
        inv Hy. destruct H0. inv H0.
(* Goal: forall _ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a (@nil A)))), P y, P (@cons A a (@nil A)) *)
(* Goal: forall (x : A) (l : list A) (_ : forall _ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a l))), P y, P (@cons A a l)) (_ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a (@app A l (@cons A x (@nil A)))))), P y), P (@cons A a (@app A l (@cons A x (@nil A)))) *)
        eapply Start_fresh. eauto. eauto. 
(* Goal: and (@eq (list nat) (@rev nat (@app nat x (@app nat v y0))) (@app nat x (@app nat v y0))) (le (count (@app nat x (@app nat v y0)) (fresh Sigma)) (Datatypes.S O)) *)
        eapply in_flat_map in H0 as (? & ? & [ | [ | [] ]]).
(* Goal: lt (@length A l) (@length A (@cons A a (@app A l (@cons A x (@nil A))))) *)
        * inv H1. eapply Start_fresh. eauto. rewrite H. simpl_list. cbn. eauto. 
(* Goal: lt (@length A l) (@length A (@cons A a (@app A l (@cons A x (@nil A))))) *)
        * inv H1. eapply Start_fresh. eauto. rewrite H. simpl_list. cbn. eauto. 
    - intros [[] % G_left Ht]. eauto.
  Qed.
  
End Palindrome.

Theorem CFP_CFI :
  CFP' ⪯ CFI'.
Proof.
(* Goal: @reduces cfg (prod cfg cfg) CFP' CFI' *)
  exists (fun G => (palin_G (sym_G G), G)). intros G. split; intros (? & ? & ?).
  - exists x. rewrite <- G_char. intuition. destruct H. eapply sym_G_rewt; try eassumption.
(* Goal: forall _ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a (@nil A)))), P y, P (@cons A a (@nil A)) *)
(* Goal: forall (x : A) (l : list A) (_ : forall _ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a l))), P y, P (@cons A a l)) (_ : forall (y : list A) (_ : lt (@length A y) (@length A (@cons A a (@app A l (@cons A x (@nil A)))))), P y), P (@cons A a (@app A l (@cons A x (@nil A)))) *)
    destruct G. unfold sym_G; cbn; eauto.
  - destruct H. eapply G_left in H.
(* Goal: and (L G x) (@eq (list nat) x (@rev nat x)) *)
    exists x. intuition.
Qed.
