Require Import Undecidability.PCP.Definitions.

(** * PCP to CFP *)

Section PCP_CFP.

  Variable P : SRS.

  Definition Sigma := sym P.
  Notation "#" := (fresh Sigma).
  
  Definition gamma (A : SRS) := map (fun '(x,y) => (x, rev y)) A.

  Lemma sigma_gamma a A :
    sigma a (gamma A) = tau1 A ++ a ++ rev (tau2 A).
  Proof.
(* Goal: @eq (list symbol) (sigma a (gamma A)) (@app nat (@tau1 nat A) (@app nat (sing a) (@rev nat (@tau2 nat A)))) *)
    induction A as [ | (x & y) ]; unfold gamma 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 el sym A ->
    tau1 A = tau2 A <-> palin (sigma a (gamma A)).
  Proof.
(* Goal: forall _ : not (@In nat a (sym A)), iff (@eq (PCP.string nat) (@tau1 nat A) (@tau2 nat A)) (@palin symbol (sigma a (gamma A))) *)
    rewrite sigma_gamma. unfold palin.
(* Goal: @eq (list (prod (PCP.string nat) (list nat))) (@cons (prod (PCP.string nat) (list nat)) (@pair (PCP.string nat) (list nat) x (@rev nat (@rev nat y))) (@map (prod (PCP.string nat) (list nat)) (prod (PCP.string nat) (list nat)) (fun '(pair x y) => @pair (PCP.string nat) (list nat) x (@rev nat y)) (@map (prod (PCP.string nat) (list nat)) (prod (PCP.string nat) (list nat)) (fun '(pair x y) => @pair (PCP.string nat) (list nat) x (@rev nat y)) A))) (@cons (PCP.card nat) (@pair (PCP.string nat) (PCP.string nat) x y) A) *)
    simpl_list. intuition.
    - now rewrite H0.
    - eapply list_prefix_inv in H0; firstorder using tau1_sym, tau2_sym.
  Qed.

  Lemma gamma_invol A :
    gamma (gamma A) = A.
  Proof.
(* Goal: @eq (list (prod (PCP.string nat) (list nat))) (gamma (gamma A)) A *)
    induction A as [ | (x,y) ]; cbn.
    - reflexivity.
    - simpl_list. now rewrite <- IHA at 2.
  Qed.

  Lemma gamma_mono A B :
    A <<= gamma B -> gamma A <<= B.
  Proof.
(* Goal: forall _ : @incl (prod (PCP.string nat) (list nat)) A (gamma B), @incl (prod (PCP.string nat) (list nat)) (gamma A) B *)
    induction A as [ | (x,y) ]; cbn; intros.
    - firstorder.
    - intros ? [ <- | ].
(* Goal: @In (prod (PCP.string nat) (list nat)) a B *)
      + assert ( x/y el gamma B) by firstorder.
(* Goal: @In (prod (PCP.string nat) (list nat)) (@pair (PCP.string nat) (list nat) x (@rev nat y)) B *)
        unfold gamma in H0. eapply in_map_iff in H0 as ((x',y') & ? & ?).
(* Goal: @In (prod (PCP.string nat) (list nat)) (@pair (PCP.string nat) (list nat) x (@rev nat (@rev nat y'))) B *)
        inv H0. now simpl_list.
(* Goal: @In (prod (PCP.string nat) (list nat)) a B *)
      + firstorder.
  Qed.

End PCP_CFP.

Theorem PCP_CFP :
  PCP ⪯ CFP.
Proof.
(* Goal: @reduces (list (PCP.card nat)) (prod (list (PCP.card nat)) symbol) PCP CFP *)
  exists (fun P => (gamma P, fresh (sym P))).
(* Goal: forall x : list (PCP.card nat), iff (PCP x) (CFP (@pair (list (prod (PCP.string nat) (list nat))) nat (gamma x) (fresh (sym x)))) *)
  intros P. split; intros.
  - destruct H as (A & Hi & He & H).
(* Goal: CFP (@pair (list (prod (PCP.string nat) (list nat))) nat (gamma P) (fresh (sym P))) *)
    exists (gamma 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).
(* Goal: and (@incl (PCP.card nat) (gamma B) P) (and (not (@eq SRS (gamma B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (gamma B)) (@tau2 nat (gamma B)))) *)
    exists (gamma B). repeat split.
    + now eapply gamma_mono.
    + destruct B; cbn in *; congruence.
    + eapply tau_eq_iff with (a := fresh (sym P)).
(* Goal: @incl (PCP.card nat) (gamma A) (gamma P) *)
      * intros F % (sym_mono (P := P)) % fresh_spec.  now eapply F. now eapply gamma_mono.
      * rewrite gamma_invol. eassumption.
Qed.
                   
      
    
  
