Require Import List.
Import ListNotations.

Require Import Undecidability.PCP.PCP.
Require Import Undecidability.PCP.Util.Facts.

Require Import Undecidability.Shared.ListAutomation.
Require Import Undecidability.Synthetic.Definitions.

Set Default Proof Using "Type".

Section derivable_iff_PCPX.

  Variable X : Type.

  Implicit Type P : stack X.

  Lemma derivable_PCPX P u v : derivable P u v -> exists A, A <<= P /\ A <> nil /\ tau1 A = u /\ tau2 A = v.
  Proof.
    induction 1 as [ x y | x y ? ? ? ? (A & ? & ? & ? & ?)].
    - exists [(x,y)]; repeat split; cbn; simpl_list; auto; discriminate.
    - exists ((x,y) :: A); repeat split; simpl; auto; try discriminate; congruence.
  Qed.

  Lemma PCPX_derivable P u v : (exists A, A <<= P /\ A <> nil /\ tau1 A = u /\ tau2 A = v) -> derivable P u v.
  Proof.
    intros (A & H1 & H2 & <- & <-).
    revert H1; pattern A; revert A H2.
    eapply list_ind_ne; cbn; intros (x,y) H.
    - simpl_list; constructor 1; auto.
    - constructor 2; eauto.
  Qed.

  Theorem PCPX_iff_dPCP P : PCPX P <-> dPCP P.
  Proof.
    split.
    - intros (A & H1 & H2 & H3); exists (tau1 A).
      rewrite H3 at 2; apply PCPX_derivable.
      exists A; auto.
    - intros (u & Hu).
      apply derivable_PCPX in Hu.
      destruct Hu as (A & H1 & H2 & H3 & H4).
      exists A; subst; auto.
  Qed.

End derivable_iff_PCPX.

Lemma reductionLR (X : Type) : @PCPX X ⪯ @dPCP X.
Proof. exists id; intro; now rewrite PCPX_iff_dPCP. Qed.

Lemma reductionRL (X : Type) : @dPCP X ⪯ @PCPX X.
Proof. exists id; intro; now rewrite PCPX_iff_dPCP. Qed.