Require Import List.
Import ListNotations.
Require Import Undecidability.PCP.PCP.
Require Import Undecidability.PCP.Util.Facts.
From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_tac utils_list utils_nat finite.
Require Import Coq.Init.Wf.
Import PCPListNotation.
Set Implicit Arguments.
Unset Strict Implicit.
Set Default Proof Using "Type".
Lemma tau1_app {X : Type} (A B: stack X) : tau1 (A ++ B) = tau1 A ++ tau1 B.
Proof.
induction A; cbn; auto. destruct a. rewrite <- app_assoc. congruence.
Qed.
Lemma tau2_app {X : Type} (A B: stack X) : tau2 (A ++ B) = tau2 A ++ tau2 B.
Proof.
induction A; cbn; auto. destruct a. rewrite <- app_assoc. congruence.
Qed.
Lemma tau1_inv (a : nat) B z :
tau1 B = a :: z ->
exists x y, (a :: x, y) el B.
Proof.
induction B; cbn; intros; inv H.
destruct a0 as ([],y).
- cbn in H1. firstorder.
- cbn in H1. inv H1. eauto.
Qed.
Lemma tau2_inv (a : nat) B z :
tau2 B = a :: z ->
exists x y, (y, a :: x) el B.
Proof.
induction B; cbn; intros; inv H.
destruct a0 as (x,[]).
- cbn in H1. firstorder.
- cbn in H1. inv H1. eauto.
Qed.
Definition cards {X : Type} (x: list X) := map (fun a => ([a], [a])) x.
Lemma tau1_cards {X : Type} (x: list X) : tau1 (cards x) = x.
Proof.
induction x; cbv in *; try rewrite IHx; trivial.
Qed.
Lemma tau2_cards {X : Type} (x: list X) : tau2 (cards x) = x.
Proof.
induction x; cbv in *; try rewrite IHx; trivial.
Qed.
Lemma itau1_app {X : Type} {P : stack X} A B : itau1 P (A++B) = itau1 P A ++ itau1 P B.
Proof. induction A; simpl; auto; rewrite app_ass; simpl; f_equal; auto. Qed.
Lemma itau2_app {X : Type} {P : stack X} A B : itau2 P (A++B) = itau2 P A ++ itau2 P B.
Proof. induction A; simpl; auto; rewrite app_ass; simpl; f_equal; auto. Qed.
Definition card_eq : forall x y : card bool, {x = y} + {x <> y}.
Proof.
intros. repeat decide equality.
Defined.
Global Hint Rewrite (@tau1_app nat) (@tau2_app nat) (@tau1_cards nat) (@tau2_cards nat) : list.
Fixpoint sym (R : stack nat) :=
match R with
[] => []
| (x, y) :: R => x ++ y ++ sym R
end.
Lemma sym_app P R :
sym (P ++ R) = sym P ++ sym R.
Proof.
induction P as [ | [] ]; eauto; cbn; rewrite IHP. now rewrite <- ? app_assoc.
Qed.
Lemma sym_map X (f : X -> card nat) l Sigma :
(forall x : X, x el l -> sym [f x] <<= Sigma) -> sym (map f l) <<= Sigma.
Proof.
intros. induction l as [ | ]; cbn in *.
- firstorder.
- pose proof (H a). destruct (f a). repeat eapply incl_app.
+ eapply app_incl_l, H0. eauto.
+ eapply app_incl_l, app_incl_R; eauto.
+ eauto.
Qed.
Lemma sym_word_l R u v :
(u, v) el R -> u <<= sym R.
Proof.
induction R; cbn; intros.
- tauto.
- destruct a as (u', v'). destruct H.
+ inv H. intros x Hx. eapply in_app_iff. now left.
+ intros x Hx. rewrite ? in_app_iff. right. right. now eapply IHR.
Qed.
Lemma sym_word_R R u v :
(u, v) el R -> v <<= sym R.
Proof.
induction R; cbn; intros.
- tauto.
- destruct a as (u', v'). destruct H.
+ inv H. intros x Hx. rewrite ? in_app_iff. right. now left.
+ intros x Hx. rewrite ? in_app_iff. right. right. now eapply IHR.
Qed.
#[export] Hint Resolve sym_word_l sym_word_R : core.
Lemma sym_mono A P :
A <<= P -> sym A <<= sym P.
Proof.
induction A as [ | (x,y) ]; cbn; intros.
- firstorder.
- eapply incl_app; try eapply incl_app.
+ eapply sym_word_l. eapply H. now left.
+ eapply sym_word_R. eapply H. now left.
+ eapply IHA. eapply cons_incl. eassumption.
Qed.
Lemma tau1_sym A : tau1 A <<= sym A.
Proof.
induction A as [ | (x & y) ].
- firstorder.
- cbn. intros ? [ | ] % in_app_iff. eapply in_app_iff. eauto.
rewrite !in_app_iff. eauto.
Qed.
Lemma tau2_sym A : tau2 A <<= sym A.
Proof.
induction A as [ | (x & y) ].
- firstorder.
- cbn. intros ? [ | ] % in_app_iff. rewrite ? in_app_iff. eauto.
rewrite !in_app_iff. eauto.
Qed.
Coercion sing (n : nat) := [n].
From Undecidability.Synthetic Require Import Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts.
From Undecidability Require Export PCP.PCP.
From Undecidability.Shared Require Export ListAutomation.
Import ListAutomationNotations.
Lemma stack_discrete :
discrete (stack bool).
Proof.
eapply discrete_iff; econstructor. intros ? ?. hnf. repeat decide equality.
Qed.
Lemma stack_enum :
enumerable__T (stack bool).
Proof.
unfold stack, card. eauto.
Qed.
Local Definition BSRS := list (card bool).
Local Notation "x / y" := (x, y).
Fixpoint L_PCP n : list (BSRS * (string bool * string bool)) :=
match n with
| 0 => []
| S n => L_PCP n
++ [ (C, (x, y)) | (C, x, y) ∈ (L_T BSRS n × L_T (string bool) n × L_T (string bool) n), (x/y) el C ]
++ [ (C, (x ++ u, y ++ v)) | ( (C, (u,v)), x, y) ∈ (L_PCP n × L_T (string bool) n × L_T (string bool) n), (x,y) el C ]
end.
Lemma enum_PCP' :
list_enumerator L_PCP (fun '(C, (u, v)) => @derivable bool C u v).
Proof.
intros ( C & u & v ). split.
+ induction 1.
* destruct (el_T C) as [m1], (el_T x) as [m2], (el_T y) as [m3].
exists (1 + m1 + m2 + m3). cbn. in_app 2.
in_collect (C, x, y); eapply cum_ge'; eauto; lia.
* destruct IHderivable as [m1], (el_T x) as [m2], (el_T y) as [m3].
exists (1 + m1 + m2 + m3). cbn. in_app 3.
in_collect ( (C, (u, v), x, y)); eapply cum_ge'; eauto; try lia.
+ intros [m]. revert C u v H. induction m; intros.
* inv H.
* cbn in H. inv_collect; inv H; eauto using der_sing, der_cons.
Qed.
Lemma enumerable_derivable : enumerable (fun '(C, (u, v)) => @derivable bool C u v).
Proof.
eapply list_enumerable_enumerable. eexists. eapply enum_PCP'.
Qed.
Lemma enumerable_PCP : enumerable dPCPb.
Proof.
pose proof enumerable_derivable.
assert (enumerable (X := (stack bool * (string bool * string bool))) (fun '(C, (s, t)) => s = t)). {
eapply dec_count_enum.
- eapply decidable_iff. econstructor. intros (? & ? & ?). exact _.
- eapply enum_enumT. econstructor. exact _.
}
unshelve epose proof (enumerable_conj _ _ _ _ H H0).
- eapply discrete_iff. econstructor. exact _.
- eapply projection in H1 as [f]. exists f.
unfold enumerator in *.
intros x. rewrite <- H1. intuition.
+ destruct H2 as [u]. exists (u,u). eauto.
+ destruct H2 as [[u v] [? ->]]. exists v. eauto.
Qed.
Section dec.
Variable (X : Type) (eqX_dec : forall x y : X, { x = y } + { x <> y }).
Fact is_a_head_dec (l t : list X) : { x : list X | l = t++x } + { ~ exists x : list X, l = t++x }.
Proof using eqX_dec.
revert t.
induction l as [ | a l IHl ].
+ intros [ | t ].
* left; exists nil; auto.
* right; intros ([ | ] & ?); discriminate.
+ intros [ | b t ].
* left; exists (a::l); auto.
* destruct (eqX_dec a b) as [ -> | C ].
- destruct (IHl t) as [ H | C ].
++ left; destruct H as (x & ->).
exists x; auto.
++ right; contradict C; destruct C as (x & E).
exists x; inversion E; subst; auto.
- right; contradict C; destruct C as (? & E); inversion E; auto.
Qed.
Fact is_a_tail_dec (l t : list X) : { exists x : list X, x++t = l } + { ~ exists x : list X, x++t = l }.
Proof using eqX_dec.
destruct (is_a_head_dec (rev l) (rev t)) as [ H | H ].
+ left; destruct H as (x & Hx).
exists (rev x).
apply f_equal with (f := @rev _) in Hx.
rewrite rev_app_distr in Hx.
do 2 rewrite rev_involutive in Hx; auto.
+ right; contradict H.
destruct H as (x & Hx); exists (rev x); subst.
apply rev_app_distr.
Qed.
End dec.
Notation "R ⊳ s ∕ t" := (derivable R s t) (at level 70, format "R ⊳ s ∕ t").
Section pcp_hand_dec.
Variable (X : Type) (lc : list (list X * list X)).
Notation pcp_hand := (fun s t => lc ⊳ s∕t).
Lemma pcp_hand_inv p q :
lc ⊳ p∕q -> In (p,q) lc
\/ exists x y p' q', In (x,y) lc /\ lc ⊳ p'∕q'
/\ p = x++p' /\ q = y++q'
/\ (x <> nil /\ y = nil
\/ x = nil /\ y <> nil
\/ x <> nil /\ y <> nil ).
Proof.
induction 1 as [ x y H | x y p q H1 H2 IH2 ].
+ left; auto.
+ destruct x as [ | a x ]; [ destruct y as [ | b y ] | ].
* simpl; auto.
* right; exists nil, (b::y), p, q; simpl; repeat split; auto.
right; left; split; auto; discriminate.
* right; exists (a::x), y, p, q; simpl; repeat split; auto.
destruct y.
- left; split; auto; discriminate.
- right; right; split; discriminate.
Qed.
Section pcp_induction.
Implicit Type (l m : list X).
Definition strict_suffix x y l m := { a : _ & { b | (a <> nil \/ b <> nil) /\ l = a++x /\ m = b++y } }.
Variable (P : list X -> list X -> Type)
(IHP : forall l m, (forall l' m', strict_suffix l' m' l m -> P l' m') -> P l m).
Theorem pcp_induction l m : P l m.
Proof using IHP.
induction on l m as IH with measure (length l + length m).
apply IHP.
intros l' m' (x & y & H & -> & ->).
apply IH.
do 2 rewrite app_length.
destruct x; destruct y; simpl; try lia.
destruct H as [ [] | [] ]; auto.
Qed.
End pcp_induction.
Section bounded_dec.
Variable eqX_dec : forall x y : X, { x = y } + { x <> y }.
Let eqlX_dec : forall l m : list X, { l = m } + { l <> m }.
Proof. apply list_eq_dec; auto. Qed.
Let eqXX_dec : forall p q : list X * list X, { p = q } + { p <> q }.
Proof. decide equality; auto. Qed.
Theorem pcp_hand_dec p q : { lc ⊳ p∕q } + { ~ lc ⊳ p∕q }.
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.
End bounded_dec.
End pcp_hand_dec.
Import ListNotations.
Require Import Undecidability.PCP.PCP.
Require Import Undecidability.PCP.Util.Facts.
From Undecidability.Shared.Libs.DLW.Utils
Require Import utils_tac utils_list utils_nat finite.
Require Import Coq.Init.Wf.
Import PCPListNotation.
Set Implicit Arguments.
Unset Strict Implicit.
Set Default Proof Using "Type".
Lemma tau1_app {X : Type} (A B: stack X) : tau1 (A ++ B) = tau1 A ++ tau1 B.
Proof.
induction A; cbn; auto. destruct a. rewrite <- app_assoc. congruence.
Qed.
Lemma tau2_app {X : Type} (A B: stack X) : tau2 (A ++ B) = tau2 A ++ tau2 B.
Proof.
induction A; cbn; auto. destruct a. rewrite <- app_assoc. congruence.
Qed.
Lemma tau1_inv (a : nat) B z :
tau1 B = a :: z ->
exists x y, (a :: x, y) el B.
Proof.
induction B; cbn; intros; inv H.
destruct a0 as ([],y).
- cbn in H1. firstorder.
- cbn in H1. inv H1. eauto.
Qed.
Lemma tau2_inv (a : nat) B z :
tau2 B = a :: z ->
exists x y, (y, a :: x) el B.
Proof.
induction B; cbn; intros; inv H.
destruct a0 as (x,[]).
- cbn in H1. firstorder.
- cbn in H1. inv H1. eauto.
Qed.
Definition cards {X : Type} (x: list X) := map (fun a => ([a], [a])) x.
Lemma tau1_cards {X : Type} (x: list X) : tau1 (cards x) = x.
Proof.
induction x; cbv in *; try rewrite IHx; trivial.
Qed.
Lemma tau2_cards {X : Type} (x: list X) : tau2 (cards x) = x.
Proof.
induction x; cbv in *; try rewrite IHx; trivial.
Qed.
Lemma itau1_app {X : Type} {P : stack X} A B : itau1 P (A++B) = itau1 P A ++ itau1 P B.
Proof. induction A; simpl; auto; rewrite app_ass; simpl; f_equal; auto. Qed.
Lemma itau2_app {X : Type} {P : stack X} A B : itau2 P (A++B) = itau2 P A ++ itau2 P B.
Proof. induction A; simpl; auto; rewrite app_ass; simpl; f_equal; auto. Qed.
Definition card_eq : forall x y : card bool, {x = y} + {x <> y}.
Proof.
intros. repeat decide equality.
Defined.
Global Hint Rewrite (@tau1_app nat) (@tau2_app nat) (@tau1_cards nat) (@tau2_cards nat) : list.
Fixpoint sym (R : stack nat) :=
match R with
[] => []
| (x, y) :: R => x ++ y ++ sym R
end.
Lemma sym_app P R :
sym (P ++ R) = sym P ++ sym R.
Proof.
induction P as [ | [] ]; eauto; cbn; rewrite IHP. now rewrite <- ? app_assoc.
Qed.
Lemma sym_map X (f : X -> card nat) l Sigma :
(forall x : X, x el l -> sym [f x] <<= Sigma) -> sym (map f l) <<= Sigma.
Proof.
intros. induction l as [ | ]; cbn in *.
- firstorder.
- pose proof (H a). destruct (f a). repeat eapply incl_app.
+ eapply app_incl_l, H0. eauto.
+ eapply app_incl_l, app_incl_R; eauto.
+ eauto.
Qed.
Lemma sym_word_l R u v :
(u, v) el R -> u <<= sym R.
Proof.
induction R; cbn; intros.
- tauto.
- destruct a as (u', v'). destruct H.
+ inv H. intros x Hx. eapply in_app_iff. now left.
+ intros x Hx. rewrite ? in_app_iff. right. right. now eapply IHR.
Qed.
Lemma sym_word_R R u v :
(u, v) el R -> v <<= sym R.
Proof.
induction R; cbn; intros.
- tauto.
- destruct a as (u', v'). destruct H.
+ inv H. intros x Hx. rewrite ? in_app_iff. right. now left.
+ intros x Hx. rewrite ? in_app_iff. right. right. now eapply IHR.
Qed.
#[export] Hint Resolve sym_word_l sym_word_R : core.
Lemma sym_mono A P :
A <<= P -> sym A <<= sym P.
Proof.
induction A as [ | (x,y) ]; cbn; intros.
- firstorder.
- eapply incl_app; try eapply incl_app.
+ eapply sym_word_l. eapply H. now left.
+ eapply sym_word_R. eapply H. now left.
+ eapply IHA. eapply cons_incl. eassumption.
Qed.
Lemma tau1_sym A : tau1 A <<= sym A.
Proof.
induction A as [ | (x & y) ].
- firstorder.
- cbn. intros ? [ | ] % in_app_iff. eapply in_app_iff. eauto.
rewrite !in_app_iff. eauto.
Qed.
Lemma tau2_sym A : tau2 A <<= sym A.
Proof.
induction A as [ | (x & y) ].
- firstorder.
- cbn. intros ? [ | ] % in_app_iff. rewrite ? in_app_iff. eauto.
rewrite !in_app_iff. eauto.
Qed.
Coercion sing (n : nat) := [n].
From Undecidability.Synthetic Require Import Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts.
From Undecidability Require Export PCP.PCP.
From Undecidability.Shared Require Export ListAutomation.
Import ListAutomationNotations.
Lemma stack_discrete :
discrete (stack bool).
Proof.
eapply discrete_iff; econstructor. intros ? ?. hnf. repeat decide equality.
Qed.
Lemma stack_enum :
enumerable__T (stack bool).
Proof.
unfold stack, card. eauto.
Qed.
Local Definition BSRS := list (card bool).
Local Notation "x / y" := (x, y).
Fixpoint L_PCP n : list (BSRS * (string bool * string bool)) :=
match n with
| 0 => []
| S n => L_PCP n
++ [ (C, (x, y)) | (C, x, y) ∈ (L_T BSRS n × L_T (string bool) n × L_T (string bool) n), (x/y) el C ]
++ [ (C, (x ++ u, y ++ v)) | ( (C, (u,v)), x, y) ∈ (L_PCP n × L_T (string bool) n × L_T (string bool) n), (x,y) el C ]
end.
Lemma enum_PCP' :
list_enumerator L_PCP (fun '(C, (u, v)) => @derivable bool C u v).
Proof.
intros ( C & u & v ). split.
+ induction 1.
* destruct (el_T C) as [m1], (el_T x) as [m2], (el_T y) as [m3].
exists (1 + m1 + m2 + m3). cbn. in_app 2.
in_collect (C, x, y); eapply cum_ge'; eauto; lia.
* destruct IHderivable as [m1], (el_T x) as [m2], (el_T y) as [m3].
exists (1 + m1 + m2 + m3). cbn. in_app 3.
in_collect ( (C, (u, v), x, y)); eapply cum_ge'; eauto; try lia.
+ intros [m]. revert C u v H. induction m; intros.
* inv H.
* cbn in H. inv_collect; inv H; eauto using der_sing, der_cons.
Qed.
Lemma enumerable_derivable : enumerable (fun '(C, (u, v)) => @derivable bool C u v).
Proof.
eapply list_enumerable_enumerable. eexists. eapply enum_PCP'.
Qed.
Lemma enumerable_PCP : enumerable dPCPb.
Proof.
pose proof enumerable_derivable.
assert (enumerable (X := (stack bool * (string bool * string bool))) (fun '(C, (s, t)) => s = t)). {
eapply dec_count_enum.
- eapply decidable_iff. econstructor. intros (? & ? & ?). exact _.
- eapply enum_enumT. econstructor. exact _.
}
unshelve epose proof (enumerable_conj _ _ _ _ H H0).
- eapply discrete_iff. econstructor. exact _.
- eapply projection in H1 as [f]. exists f.
unfold enumerator in *.
intros x. rewrite <- H1. intuition.
+ destruct H2 as [u]. exists (u,u). eauto.
+ destruct H2 as [[u v] [? ->]]. exists v. eauto.
Qed.
Section dec.
Variable (X : Type) (eqX_dec : forall x y : X, { x = y } + { x <> y }).
Fact is_a_head_dec (l t : list X) : { x : list X | l = t++x } + { ~ exists x : list X, l = t++x }.
Proof using eqX_dec.
revert t.
induction l as [ | a l IHl ].
+ intros [ | t ].
* left; exists nil; auto.
* right; intros ([ | ] & ?); discriminate.
+ intros [ | b t ].
* left; exists (a::l); auto.
* destruct (eqX_dec a b) as [ -> | C ].
- destruct (IHl t) as [ H | C ].
++ left; destruct H as (x & ->).
exists x; auto.
++ right; contradict C; destruct C as (x & E).
exists x; inversion E; subst; auto.
- right; contradict C; destruct C as (? & E); inversion E; auto.
Qed.
Fact is_a_tail_dec (l t : list X) : { exists x : list X, x++t = l } + { ~ exists x : list X, x++t = l }.
Proof using eqX_dec.
destruct (is_a_head_dec (rev l) (rev t)) as [ H | H ].
+ left; destruct H as (x & Hx).
exists (rev x).
apply f_equal with (f := @rev _) in Hx.
rewrite rev_app_distr in Hx.
do 2 rewrite rev_involutive in Hx; auto.
+ right; contradict H.
destruct H as (x & Hx); exists (rev x); subst.
apply rev_app_distr.
Qed.
End dec.
Notation "R ⊳ s ∕ t" := (derivable R s t) (at level 70, format "R ⊳ s ∕ t").
Section pcp_hand_dec.
Variable (X : Type) (lc : list (list X * list X)).
Notation pcp_hand := (fun s t => lc ⊳ s∕t).
Lemma pcp_hand_inv p q :
lc ⊳ p∕q -> In (p,q) lc
\/ exists x y p' q', In (x,y) lc /\ lc ⊳ p'∕q'
/\ p = x++p' /\ q = y++q'
/\ (x <> nil /\ y = nil
\/ x = nil /\ y <> nil
\/ x <> nil /\ y <> nil ).
Proof.
induction 1 as [ x y H | x y p q H1 H2 IH2 ].
+ left; auto.
+ destruct x as [ | a x ]; [ destruct y as [ | b y ] | ].
* simpl; auto.
* right; exists nil, (b::y), p, q; simpl; repeat split; auto.
right; left; split; auto; discriminate.
* right; exists (a::x), y, p, q; simpl; repeat split; auto.
destruct y.
- left; split; auto; discriminate.
- right; right; split; discriminate.
Qed.
Section pcp_induction.
Implicit Type (l m : list X).
Definition strict_suffix x y l m := { a : _ & { b | (a <> nil \/ b <> nil) /\ l = a++x /\ m = b++y } }.
Variable (P : list X -> list X -> Type)
(IHP : forall l m, (forall l' m', strict_suffix l' m' l m -> P l' m') -> P l m).
Theorem pcp_induction l m : P l m.
Proof using IHP.
induction on l m as IH with measure (length l + length m).
apply IHP.
intros l' m' (x & y & H & -> & ->).
apply IH.
do 2 rewrite app_length.
destruct x; destruct y; simpl; try lia.
destruct H as [ [] | [] ]; auto.
Qed.
End pcp_induction.
Section bounded_dec.
Variable eqX_dec : forall x y : X, { x = y } + { x <> y }.
Let eqlX_dec : forall l m : list X, { l = m } + { l <> m }.
Proof. apply list_eq_dec; auto. Qed.
Let eqXX_dec : forall p q : list X * list X, { p = q } + { p <> q }.
Proof. decide equality; auto. Qed.
Theorem pcp_hand_dec p q : { lc ⊳ p∕q } + { ~ lc ⊳ p∕q }.
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.
End bounded_dec.
End pcp_hand_dec.