Require Import 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.
  destruct l; cbn; firstorder congruence.
Qed.


Section MPCP_PCP.

  Variable R : SRS.
  Variable : string.

  Definition := sym (/ :: R).
  Definition R_Sigma : sym R .
  Proof. unfold . cbn. eauto. Qed.

  Definition dollar := fresh .
  Notation "$" := dollar.
  Definition hash := fresh (dollar :: ).
  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 )) / ($ :: # :: (#_R )).
  Definition e := [#;$] / [$].
  Definition P := [d;e] map ( '(x,y) (#_L x, #_R y)) (filter ( '(x,y) is_cons x || is_cons y) (/::R)).

  Lemma P_inv c :
    c P
    c = d c = e ( x y, (x,y) (/ :: R) c = (#_L x, #_R y) ( (x,y) (nil, nil))).
  Proof.
    cbn -[filter]. intros. firstorder. eapply in_map_iff in H as ((x,y) & & (? & ? % orb_prop) % filter_In).
    rewrite !is_cons_true_iff in .
    right. right. exists x, y. firstorder; destruct x, y; cbn; firstorder congruence.
  Qed.


  Lemma P_inv_top x y a :
    a
    (a :: x,y) P.
  Proof.
    intros ? [ | [ | (x'' & y' & ? & ? & ?) ] ] % P_inv.
    - inv . edestruct fresh_spec; eauto.
    - inv . edestruct fresh_spec with (l := dollar :: ); [ | reflexivity]. firstorder.
    - inv . destruct x''; cbn -[fresh] in *; [congruence | ]. inversion .
      edestruct fresh_spec with (l := dollar :: ); [ | reflexivity ]. unfold hash in *.
      rewrite . firstorder.
  Qed.


  Lemma tau1_inv a B z :
     B = a :: z
     x y, (a :: x, y) B.
  Proof.
    induction B; cbn; intros; inv H.
    destruct as ([],y).
    - cbn in . firstorder.
    - cbn in . inv . eauto.
  Qed.


  Lemma P_inv_bot x y :
    (y, # :: x) P.
  Proof.
    intros [ | [ | (x'' & y' & ? & ? & ?) ] ] % P_inv.
    - inv H. edestruct fresh_spec; eauto. eauto.
    - inv H. edestruct fresh_spec; eauto. eauto.
    - inv . destruct y'; cbn -[fresh] in *; [congruence | ]. inversion .
      edestruct fresh_spec with (l := dollar :: ); [ | reflexivity ]. unfold hash in *.
      rewrite . right. eapply sym_word_R; eauto.
  Qed.


  Lemma tau2_inv a B z :
     B = a :: z
     x y, (y, a :: x) B.
  Proof.
    induction B; cbn; intros; inv H.
    destruct as (x,[]).
    - cbn in . firstorder.
    - cbn in . inv . eauto.
  Qed.


  Lemma match_start d' B :
    d' :: B P (d' :: B) = (d' :: B) d' = d.
  Proof.
    intros Hs Hm.
    assert (d' P) as [ | [ | (x & y & ? & & ?) ] ] % P_inv by now eapply Hs; cbn -[fresh] in Hm.
    - congruence.
    - inv Hm. now edestruct fresh_spec; eauto.
    - cbn in Hm. destruct x, y; try firstorder congruence.
      + destruct (tau1_inv Hm) as (x' & y' & ? ).
        assert ( (s :: x') / y' P) as [] % P_inv_top by firstorder.
        eapply sym_word_R; eauto.
      + cbn -[fresh] in Hm. symmetry in Hm. destruct (tau2_inv Hm) as (x' & y' & ? ).
        assert ( y' / (# :: x') P) as [] % P_inv_bot by firstorder.
      + cbn -[fresh] in Hm. inversion Hm. edestruct fresh_spec; eauto. right.
        eapply sym_word_R in H. firstorder.
  Qed.


  Lemma hash_swap x :
    #_L x [#] = # :: #_R x.
  Proof.
    induction x; cbn in *; now try rewrite IHx.
  Qed.


  Lemma hash_L_app x y :
    #_L (x y) = #_L x #_L y.
  Proof.
    induction x; cbn in *; now try rewrite IHx.
  Qed.


  Lemma hash_R_app x y :
    #_R (x y) = #_R x #_R y.
  Proof.
    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.
    destruct y; inv . firstorder.
  Qed.


  Lemma hash_R_inv x y :
    #_R x = #_R y x = y.
  Proof.
    revert y; induction x; intros [] H; inv H; firstorder congruence.
  Qed.


  Lemma doll_hash_L x:
    x $ #_L x.
  Proof.
    induction x; intros.
    -- firstorder.
    -- intros [ | []].
       ++ now eapply fresh_spec in as [].
       ++ symmetry in . eapply fresh_spec in as []. firstorder.
       ++ firstorder.
  Qed.


  Lemma MPCP_PCP x y A :
    A / :: R x A = y A
     B, B P (#_L x) B = # :: #_R y B.
  Proof.
    revert x y; induction A; cbn -[fresh P] in *; intros.
    - rewrite !app_nil_r in . subst. exists [e]. firstorder.
      cbn -[fresh].
      enough ((#_L y [#]) [$] = # :: #_R y [$]) by now autorewrite with list in *.
      now rewrite hash_swap.
    - destruct a as (x', y').
      assert ( (x x') A = (y y') A) by now simpl_list.
      eapply IHA in as (B & ? & ?) ; [ | firstorder].
      rewrite hash_L_app, hash_R_app in .
      autorewrite with list in .
      destruct (is_cons x' || is_cons y') eqn:E.
      + exists ( (#_L x' / #_R y') :: B). split.
        * intros ? [ | ]; [ | eauto].
          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.
        destruct x', y'; firstorder congruence.
  Qed.


  Lemma PCP_MPCP x y B :
    B P x y
    (#_L x) B = # :: (#_R y) B
     A, A /::R x A = y A.
  Proof.
    revert x y. induction B; cbn -[fresh P] in *; intros.
    - exfalso. rewrite !app_nil_r in . eapply hash_L_diff in as [].
    - assert (a P) as [ | [ | (x' & y' & ? & & ?) ] ] % P_inv by intuition; cbn -[fresh P] in *.
      + exfalso. setoid_rewrite app_comm_cons in at 2.
        eapply list_prefix_inv in as [[] % hash_L_diff ].
        * now eapply doll_hash_L.
        * rewrite hash_swap. rewrite in_app_iff. intros [ | [ | []]]. eapply doll_hash_L; eauto.
          now eapply fresh_spec in as [].
      + exists []. assert ((#_L x [#]) $ :: B = (# :: #_R y) $ :: B) by now simpl_list.
        eapply list_prefix_inv in .
        rewrite hash_swap in . inv .
        inv . eapply hash_R_inv in as . firstorder.
        * rewrite in_app_iff. intros [ | [ | []]]. eapply doll_hash_L in ; eauto.
          now eapply fresh_spec in as [].
        * rewrite hash_swap. rewrite in_app_iff. intros [ | [ | []]]. eapply doll_hash_L; eauto.
          now eapply fresh_spec in as [].
      + assert ((#_L x #_L x') B = # :: (#_R y #_R y') B) by now simpl_list.
        rewrite hash_L_app, hash_R_app in . eapply IHB in as (A & ? & ?).
        * exists (x' / y' :: A). intuition; try inv ; intuition;
          cbn; now autorewrite with list in *.
        * eauto.
        * eapply incl_app. eauto. intros ? ?. destruct . inv . eauto. eapply R_Sigma, sym_word_l; eauto.
        * eapply incl_app. eauto. intros ? ?. destruct . inv . eauto. eapply R_Sigma, sym_word_R; eauto.
  Qed.


  Lemma MPCP_PCP_cor :
    MPCP (/, R) PCP P.
  Proof.
    split.
    - intros (A & Hi & (B & HiB & H) % MPCP_PCP).
      exists (d :: B). firstorder. congruence.
      cbn. f_equal. now rewrite H. eassumption.
    - intros ([|d' B] & Hi & He & H); firstorder.
      pose proof H as % match_start; eauto.
      cbn -[fresh] in H. inv H.
      eapply PCP_MPCP in ; cbn; eauto.
  Qed.


End MPCP_PCP.

Theorem reduction :
  MPCP PCP.
Proof.
  exists ( '(x, y, R) P R x y).
  intros ((x & y) & R).
  eapply MPCP_PCP_cor.
Qed.