Require Import List.
Import ListNotations.

Require Import Undecidability.CFG.CFP.
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 Arith Lia.

Set Default Proof Using "Type".

(* * PCP to CFPP *)
Section PCP_CFPP.

  Variable P : stack .

  Definition := sym P.
  Notation "#" := (fresh ).

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

  Lemma sigma_gamma a A :
     a ( A) = A a rev ( A).
  Proof.
    induction A as [ | (x & y) ]; unfold in *; cbn.
    - reflexivity.
    - rewrite IHA. now simpl_list.
  Qed.


  Definition palin {X} (A : list X) := A = rev A.

  Lemma tau_eq_iff A a :
     a sym A
     A = A palin ( a ( A)).
  Proof.
    rewrite sigma_gamma. unfold palin.
    simpl_list. intuition.
    - now rewrite .
    - eapply list_prefix_inv in ; firstorder using tau1_sym, tau2_sym.
  Qed.


  Lemma gamma_invol A :
     ( A) = A.
  Proof.
    induction A as [ | (x,y) ]; cbn.
    - reflexivity.
    - simpl_list. now rewrite IHA at 2.
  Qed.


  Lemma gamma_mono A B :
    A B A B.
  Proof.
    induction A as [ | (x,y) ]; cbn; intros.
    - firstorder.
    - intros ? [ | ].
      + assert ( (x, y) B) by firstorder.
        unfold in . eapply in_map_iff in as ((x',y') & ? & ?).
        inv . now simpl_list.
      + firstorder.
  Qed.


End PCP_CFPP.

Theorem reduction :
  PCP CFPP.
Proof.
  exists ( P ( P, fresh (sym P))).
  intros P. split; intros.
  - destruct H as (A & Hi & He & H).
    exists ( A). repeat split.
    + eapply gamma_mono. now rewrite gamma_invol.
    + destruct A; cbn in *; congruence.
    + eapply tau_eq_iff. intros F % (sym_mono (P := P)) % fresh_spec; now try eapply F. eauto.
  - destruct H as (B & Hi & He & H).
    exists ( B). repeat split.
    + now eapply gamma_mono.
    + destruct B; cbn in *; congruence.
    + eapply tau_eq_iff with (a := fresh (sym P)).
      * intros F % (sym_mono (P := P)) % fresh_spec. now eapply F. now eapply gamma_mono.
      * rewrite gamma_invol. eassumption.
Qed.