Require Import List.
Import ListNotations.

Require Import Undecidability.CFG.CFP.
Require Import Undecidability.CFG.CFG.
Require Import Undecidability.CFG.Util.Facts.

Require Import Undecidability.PCP.PCP.
Require Import Undecidability.PCP.Util.Facts.
Require Import Undecidability.PCP.Util.PCP_facts.

Require Import Undecidability.Shared.ListAutomation.
Require Import Undecidability.Synthetic.Definitions.

Require Import Setoid Morphisms Arith Lia.

Set Default Proof Using "Type".

Hint Rewrite concat_app map_app map_map : list.
Hint Rewrite map_rev : list.

Lemma nil_app_nil {X} (A : list X) :
  A = [] A [].
Proof.
  now autorewrite with list.
Qed.


Definition (A : stack ) := map ( '(x,y) (x, rev y)) A.

Lemma sigma_eq s A :
   s A = A [s] rev ( ( A)).
Proof.
  induction A as [ | [u v] ].
  - reflexivity.
  - cbn. rewrite IHA. now simpl_list.
Qed.


Lemma tau2_gamma s A :
  s rev ( ( A)) s A.
Proof.
  induction A as [ | [u v] ]; cbn.
  - reflexivity.
  - simpl_list. rewrite !in_app_iff, IHA. firstorder.
Qed.


Lemma sigma_inv A s1 s x y :
   A = x [s] y s x s y s sym A
   = s.
Proof.
  rewrite sigma_eq. intros.
  cbn in H. assert (s A :: rev ( ( A))) by (rewrite H; eauto).
  eapply in_app_iff in as [ | [ | ? % tau2_gamma]]; try firstorder using tau1_sym, tau2_sym.
Qed.


Lemma sigma_snoc A (x y u v: list sig) (s s': sig) :
   s A = x [s] y s x s y
   s' (A [(u, v)]) = x u s' v y.
Proof.
  rewrite !sigma_eq. unfold . cbn. simpl_list. cbn. simpl_list. cbn.
  intros. eapply list_prefix_inv in H as [ ]; eauto.
  eapply notInZero.
  eapply (f_equal ( a count a s)) in H. rewrite !countSplit in H. cbn in H.
  rewrite !Nat.eqb_refl in H. eapply notInZero in . eapply notInZero in .
  rewrite , in *. .
Qed.


Section CFGs.

  Lemma rewrite_sing R a x :
    (a, x) rules R rew_cfg R [a] x.
  Proof.
    intro. rewrite nil_app_nil, (nil_app_nil [a]). now econstructor.
  Qed.


  Global Instance rewtTrans R :
    PreOrder (rewt R).
  Proof.
    split.
    - hnf. econstructor.
    - induction 2; eauto.
  Qed.


  Global Instance rewrite_proper R :
    Proper (rewt R rewt R rewt R) (@app sig).
  Proof.
    intros .
    induction .
    - induction .
      + reflexivity.
      + rewrite IHrewt. inv H. eapply rewtRule.
        replace ( x [a] ) with ( ( x) [a] ) by now autorewrite with list.
        eauto. replace ( x v ) with ( ( x) v ) by now autorewrite with list. eauto.
    - rewrite IHrewt. inv H. autorewrite with list. eauto.
  Qed.


  Global Instance subrel R :
    subrelation (rew_cfg R) (rewt R).
  Proof.
    intros x y H. econstructor. reflexivity. eassumption.
  Qed.


  Lemma terminal_iff G x :
    terminal G x s y, s x (s, y) rules G.
  Proof.
    split.
    - intros H s y A B. apply H. destruct (@in_split _ _ _ A) as ( & & ).
      exists ( y ). change (s :: ) with ([s] ). now econstructor.
    - intros [y ]. inv . eapply ( _ v); eauto.
  Qed.


  Definition sym_G (G : cfg) :=
    startsym G :: flat_map ( '(a, x) a :: x) (rules G).

  Lemma sym_G_rewt x G y :
    x sym_G G rewt G x y y sym_G G.
  Proof.
    intros. induction .
    - eauto.
    - destruct . destruct R. cbn in *.
      pose (app_incl_l IHrewt).
      eapply incl_app. eapply app_incl_l. eassumption.
      eapply incl_app.
      + unfold sym_G. intros ? ?.
        right. eapply in_flat_map. exists (a, v). eauto.
      + eapply cons_incl. eapply app_incl_R. eassumption.
  Qed.


End CFGs.

Section Post_CFG.

  Variable R : stack .
  Variable a : .

  Definition := sym R [a].
  Definition S : := fresh .

  Definition G := (S, (S,[S]) :: map ( '(u, v) (S, u [S] v)) R map ( '(u, v) (S, u [a] v)) R).

  Lemma terminal_iff_G y :
    terminal G y S y.
  Proof.
    unfold terminal.
    enough (( y0, rew_cfg G y ) S y). firstorder. split.
    - intros [ ?]. inv H. cbn in .
      destruct as [ | [ [[] []] % in_map_iff | [[] []] % in_map_iff ] % in_app_iff]; inv H; eauto.
    - intros (u' & v' & ?) % List.in_split.
      subst. exists (u' [S] v'). econstructor. cbn. eauto.
  Qed.


  Lemma rewt_count x :
    rewt G [S] x count x S 1.
  Proof.
    induction 1.
    - cbn. now rewrite Nat.eqb_refl.
    - inv . destruct as [ | [ [[] []] % in_map_iff | [[] []] % in_map_iff ] % in_app_iff]; inv .
      + eauto.
      + unfold . simpl_list. rewrite !countSplit in *. cbn in *.
        rewrite Nat.eqb_refl in *.
        enough (count l S = 0) as . enough (count S = 0) as . .
        * eapply notInZero. intros D.
          edestruct (fresh_spec) with (l := ); try reflexivity.
          eapply sym_word_R in . unfold . eauto.
        * eapply notInZero. intros D.
          edestruct (fresh_spec) with (l := ); try reflexivity.
          eapply sym_word_l in . unfold . eauto.
      + unfold . simpl_list. rewrite !countSplit in *. cbn in *.
        rewrite Nat.eqb_refl in *.
        assert (S =? a = false) as . eapply Nat.eqb_neq. intros D.
        edestruct fresh_spec with (l := ); try reflexivity.
        unfold S in *. rewrite D. unfold ; eauto.
        enough (count l S = 0) as . enough (count S = 0) as . .
        * eapply notInZero. intros D.
          edestruct (fresh_spec) with (l := ); try reflexivity.
          eapply sym_word_R in . unfold . eauto.
        * eapply notInZero. intros D.
          edestruct (fresh_spec) with (l := ); try reflexivity.
          eapply sym_word_l in . unfold . eauto.
  Qed.


  Lemma Post_CFG_1' A :
    A R A = [] rewt G [S] ( a A).
  Proof.
    induction A.
    - cbn. eauto.
    - intros. assert (A R) by eauto. eapply IHA in .
      destruct as [u v]. destruct .
      + subst. right. erewrite rewrite_sing with (x := u [a] v). reflexivity.
        right. eapply in_app_iff. right. eapply in_map_iff. exists (u,v); eauto.
      + right. erewrite rewrite_sing with (x := u [S] v).
        now rewrite . right. eapply in_app_iff. left. eapply in_map_iff. exists (u,v); eauto.
  Qed.


  Lemma Post_CFG_2 x :
    rewt G [S] x
     A m, A R m A = x (m = S m = a A []).
  Proof.
    intros. induction H.
    - cbn. exists [], S. eauto.
    - inv . destruct as [ | [(? & ? & ?) % in_map_iff | (? & ? & ?) % in_map_iff] % in_app_iff]; inv .
      + eassumption.
      + destruct as [u' v']. inv .
        destruct IHrewt as (A & m & HA & IHA & Hm).
        exists (A [(u', v')]), S. repeat split.
        * eauto.
        * simpl_list. cbn.
          enough ( S x). enough ( S ).
          eapply sigma_snoc with (s := S); eauto.
          -- assert ( := IHA).
          eapply sigma_inv in IHA; eauto. subst. eauto.
          intros D.
          edestruct fresh_spec with (l := sym R [a]); try reflexivity.
          eapply in_app_iff. left. eapply sym_mono. eauto. eauto.
          -- eapply rewt_count in H. rewrite !countSplit in H. cbn in H.
             rewrite Nat.eqb_refl in H. eapply notInZero. .
          -- eapply rewt_count in H. rewrite !countSplit in H. cbn in H.
             rewrite Nat.eqb_refl in H. eapply notInZero. .
        * eauto.
      + destruct as [u' v']. inv .
        destruct IHrewt as (A & m & HA & IHA & Hm).
        exists (A [(u', v')]), a. repeat split.
        * eauto.
        * simpl_list. cbn.
          enough ( S x). enough ( S ).
          eapply sigma_snoc with (s := S); eauto.
          -- assert ( := IHA).
          eapply sigma_inv in IHA; eauto. subst. eauto.
          intros D.
          edestruct fresh_spec with (l := sym R [a]); try reflexivity.
          eapply in_app_iff. left. eapply sym_mono. eauto. eauto.
          -- eapply rewt_count in H. rewrite !countSplit in H. cbn in H.
             rewrite Nat.eqb_refl in H. eapply notInZero. .
          -- eapply rewt_count in H. rewrite !countSplit in H. cbn in H.
             rewrite Nat.eqb_refl in H. eapply notInZero. .
        * destruct A; cbn; firstorder congruence.
  Qed.


  Lemma reduction_full x :
    ( A, A R A [] a A = x) L G x.
  Proof.
    split.
    - intros (A & ? & ? & ?). subst. destruct Post_CFG_1' with (A := A); intuition.
      split.
      + eassumption.
      + eapply terminal_iff_G. rewrite sigma_eq. intros E.
        edestruct fresh_spec with (l := sym R [a]); try reflexivity.
        eapply in_app_iff in E as [ | [ | ? % tau2_gamma ] % in_app_iff].
        * eapply in_app_iff. left. eapply sym_mono; eauto. now eapply tau1_sym.
        * eapply in_app_iff. right. eauto.
        * eapply in_app_iff. left. eapply sym_mono; eauto. now eapply tau2_sym.
    - intros [(A & m & HA & HE & Hm) % Post_CFG_2 ?].
      subst. destruct Hm as [ | [ ?]].
      + eapply terminal_iff_G in H. exfalso. rewrite sigma_eq in H.
        eapply H. eauto.
      + exists A. eauto.
  Qed.


End Post_CFG.

Theorem reduction :
  CFPP CFP.
Proof.
  exists ( '(R, a) (G R a)). intros [R a].
  intuition; cbn in *.
  - destruct H as (A & HR & HA & H).
    exists ( a A). split. eapply reduction_full; eauto.
    eauto.
  - destruct H as (x & Hx & H).
    eapply reduction_full in Hx as (A & HR & HA & ).
    exists A. subst; eauto.
Qed.