proposition: Theorem pcp_hand_dec p q : { lc ⊳ p∕q } + { ~ lc ⊳ p∕q }.
proof: Proof. Proof using eqlX_dec eqX_dec eqXX_dec. revert p q; apply pcp_induction; intros p q dec. set (P (c : list X * list X) := let (x,y) := c in exists d, p = x++fst d /\ q = y++snd d /\ pcp_hand (fst d) (snd d) /\ (x <> nil \/ y <> nil)). assert (forall c, { P c } + { ~ P c }) as Pdec. { intros (x,y); simpl. assert ( { x = nil /\ y = nil } + { x <> nil \/ y <> nil } ) as H. 1: { destruct (eqlX_dec x nil); destruct (eqlX_dec y nil); tauto. } destruct H as [ (H1 & H2) | Hxy ]. 1: { right; intros ((? & ?) & ?); tauto. } destruct (is_a_head_dec eqX_dec p x) as [ (p' & Hp') | Hp ]. 2: { right; contradict Hp; revert Hp. intros ((p',?) & E & _); exists p'; auto. } destruct (is_a_head_dec eqX_dec q y) as [ (q' & Hq') | Hq ]. 2: { right; contradict Hq; revert Hq. intros ((?,q') & _ & E & _); exists q'; auto. } destruct (dec p' q') as [ H' | H' ]. + exists x, y; auto. + left; exists (p',q'); auto. + right; contradict H'; revert H'. intros ((u,v) & -> & -> & C & _); simpl in *. apply app_inv_head in Hp'. apply app_inv_head in Hq'. subst; auto. } destruct list_dec with (1 := Pdec) (l := lc) as [ ((x,y) & H1 & H) | H ]; unfold P in H. + left. destruct H as ((p',q') & -> & -> & H & _); simpl in *. constructor 2; auto. + destruct In_dec with (1 := eqXX_dec) (a := (p,q)) (l := lc) as [ H2 | H2 ]. * left; constructor 1; auto. * right; contradict H2. apply pcp_hand_inv in H2. destruct H2 as [ | (x & y & p' & q' & H2 & H3 & -> & -> & H4) ]; auto. destruct H with (1 := H2). exists (p', q'); msplit 3; tauto. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts MoreEnumerabilityFacts ListEnumerabilityFacts) Coq.Init.Wf Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite)