Require Import List.
Import ListNotations.
Definition string X := list X.
Definition card X : Type := list X * list X.
Definition stack X := list (card X).
Fixpoint tau1 {X : Type} (A : stack X) : string X :=
match A with
| [] => []
| (x, y) :: A => x ++ tau1 A
end.
Fixpoint tau2 {X : Type} (A : stack X) : string X :=
match A with
| [] => []
| (x, y) :: A => y ++ tau2 A
end.
Definition PCPX {X : Type}: stack X -> Prop :=
fun P => exists A, incl A P /\ A <> [] /\ tau1 A = tau2 A.
Definition PCP : stack nat -> Prop := @PCPX nat.
Definition PCPb : stack bool -> Prop := @PCPX bool.
Fixpoint itau1 {X : Type} (P : stack X) (A : list nat) : string X :=
match A with
| [] => []
| i :: A => fst (nth i P ([], [])) ++ itau1 P A
end.
Fixpoint itau2 {X : Type} (P : stack X) (A : list nat) : string X :=
match A with
| [] => []
| i :: A => snd (nth i P ([], [])) ++ itau2 P A
end.
Definition iPCPb : stack bool -> Prop :=
fun P => exists (A : list nat),
(forall a, In a A -> a < length P) /\ A <> [] /\ itau1 P A = itau2 P A.
Inductive derivable {X : Type} (P : stack X) : string X -> string X -> Prop :=
| der_sing x y : In (x, y) P -> derivable P x y
| der_cons x y u v : In (x, y) P -> derivable P u v -> derivable P (x ++ u) (y ++ v).
Definition dPCP {X : Type} : stack X -> Prop :=
fun P => exists u, @derivable X P u u.
Definition dPCPb : stack bool -> Prop := @dPCP bool.
Inductive BPCP (P : stack bool) : Prop :=
| cBPCP : forall u, derivable P u u -> BPCP P.
Hint Constructors BPCP : core.
Definition MPCP : card nat * stack nat -> Prop :=
fun '((x, y), P) => exists (A : stack nat),
incl A ((x, y) :: P) /\ x ++ tau1 A = y ++ tau2 A.
Definition MPCPb : card bool * stack bool -> Prop :=
fun '((x, y), P) => exists (A : stack bool),
incl A ((x, y) :: P) /\ x ++ tau1 A = y ++ tau2 A.