Require Import Undecidability.PCP.Definitions.

(** * SR to MPCP *)

Section SR_to_MPCP.

  Variable R : SRS.
  Variables x0 y0 : string.

  Notation "x ≻ y" := (rew R x y) (at level 70).
  Notation "x ≻* y" := (rewt R x y) (at level 70).

  Notation Sigma := (x0 ++ y0 ++ sym R).

  Definition dollar := fresh Sigma.
  Notation "$" := dollar.
  Definition hash := fresh (dollar :: Sigma).
  Notation "#" := hash.

  Lemma sep_doll : $ <> #.
  Proof.
(* Goal: not (@eq nat dollar hash) *)
    intros H. symmetry in H. now eapply fresh_spec in H.
  Qed.

  Lemma doll_sig a : a el Sigma -> $ <> a.
  Proof.
(* Goal: forall _ : @In nat a (@app nat x0 (@app nat y0 (sym R))), not (@eq nat dollar a) *)
    now eapply fresh_spec.
  Qed.

  Lemma hash_sig a : a el Sigma -> # <> a.
  Proof.
(* Goal: forall _ : @In nat a (@app nat x0 (@app nat y0 (sym R))), not (@eq nat hash a) *)
    intros; eapply fresh_spec. eauto.
  Qed.
  
  Definition d := [$] / ($ :: x0 ++ [#]).
  Definition e := (y0 ++ [#;$]) / [$].
  Definition P := [d ; e] ++ R ++ [ ([#] / [#] )] ++ map (fun a => [a] / [a]) Sigma.

  Lemma P_inv c :
    c el P ->
    c = d \/ c = e \/ c el R \/ c = ( [#] / [#] ) \/ exists a, a el Sigma /\ c = [a] / [a].
  Proof.
(* Goal: @eq (PCP.string nat) (@app nat x1 (@app nat (@tau1 nat (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat))))) (@app nat y1 (@app nat (@tau1 nat (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat))))) (@tau1 nat A))))) (@app nat x1 (@app nat u (@app nat y1 (@app nat (@cons nat hash (@nil nat)) (@app nat x1 (@app nat (@tau2 nat (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat))))) (@app nat y1 (@app nat (@tau2 nat (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat))))) (@tau2 nat A))))))))) *)
    cbn. intros. firstorder. eapply in_app_iff in H. firstorder.
(* Goal: iff (@ex (list (prod (list nat) (list nat))) (fun A : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) A (P R x y)) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) (d R x y) A)) (@tau2 nat (@cons (prod (list nat) (list nat)) (d R x y) A))))) (MPCP (@pair (prod (list nat) (list nat)) (list (prod (list nat) (list nat))) (d R x y) (P R x y))) *)
    eapply in_map_iff in H. firstorder.
  Qed.

  Lemma cards_subset x1 : x1 <<= Sigma -> cards x1 <<= P.
  Proof.
(* Goal: forall _ : @incl nat x1 (@app nat x0 (@app nat y0 (sym R))), @incl (prod (list symbol) (list symbol)) (cards x1) P *)
    induction x1.
(* Goal: iff (@ex (list (prod (list nat) (list nat))) (fun A : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) A (P R x y)) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) (d R x y) A)) (@tau2 nat (@cons (prod (list nat) (list nat)) (d R x y) A))))) (MPCP (@pair (prod (list nat) (list nat)) (list (prod (list nat) (list nat))) (d R x y) (P R x y))) *)
    - firstorder.
(* Goal: forall (x y : string) (_ : rew R x y) (_ : rewt R y y0) (_ : forall _ : @incl nat y (@app nat x0 (@app nat y0 (sym R))), @ex (list (prod (list nat) (list nat))) (fun A : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) A P) (@eq (PCP.string nat) (@tau1 nat A) (@app nat y (@app nat (@cons nat hash (@nil nat)) (@tau2 nat A)))))) (_ : @incl nat x (@app nat x0 (@app nat y0 (sym R)))), @ex (list (prod (list nat) (list nat))) (fun A : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) A P) (@eq (PCP.string nat) (@tau1 nat A) (@app nat x (@app nat (@cons nat hash (@nil nat)) (@tau2 nat A))))) *)
    - intros. intros [] [].
      + inv H0.  unfold P. eauto 15.
(* Goal: iff (@ex (list (prod (list nat) (list nat))) (fun A : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) A (P R x y)) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) (d R x y) A)) (@tau2 nat (@cons (prod (list nat) (list nat)) (d R x y) A))))) (MPCP (@pair (prod (list nat) (list nat)) (list (prod (list nat) (list nat))) (d R x y) (P R x y))) *)
      + eapply IHx1; firstorder.
  Qed.

  Lemma rew_subset u v : u / v el R -> u / v el P.
  Proof.
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
    unfold P. intros. eauto.
  Qed.
  
  Fact SR_MPCP x :
    x <<= Sigma -> x ≻* y0 -> exists A, A <<= P /\ tau1 A = x ++ [#] ++ tau2 A.
  Proof.
(* Goal: forall (x y : string) (_ : rew R x y) (_ : rewt R y y0) (_ : forall _ : @incl nat y (@app nat x0 (@app nat y0 (sym R))), @ex (list (prod (list nat) (list nat))) (fun A : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) A P) (@eq (PCP.string nat) (@tau1 nat A) (@app nat y (@app nat (@cons nat hash (@nil nat)) (@tau2 nat A)))))) (_ : @incl nat x (@app nat x0 (@app nat y0 (sym R)))), @ex (list (prod (list nat) (list nat))) (fun A : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) A P) (@eq (PCP.string nat) (@tau1 nat A) (@app nat x (@app nat (@cons nat hash (@nil nat)) (@tau2 nat A))))) *)
    intros. revert H. pattern x; refine (rewt_induct _ _ H0).
(* Goal: @eq (PCP.string nat) (@app nat x1 (@app nat (@tau1 nat (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat))))) (@app nat y1 (@app nat (@tau1 nat (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat))))) (@tau1 nat A))))) (@app nat x1 (@app nat u (@app nat y1 (@app nat (@cons nat hash (@nil nat)) (@app nat x1 (@app nat (@tau2 nat (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat))))) (@app nat y1 (@app nat (@tau2 nat (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat))))) (@tau2 nat A))))))))) *)
    - exists [e]. cbn. firstorder. now simpl_list.
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
    - clear x H0. intros. inv H. destruct H1 as (A & ? & ?). repeat eapply incl_app; eauto.
      exists (cards x1 ++ [(u / v)] ++ cards y1 ++ [ [#] / [#] ] ++ A). split.
      + repeat (eapply incl_app); unfold P; eauto using cards_subset, rew_subset.
(* Goal: @eq (PCP.string nat) (@app nat x1 (@app nat (@tau1 nat (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat))))) (@app nat y1 (@app nat (@tau1 nat (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat))))) (@tau1 nat A))))) (@app nat x1 (@app nat u (@app nat y1 (@app nat (@cons nat hash (@nil nat)) (@app nat x1 (@app nat (@tau2 nat (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat))))) (@app nat y1 (@app nat (@tau2 nat (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat))))) (@tau2 nat A))))))))) *)
      + simpl_list. cbn. rewrite H1. now simpl_list. 
  Qed.

  Fact MPCP_SR x y A :
    A <<= P -> x <<= Sigma -> y <<= Sigma -> 
    tau1 A = x ++ [#] ++ y ++ tau2 A ->
    y ++ x ≻* y0.
  Proof.
(* Goal: forall (x y : string) (_ : rew R x y) (_ : rewt R y y0) (_ : forall _ : @incl nat y (@app nat x0 (@app nat y0 (sym R))), @ex (list (prod (list nat) (list nat))) (fun A : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) A P) (@eq (PCP.string nat) (@tau1 nat A) (@app nat y (@app nat (@cons nat hash (@nil nat)) (@tau2 nat A)))))) (_ : @incl nat x (@app nat x0 (@app nat y0 (sym R)))), @ex (list (prod (list nat) (list nat))) (fun A : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) A P) (@eq (PCP.string nat) (@tau1 nat A) (@app nat x (@app nat (@cons nat hash (@nil nat)) (@tau2 nat A))))) *)
    intros ?. revert x y. induction A; intros.
    - exfalso. destruct x; inv H2.
    - assert (a el P) as [ -> | [ ->  | [ | [-> | (? & ? & ->)]]]]  % P_inv by (now apply H).
      + exfalso. cbn -[fresh] in H2. destruct x. inv H2. destruct (sep_doll H4).
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
        inversion H2. edestruct doll_sig; eauto.        
      + cbn -[fresh] in *.
        autorewrite with list in *. cbn -[fresh] in *.
        eapply list_prefix_inv in H2 as [<- ?].
        destruct y.
        * reflexivity.
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
        * exfalso. inversion H2. edestruct doll_sig; eauto. 
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
        * intros E. edestruct hash_sig; eauto.
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
        * intros E. edestruct hash_sig; eauto.
      + destruct a as (u, v).
        cbn -[fresh] in H2.
        edestruct (split_inv H2) as (x' & ->).
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
        intros E. edestruct hash_sig. unfold Sigma. rewrite !in_app_iff. do 2 right. now eapply sym_word_l; eauto. reflexivity.
        econstructor. eauto using rew.
        enough ( (y ++ v) ++ x' ≻* y0) by now autorewrite with list in *.
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
        eapply IHA; eauto. autorewrite with list in *. now eapply app_inv_head in H2.
      + cbn -[fresh] in H2. destruct x; [inv H2 |].
        * simpl_list. change y with ([] ++ y). eapply IHA; eauto using cons_incl.
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
        * inversion H2. edestruct hash_sig; eauto.       
      + cbn -[fresh] in *. rename x1 into a. destruct x.
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
        * inversion H2. edestruct hash_sig; eauto.
        * inv H2.
          replace (y ++ n :: x) with ((y ++ [n]) ++ x) by now simpl_list.
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
          eapply IHA; eauto. simpl_list. eassumption.
  Qed.

  Corollary SR_MPCP_cor :
    x0 ≻* y0 <-> exists A, A <<= P /\ tau1 (d :: A) = tau2 (d :: A).
  Proof.
(* Goal: and (@incl (prod (list nat) (list nat)) (@app (prod (list symbol) (list symbol)) (cards x1) (@app (prod (PCP.string nat) (PCP.string nat)) (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat)))) (@app (prod (list symbol) (list symbol)) (cards y1) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) A)))) P) (@eq (PCP.string nat) (@tau1 nat (@app (prod (list symbol) (list symbol)) (cards x1) (@app (prod (PCP.string nat) (PCP.string nat)) (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat)))) (@app (prod (list symbol) (list symbol)) (cards y1) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) A))))) (@app nat (@app nat x1 (@app nat u y1)) (@app nat (@cons nat hash (@nil nat)) (@tau2 nat (@app (prod (list symbol) (list symbol)) (cards x1) (@app (prod (PCP.string nat) (PCP.string nat)) (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat)))) (@app (prod (list symbol) (list symbol)) (cards y1) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) A)))))))) *)
    split.
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
    - intros ?. cbn in H. eapply SR_MPCP in H as (A & ? & ?); eauto.
(* Goal: @eq (PCP.string nat) (@app nat x1 (@app nat (@tau1 nat (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat))))) (@app nat y1 (@app nat (@tau1 nat (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat))))) (@tau1 nat A))))) (@app nat x1 (@app nat u (@app nat y1 (@app nat (@cons nat hash (@nil nat)) (@app nat x1 (@app nat (@tau2 nat (@cons (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@nil (prod (PCP.string nat) (PCP.string nat))))) (@app nat y1 (@app nat (@tau2 nat (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat))))) (@tau2 nat A))))))))) *)
      exists A. firstorder. cbn. rewrite H0. cbn. now simpl_list.
(* Goal: @In (prod (PCP.string nat) (PCP.string nat)) (@pair (PCP.string nat) (PCP.string nat) u v) (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat))))) (@app (PCP.card nat) R (@app (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) (@pair (list nat) (list nat) (@cons nat hash (@nil nat)) (@cons nat hash (@nil nat))) (@nil (prod (list nat) (list nat)))) (@map nat (prod (list nat) (list nat)) (fun a : nat => @pair (list nat) (list nat) (@cons nat a (@nil nat)) (@cons nat a (@nil nat))) (@app nat x0 (@app nat y0 (sym R))))))) *)
    - intros (A & ? & ?). eapply MPCP_SR with (y := []) (A := A); eauto.
(* Goal: @In (prod (list symbol) (list symbol)) (@pair (list symbol) (list symbol) l l0) P *)
      inv H0. rewrite H2. now simpl_list.
  Qed.
      
End SR_to_MPCP.

Theorem reduction :
  SR ⪯ MPCP.
Proof.
(* Goal: @reduces (prod (prod SRS string) string) (prod (prod (PCP.string nat) (PCP.string nat)) (list (prod (PCP.string nat) (PCP.string nat)))) SR MPCP *)
  exists (fun '(R, x, y) => (d R x y, P R x y)). intros [[R x] y].
(* Goal: iff (@ex (list (prod (list nat) (list nat))) (fun A : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) A (P R x y)) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) (d R x y) A)) (@tau2 nat (@cons (prod (list nat) (list nat)) (d R x y) A))))) (MPCP (@pair (prod (list nat) (list nat)) (list (prod (list nat) (list nat))) (d R x y) (P R x y))) *)
  unfold SR. rewrite SR_MPCP_cor. firstorder.
Qed.
