Require Import Undecidability.PCP.Definitions.

(** * MPCP to PCP *)

Definition is_cons X (l : list X) :=
  match l with
  | [] => false
  | _ => true
  end.

Lemma is_cons_true_iff X (l : list X) :
  is_cons l = true <-> l <> [].
Proof.
(* Goal: iff (@eq bool (@is_cons X l) true) (not (@eq (list X) l (@nil X))) *)
  destruct l; cbn; firstorder congruence.
Qed.

Section MPCP_PCP.

  Variable R : SRS.
  Variable x0 y0 : string.

  Definition Sigma := sym (x0/y0 :: R).
  Definition R_Sigma : sym R <<= Sigma.
  Proof. unfold Sigma. cbn. eauto. Qed.

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

  Fixpoint hash_l (x : string) :=
    match x with
    | [] => []
    | a :: x => # :: a :: hash_l x
    end.
  Notation "#_L" := hash_l.

  Fixpoint hash_r (x : string) :=
    match x with
    | [] => []
    | a :: x => a :: # :: hash_r x
    end.
  Notation "#_R" := hash_r.

  Definition d := ($ :: (#_L x0)) / ($ :: # :: (#_R y0)).
  Definition e := [#;$] / [$].
  Definition P := [d;e] ++ map (fun '(x,y) => (#_L x, #_R y)) (filter (fun '(x,y) => is_cons x || is_cons y) (x0/y0::R)).

  Lemma P_inv c :
    c el P ->
    c = d \/ c = e \/ (exists x y, (x,y) el (x0/y0 :: R) /\ c = (#_L x, #_R y)  /\ ( (x,y) <> (nil, nil))).
  Proof.
(* Goal: forall _ : @In (prod (list nat) (list nat)) c P, or (@eq (prod (list nat) (list nat)) c d) (or (@eq (prod (list nat) (list nat)) c e) (@ex string (fun x : string => @ex string (fun y : string => and (@In (prod string string) (@pair string string x y) (@cons (prod string string) (@pair string string x0 y0) R)) (and (@eq (prod (list nat) (list nat)) c (@pair (list nat) (list nat) (hash_l x) (hash_r y))) (not (@eq (prod string string) (@pair string string x y) (@pair (list nat) (list nat) (@nil nat) (@nil nat))))))))) *)
    cbn -[filter]. intros. firstorder. eapply in_map_iff in H as ((x,y) & <- & (? & ? % orb_prop) % filter_In).
(* Goal: or (@eq (prod (list nat) (list nat)) (@pair (list nat) (list nat) (hash_l x) (hash_r y)) d) (or (@eq (prod (list nat) (list nat)) (@pair (list nat) (list nat) (hash_l x) (hash_r y)) e) (@ex string (fun x1 : string => @ex string (fun y1 : string => and (or (@eq (prod string string) (@pair string string x0 y0) (@pair string string x1 y1)) (@In (prod string string) (@pair string string x1 y1) R)) (and (@eq (prod (list nat) (list nat)) (@pair (list nat) (list nat) (hash_l x) (hash_r y)) (@pair (list nat) (list nat) (hash_l x1) (hash_r y1))) (not (@eq (prod string string) (@pair string string x1 y1) (@pair (list nat) (list nat) (@nil nat) (@nil nat))))))))) *)
    rewrite !is_cons_true_iff in H1.
(* Goal: or (@In (prod (list nat) (list nat)) (@pair (list nat) (list nat) (hash_l x') (hash_r y')) (@cons (prod (list nat) (list nat)) d (@cons (prod (list nat) (list nat)) e (@nil (prod (list nat) (list nat)))))) (@ex (prod string string) (fun x : prod string string => and (@eq (prod (list nat) (list nat)) (let 'pair x0 y := x in @pair (list nat) (list nat) (hash_l x0) (hash_r y)) (@pair (list nat) (list nat) (hash_l x') (hash_r y'))) (@In (prod string string) x (@filter (prod (list nat) (list nat)) (fun '(pair x0 y) => orb (@is_cons nat x0) (@is_cons nat y)) (@cons (prod string string) (@pair string string x0 y0) R))))) *)
    right. right. exists x, y. firstorder; destruct x, y; cbn; firstorder congruence.
  Qed.

  Lemma P_inv_top x y a :
    a el Sigma ->
    ~(a :: x,y) el P.
  Proof.
    intros ? [  | [   | (x'' & y' & ? & ? & ?) ] ] % P_inv.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
    - inv H0. edestruct fresh_spec; eauto.
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
    - inv H0. edestruct fresh_spec with (l := dollar :: Sigma); [ | reflexivity]. firstorder.
    - inv H1. destruct x''; cbn -[fresh] in *; [congruence | ]. inversion H4.
(* Goal: False *)
      edestruct fresh_spec with (l := dollar :: Sigma); [ | reflexivity ]. unfold hash in *.
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
      rewrite <- H3. firstorder.
  Qed.

  Lemma tau1_inv (a : nat) B z :
    tau1 B = a :: z ->
    exists x y, (a :: x, y) el B.
  Proof.
(* Goal: forall _ : @eq (PCP.string nat) (@tau2 nat B) (@cons nat a z), @ex (list nat) (fun x : list nat => @ex (PCP.string nat) (fun y : PCP.string nat => @In (prod (PCP.string nat) (list nat)) (@pair (PCP.string nat) (list nat) y (@cons nat a x)) B)) *)
    induction B; cbn; intros; inv H.
(* Goal: @ex (list nat) (fun x : list nat => @ex (PCP.string nat) (fun y : PCP.string nat => or (@eq (prod (list nat) (PCP.string nat)) a0 (@pair (list nat) (PCP.string nat) (@cons nat a x) y)) (@In (prod (list nat) (PCP.string nat)) (@pair (list nat) (PCP.string nat) (@cons nat a x) y) B))) *)
    destruct a0 as ([],y).
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
    - cbn in H1. firstorder.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
    - cbn in H1. inv H1. eauto.
  Qed.

  Lemma P_inv_bot x y :
    ~(y, # :: x) el P.
  Proof.
    intros [  | [  | (x'' & y' & ? & ? & ?) ] ] % P_inv.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
    - inv H. edestruct fresh_spec; eauto. eauto.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
    - inv H. edestruct fresh_spec; eauto. eauto.
    - inv H0. destruct y'; cbn -[fresh] in *; [congruence | ]. inversion H4.
(* Goal: False *)
      edestruct fresh_spec with (l := dollar :: Sigma); [ | reflexivity ]. unfold hash in *.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
      rewrite H2. right. eapply sym_word_R; eauto.
  Qed.

  Lemma tau2_inv (a : nat) B z :
    tau2 B = a :: z ->
    exists x y, (y, a :: x) el B.
  Proof.
(* Goal: forall _ : @eq (PCP.string nat) (@tau2 nat B) (@cons nat a z), @ex (list nat) (fun x : list nat => @ex (PCP.string nat) (fun y : PCP.string nat => @In (prod (PCP.string nat) (list nat)) (@pair (PCP.string nat) (list nat) y (@cons nat a x)) B)) *)
    induction B; cbn; intros; inv H.
(* Goal: @ex (list nat) (fun x : list nat => @ex (PCP.string nat) (fun y : PCP.string nat => or (@eq (prod (PCP.string nat) (list nat)) a0 (@pair (PCP.string nat) (list nat) y (@cons nat a x))) (@In (prod (PCP.string nat) (list nat)) (@pair (PCP.string nat) (list nat) y (@cons nat a x)) B))) *)
    destruct a0 as (x,[]).
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
    - cbn in H1. firstorder.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
    - cbn in H1. inv H1. eauto.
  Qed.
  
  Lemma match_start d' B :
    d' :: B <<= P -> tau1 (d' :: B) = tau2 (d' :: B) -> d' = d.
  Proof.
(* Goal: forall (_ : @incl (prod (list nat) (list nat)) (@cons (prod (list nat) (list nat)) d' B) P) (_ : @eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d' B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d' B))), @eq (prod (list nat) (list nat)) d' d *)
    intros Hs Hm.
    assert (d' el P) as [ -> | [ ->  | (x & y & ? & -> & ?) ] ] % P_inv by now eapply Hs; cbn -[fresh] in Hm.
    - congruence.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
    - inv Hm. now edestruct fresh_spec; eauto.
    - cbn in Hm. destruct x, y; try firstorder congruence.
      + destruct (tau1_inv Hm) as (x' & y' & ? ).
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
        assert ( (n :: x') / y' el P) as [] % P_inv_top by firstorder.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
        eapply sym_word_R; eauto.        
      + cbn -[fresh] in Hm. symmetry in Hm. destruct (tau2_inv Hm) as (x' & y' & ? ).
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
        assert ( y' / (# :: x') el P) as [] % P_inv_bot by firstorder.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
      + cbn -[fresh] in Hm. inversion Hm. edestruct fresh_spec; eauto. right.
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
        eapply sym_word_R in H. firstorder.
  Qed.

  Lemma hash_swap x :
    #_L x ++ [#] = # :: #_R x.
  Proof.
(* Goal: @eq (list nat) (hash_r (@app nat x y)) (@app nat (hash_r x) (hash_r y)) *)
    induction x; cbn in *; now try rewrite IHx.
  Qed.

  Lemma hash_L_app x y :
    #_L (x ++ y) = #_L x ++ #_L y.
  Proof.
(* Goal: @eq (list nat) (hash_r (@app nat x y)) (@app nat (hash_r x) (hash_r y)) *)
    induction x; cbn in *; now try rewrite IHx.
  Qed.

  Lemma hash_R_app x y :
    #_R (x ++ y) = #_R x ++ #_R y.
  Proof.
(* Goal: @eq (list nat) (hash_r (@app nat x y)) (@app nat (hash_r x) (hash_r y)) *)
    induction x; cbn in *; now try rewrite IHx.
  Qed.

  Lemma hash_L_diff x y :
    #_L x <> # :: #_R  y.
  Proof.
    revert y. induction x; cbn -[fresh]; intros ? ?; inv H.
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
    destruct y; inv H1. firstorder.
  Qed.

  Lemma hash_R_inv x y :
    #_R x = #_R y -> x = y.
  Proof.
(* Goal: not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat))) *)
(* Goal: @eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
    revert y; induction x; intros [] H; inv H; firstorder congruence.
  Qed.
  
  Lemma doll_hash_L x:
    x <<= Sigma -> ~ $ el #_L x.
  Proof.
(* Goal: forall _ : or (@eq (prod (list nat) (list nat)) d c) (or (@eq (prod (list nat) (list nat)) e c) (@In (prod (list nat) (list nat)) c (@map (prod string string) (prod (list nat) (list nat)) (fun '(pair x y) => @pair (list nat) (list nat) (hash_l x) (hash_r y)) (@filter (prod (list nat) (list nat)) (fun '(pair x y) => orb (@is_cons nat x) (@is_cons nat y)) (@cons (prod string string) (@pair string string x0 y0) R))))), or (@eq (prod (list nat) (list nat)) c d) (or (@eq (prod (list nat) (list nat)) c e) (@ex string (fun x : string => @ex string (fun y : string => and (or (@eq (prod string string) (@pair string string x0 y0) (@pair string string x y)) (@In (prod string string) (@pair string string x y) R)) (and (@eq (prod (list nat) (list nat)) c (@pair (list nat) (list nat) (hash_l x) (hash_r y))) (not (@eq (prod string string) (@pair string string x y) (@pair (list nat) (list nat) (@nil nat) (@nil nat))))))))) *)
    induction x; intros.
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
    -- firstorder.
    -- intros [ | []].
       ++ now eapply fresh_spec in H0 as []. 
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
       ++ symmetry in H0. eapply fresh_spec in H0 as []. firstorder.
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
       ++ firstorder.
  Qed.

  Lemma MPCP_PCP x y A :
    A <<= x0/y0 :: R -> x ++ tau1 A = y ++ tau2 A ->
    exists B, B <<= P /\ (#_L x) ++ tau1 B = # :: #_R y ++ tau2 B.
  Proof.
(* Goal: forall _ : or (@eq (prod (list nat) (list nat)) d c) (or (@eq (prod (list nat) (list nat)) e c) (@In (prod (list nat) (list nat)) c (@map (prod string string) (prod (list nat) (list nat)) (fun '(pair x y) => @pair (list nat) (list nat) (hash_l x) (hash_r y)) (@filter (prod (list nat) (list nat)) (fun '(pair x y) => orb (@is_cons nat x) (@is_cons nat y)) (@cons (prod string string) (@pair string string x0 y0) R))))), or (@eq (prod (list nat) (list nat)) c d) (or (@eq (prod (list nat) (list nat)) c e) (@ex string (fun x : string => @ex string (fun y : string => and (or (@eq (prod string string) (@pair string string x0 y0) (@pair string string x y)) (@In (prod string string) (@pair string string x y) R)) (and (@eq (prod (list nat) (list nat)) c (@pair (list nat) (list nat) (hash_l x) (hash_r y))) (not (@eq (prod string string) (@pair string string x y) (@pair (list nat) (list nat) (@nil nat) (@nil nat))))))))) *)
    revert x y; induction A; cbn -[fresh P] in *; intros.
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
    - rewrite !app_nil_r in H0. subst. exists [e]. firstorder.
      cbn -[fresh].
      enough ((#_L y ++ [#]) ++ [$] = # :: #_R y ++ [$]) by now autorewrite with list in *.
(* Goal: @eq (list nat) (@app nat (@app nat (hash_l y) (@cons nat hash (@nil nat))) (@cons nat dollar (@nil nat))) (@cons nat hash (@app nat (hash_r y) (@cons nat dollar (@nil nat)))) *)
      now rewrite hash_swap.
    - destruct a as (x', y').
      assert ( (x ++ x') ++ tau1 A = (y ++ y') ++ tau2 A) by now simpl_list.
(* Goal: @ex (list (prod (list nat) (list nat))) (fun B : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) B P) (@eq (list nat) (@app nat (hash_l x) (@tau1 nat B)) (@cons nat hash (@app nat (hash_r y) (@tau2 nat B))))) *)
      eapply IHA in H1 as (B & ? & ?) ; [ | firstorder].
(* Goal: @ex (list (prod (list nat) (list nat))) (fun B : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) B P) (@eq (list nat) (@app nat (hash_l x) (@tau1 nat B)) (@cons nat hash (@app nat (hash_r y) (@tau2 nat B))))) *)
      rewrite hash_L_app, hash_R_app in H2.
(* Goal: @ex (list (prod (list nat) (list nat))) (fun B : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) B P) (@eq (list nat) (@app nat (hash_l x) (@tau1 nat B)) (@cons nat hash (@app nat (hash_r y) (@tau2 nat B))))) *)
      autorewrite with list in H2.
(* Goal: @ex (list (prod (list nat) (list nat))) (fun B : list (prod (list nat) (list nat)) => and (@incl (prod (list nat) (list nat)) B P) (@eq (list nat) (@app nat (hash_l x) (@tau1 nat B)) (@cons nat hash (@app nat (hash_r y) (@tau2 nat B))))) *)
      destruct (is_cons x' || is_cons y') eqn:E.
      + exists ( (#_L x' / #_R y') :: B). split.
        * intros ? [ <- | ]; [ | eauto].
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
          unfold P. rewrite in_app_iff, in_map_iff. right. exists (x', y'). eauto.
        * eassumption. 
      + exists B. rewrite orb_false_iff, <- !not_true_iff_false, !is_cons_true_iff in E. destruct E.
(* Goal: not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat))) *)
(* Goal: @eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
        destruct x', y'; firstorder congruence.
  Qed.

  Lemma PCP_MPCP x y B :
    B <<= P -> x <<= Sigma -> y <<= Sigma ->
    (#_L x) ++ tau1 B = # :: (#_R y) ++ tau2 B ->
    exists A, A <<= x0/y0::R /\ x ++ tau1 A = y ++ tau2 A.
  Proof.
(* Goal: forall _ : or (@eq (prod (list nat) (list nat)) d c) (or (@eq (prod (list nat) (list nat)) e c) (@In (prod (list nat) (list nat)) c (@map (prod string string) (prod (list nat) (list nat)) (fun '(pair x y) => @pair (list nat) (list nat) (hash_l x) (hash_r y)) (@filter (prod (list nat) (list nat)) (fun '(pair x y) => orb (@is_cons nat x) (@is_cons nat y)) (@cons (prod string string) (@pair string string x0 y0) R))))), or (@eq (prod (list nat) (list nat)) c d) (or (@eq (prod (list nat) (list nat)) c e) (@ex string (fun x : string => @ex string (fun y : string => and (or (@eq (prod string string) (@pair string string x0 y0) (@pair string string x y)) (@In (prod string string) (@pair string string x y) R)) (and (@eq (prod (list nat) (list nat)) c (@pair (list nat) (list nat) (hash_l x) (hash_r y))) (not (@eq (prod string string) (@pair string string x y) (@pair (list nat) (list nat) (@nil nat) (@nil nat))))))))) *)
    revert x y. induction B; cbn -[fresh P] in *; intros.
    - exfalso. rewrite !app_nil_r in H2. eapply hash_L_diff in H2 as [].
    - assert (a el P) as [ -> | [ ->  | (x' & y' & ? & -> & ?) ] ] % P_inv by intuition; cbn -[fresh P] in *.
      + exfalso. setoid_rewrite app_comm_cons in H2 at 2.
(* Goal: False *)
        eapply list_prefix_inv in H2 as [[] % hash_L_diff E2].
        * now eapply doll_hash_L.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
        * rewrite <- hash_swap. rewrite in_app_iff. intros [ | [ | []]]. eapply doll_hash_L; eauto.
(* Goal: False *)
          now eapply fresh_spec in H3 as []. 
      + exists []. assert ((#_L x ++ [#]) ++ $ :: tau1 B = (# :: #_R y) ++ $ :: tau2 B) by now simpl_list.
(* Goal: and (@incl (prod string string) (@nil (prod string string)) (@cons (prod string string) (@pair string string x0 y0) R)) (@eq (list nat) (@app nat x (@tau1 nat (@nil (prod string string)))) (@app nat y (@tau2 nat (@nil (prod string string))))) *)
        eapply list_prefix_inv in H3.
(* Goal: and (@incl (prod string string) (@nil (prod string string)) (@cons (prod string string) (@pair string string x0 y0) R)) (@eq (list nat) (@app nat x (@tau1 nat (@nil (prod string string)))) (@app nat y (@tau2 nat (@nil (prod string string))))) *)
(* Goal: not (@In nat dollar (@app nat (hash_l x) (@cons nat hash (@nil nat)))) *)
(* Goal: not (@In nat dollar (@cons nat hash (hash_r y))) *)
        rewrite hash_swap in H3. inv H3.
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
        inv H4. eapply hash_R_inv in H6 as ->. firstorder.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
        * rewrite in_app_iff. intros [ | [ | []]]. eapply doll_hash_L in H4; eauto.
(* Goal: False *)
          now eapply fresh_spec in H4 as []. 
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
        * rewrite <- hash_swap. rewrite in_app_iff. intros [ | [ | []]]. eapply doll_hash_L; eauto.
(* Goal: False *)
          now eapply fresh_spec in H4 as []. 
      + assert ((#_L x ++ #_L x') ++ tau1 B = # :: (#_R y ++ #_R y') ++ tau2 B) by now simpl_list.
        rewrite <- hash_L_app, <- hash_R_app in H5. eapply IHB in H5 as (A & ? & ?).
        * exists (x' / y' :: A). intuition; try inv H7; intuition;
          cbn; now autorewrite with list in *. 
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
        * eauto.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
        * eapply incl_app. eauto. intros ? ?. destruct H3. inv H3. eauto. eapply R_Sigma, sym_word_l; eauto.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
        * eapply incl_app. eauto. intros ? ?. destruct H3. inv H3. eauto. eapply R_Sigma, sym_word_R; eauto.
  Qed.

  Lemma MPCP_PCP_cor :
    MPCP (x0/y0, R) <-> PCP P.
  Proof.
(* Goal: iff (MPCP (@pair (prod string string) SRS (@pair string string x0 y0) R)) (PCP P) *)
    split.
    - intros (A & Hi & (B & HiB & H) % MPCP_PCP).
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
      exists (d :: B). firstorder. congruence.
(* Goal: @eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
      cbn. f_equal. now rewrite H. eassumption.
(* Goal: and (@incl (PCP.card nat) (@cons (prod (list nat) (list nat)) d B) P) (and (not (@eq SRS (@cons (prod (list nat) (list nat)) d B) (@nil (PCP.card nat)))) (@eq (PCP.string nat) (@tau1 nat (@cons (prod (list nat) (list nat)) d B)) (@tau2 nat (@cons (prod (list nat) (list nat)) d B)))) *)
(* Goal: @incl (prod string string) A (@cons (prod string string) (@pair string string x0 y0) R) *)
    - intros ([|d' B] & Hi & He & H); firstorder.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
      pose proof H as -> % match_start; eauto.
      cbn -[fresh] in H. inv H.
(* Goal: @In nat a (@app nat x' (@app nat y' (sym R))) *)
(* Goal: @In nat a (@app nat x0 (@app nat y0 (sym R))) *)
      eapply PCP_MPCP in H1; cbn; eauto. 
  Qed.

End MPCP_PCP.

Theorem reduction :
  MPCP ⪯ PCP.
Proof.
(* Goal: @reduces (prod (prod (PCP.string nat) (PCP.string nat)) (list (prod (PCP.string nat) (PCP.string nat)))) (list (PCP.card nat)) MPCP PCP *)
  exists (fun '(x, y, R) => P R x y).
(* Goal: forall x : prod (prod (PCP.string nat) (PCP.string nat)) (list (prod (PCP.string nat) (PCP.string nat))), iff (MPCP x) (PCP (let 'pair (pair x0 y as y0) R := x in P R x0 y)) *)
  intros ((x & y) & R).
(* Goal: iff (MPCP (@pair (prod (PCP.string nat) (PCP.string nat)) (list (prod (PCP.string nat) (PCP.string nat))) (@pair (PCP.string nat) (PCP.string nat) x y) R)) (PCP (P R x y)) *)
  eapply MPCP_PCP_cor.
Qed.
  
                         
        
     

        
     
