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.