Require Import Lia Arith.
Require Import Undecidability.PCP.PCP.
Require Import Undecidability.PCP.Util.PCP_facts.
Require Import Undecidability.Synthetic.DecidabilityFacts.
From Undecidability Require Import FOL.FullSyntax.
From Undecidability Require FOL.Semantics.FiniteTarski.Fragment.
From Undecidability Require Import FOL.Undecidability.FSAT.
Require Import Undecidability.Shared.ListAutomation.
Import ListAutomationNotations.
Set Default Proof Using "Type".
Local Unset Strict Implicit.
Local Notation "| s |" := (length s) (at level 100).
Definition bstring n :=
{ s : string bool | | s | <= n}.
Lemma string_nil (s : string bool) :
|s| <= 0 <-> s = nil.
Proof.
destruct s; cbn.
- split; trivial; lia.
- split; try congruence. intros H. lia.
Qed.
Definition bnil n : bstring n := exist _ nil (Nat.le_0_l n).
Definition bcons n (b : bool) (H : bstring n) : bstring (S n) :=
match H with
exist _ bs Hs => exist _ (b::bs) (le_n_S (|bs|) n Hs) end.
Lemma bstring_eq n (s t : bstring n) :
proj1_sig s = proj1_sig t <-> s = t.
Proof.
split; try now intros ->.
destruct s as [s H1], t as [t H2]; cbn.
intros ->. now rewrite (le_unique _ _ H1 H2).
Qed.
Lemma bstring_eq' n (s t : bstring n) :
proj1_sig s = proj1_sig t -> s = t.
Proof.
apply bstring_eq.
Qed.
Definition bstring_step n (L : list (bstring n)) :=
[bnil (S n)] ++ map (bcons true) L ++ map (bcons false) L.
Definition bcast n s (H : |s| <= n) : bstring n :=
exist _ s H.
Lemma listable_bstring n :
listable (bstring n).
Proof.
induction n.
- exists [bnil 0]. intros [s H].
assert (s = nil) as -> by now apply string_nil.
left. now apply bstring_eq.
- destruct IHn as [L HL]. exists (bstring_step L).
intros [ [|[] s] H]; apply in_app_iff; cbn in H.
+ left. left. now apply bstring_eq.
+ right. apply in_app_iff. left. apply in_map_iff.
assert (H' : |s| <= n) by lia. exists (bcast H').
split; trivial. now apply bstring_eq.
+ right. apply in_app_iff. right. apply in_map_iff.
assert (H' : |s| <= n) by lia. exists (bcast H').
split; trivial. now apply bstring_eq.
Qed.
Notation i_f b x := (@i_func _ _ _ _ (f b) (Vector.cons _ x _ (Vector.nil _))).
Definition i_f' {domain:Type} {i:interp domain} (b:bool) (x:domain) := i_f b x.
Notation i_e := (@i_func _ _ _ _ e (Vector.nil _)).
Notation i_dum := (@i_func _ _ _ _ dum (Vector.nil _)).
Notation i_P x y := (@i_atom _ _ _ _ P (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Notation i_less x y := (@i_atom _ _ _ _ less (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Notation i_equiv x y := (@i_atom _ _ _ _ equiv (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Fixpoint iprep domain {I : interp domain} (x : list bool) (y : domain) :=
match x with
| nil => y
| b::x => i_f b (iprep x y)
end.
Definition ienc domain {I : interp domain} (x : list bool) := iprep x i_e.
Local Definition BSRS := list (card bool).
Local Notation "x / y" := (x, y).
Section FIB.
Variable R : BSRS.
Definition obstring n :=
option (bstring n).
Lemma listable_obstring n :
listable (obstring n).
Proof.
destruct (listable_bstring n) as [L HL]. exists (None :: map Some L).
intros [x|].
- right. apply in_map, HL.
- cbn. eauto.
Qed.
Notation obcast H := (Some (bcast H)).
Definition ccons n b (s : obstring n) : obstring n :=
match s with
| Some (exist _ s _) => match (le_dec (|b::s|) n) with
| left H => obcast H
| right _ => None
end
| None => None
end.
Definition cdrv n (s t : obstring n) :=
match s, t with
| Some (exist _ s _), Some (exist _ t _) => derivable R s t
| _, _ => False
end.
Definition sub n (x y : obstring n) :=
match x, y with
| Some (exist _ s _), Some (exist _ t _) => s <> t /\ exists s', t = s'++s
| _, _ => False
end.
Global Instance FIB n : interp (obstring n).
Proof using R.
split.
- intros k; cbn. destruct k as [b | |].
+ intros v. exact (ccons b (Vector.hd v)).
+ intros _. exact (Some (bnil n)).
+ intros _. exact None.
- intros k; cbn. destruct k.
+ intros v. exact (cdrv (Vector.hd v) (Vector.hd (Vector.tl v))).
+ intros v. exact (sub (Vector.hd v) (Vector.hd (Vector.tl v))).
+ intros v. exact (eq (Vector.hd v) (Vector.hd (Vector.tl v))).
Defined.
Lemma app_bound n (s t : string bool) :
|t| <= n -> |s++t| <= n + |s|.
Proof.
intros H. rewrite app_length. lia.
Qed.
Lemma obstring_iprep n x u (HX : |x++u| <= n) (HU : |u| <= n) :
iprep x (obcast HU) = obcast HX.
Proof.
induction x; cbn.
- f_equal. now apply bstring_eq.
- assert (H : |x++u| <= n).
{ rewrite app_length in *. cbn in HX. lia. }
rewrite (IHx H). unfold ccons, bcast at 1. destruct le_dec.
+ f_equal. now apply bstring_eq.
+ exfalso. cbn in *. rewrite app_length in *. lia.
Qed.
Lemma obstring_ienc n s (H : |s| <= n) :
ienc s = obcast H.
Proof.
unfold ienc. cbn.
setoid_rewrite obstring_iprep.
f_equal. apply bstring_eq, app_nil_r.
Unshelve. rewrite app_length. cbn. lia.
Qed.
Lemma obstring_ienc' n s (H : ~ |s| <= n) :
@ienc _ (FIB n) s = None.
Proof.
induction s; cbn in *; try lia.
change (@ccons n a (ienc s) = None).
destruct (le_dec (|s|) n) as [H'|H'].
- setoid_rewrite (obstring_ienc H'). cbn.
destruct le_dec; tauto.
- now rewrite IHs.
Qed.
Lemma crdv_iff n (x y : obstring n) :
i_P x y <-> exists s t, derivable R s t /\ x = ienc s /\ y = ienc t /\ |s| <= n /\ |t| <= n.
Proof.
destruct x as [ [x HX]|], y as [ [y HY]|]; split; cbn; auto.
{ intros H. exists x, y. repeat setoid_rewrite obstring_ienc. now repeat split. }
all: intros (s&t&H1&H2&H3&H4&H5). all: try unshelve setoid_rewrite obstring_ienc in H2; try unshelve setoid_rewrite obstring_ienc in H3; auto.
all: try discriminate.
revert H2 H3. now intros [= ->] [= ->].
Qed.
Definition obembed n (s : obstring n) : obstring (S n) :=
match s with
| Some (exist _ s H) => Some (exist _ s (le_S _ _ H))
| None => None
end.
Lemma cdrv_mon n (s t : obstring n) :
cdrv s t -> @cdrv (S n) (obembed s) (obembed t).
Proof.
now destruct s as [ [s HS]|], t as [ [t HT]|].
Qed.
Lemma cdrv_mon' n s t :
@cdrv n (ienc s) (ienc t) -> @cdrv (S n) (ienc s) (ienc t).
Proof.
destruct (le_dec (|s|) n) as [H|H], (le_dec (|t|) n) as [H'|H'].
- repeat unshelve setoid_rewrite obstring_ienc; trivial; lia.
- setoid_rewrite (obstring_ienc H). setoid_rewrite (obstring_ienc' H'). cbn. tauto.
- rewrite (obstring_ienc' H). cbn. tauto.
- rewrite (obstring_ienc' H). cbn. tauto.
Qed.
Lemma drv_cdrv s t :
derivable R s t <-> @cdrv (max (|s|) (|t|)) (ienc s) (ienc t).
Proof.
repeat unshelve setoid_rewrite obstring_ienc; try reflexivity; lia.
Qed.
Lemma drv_cdrv' s :
derivable R s s <-> @cdrv (|s|) (ienc s) (ienc s).
Proof.
repeat unshelve setoid_rewrite obstring_ienc; try reflexivity; lia.
Qed.
Lemma BPCP_P :
dPCPb R <-> exists n x, @i_atom _ _ _ (FIB n) P ((Vector.cons _ x _ (Vector.cons _ x _ (Vector.nil _)))).
Proof.
split.
- intros [s H]. exists (|s|), (ienc s). cbn. now apply drv_cdrv'.
- intros [n[ [ [s H]|] H'] ].
+ cbn in H'. now exists s.
+ destruct H'.
Qed.
Section Ax.
Variable n : nat.
Implicit Type x y : obstring n.
Lemma app_eq_nil' (s t : string bool) :
s = t++s -> t = nil.
Proof.
destruct t; trivial. intros H. exfalso.
assert (H' : |s| = |(b :: t) ++ s|) by now rewrite H at 1.
cbn in H'. rewrite app_length in H'. lia.
Qed.
Lemma app_neq b (s t : string bool) :
s <> (b :: t) ++ s.
Proof.
intros H. apply app_eq_nil' in H. discriminate.
Qed.
Lemma FIB_HP x y :
i_P x y -> x <> None /\ y <> None.
Proof.
destruct x as [ [s HS] |], y as [ [t HT]|]; auto.
intros _. split; discriminate.
Qed.
Lemma FIB_HS1 x :
~ sub x x.
Proof.
destruct x as [ [s HS]|]; cbn; firstorder.
Qed.
Lemma FIB_HS2 x y z :
sub x y -> sub y z -> sub x z.
Proof.
destruct x as [ [s HS]|], y as [ [t HT]|], z as [ [u HU]|]; cbn; auto.
intros [H1[s' HS'] ] [H2[t' HT'] ]. subst. split.
- rewrite app_assoc. intros H % app_eq_nil'.
apply app_eq_nil in H as [-> ->]. now apply H1.
- exists (t'++s'). apply app_assoc.
Qed.
Lemma FIB_HF1 b x :
i_f b x <> i_e.
Proof.
destruct x as [ [s H]|]; cbn; try congruence.
destruct le_dec; try congruence. injection. congruence.
Qed.
Lemma FIB_HF2 b1 b2 x y :
i_f b1 x <> None -> i_f b1 x = i_f b2 y -> x = y /\ b1 = b2.
Proof.
destruct x as [ [s HS] |], y as [ [t HT]|]; cbn.
all: repeat destruct le_dec; cbn. all: try congruence.
intros _ [= -> ->]. split; trivial. f_equal. now apply bstring_eq.
Qed.
Lemma None_dec X (x : option X) :
{x = None} + {x <> None}.
Proof.
destruct x; auto. right. discriminate.
Qed.
Lemma FIB_HF2' x y :
i_f true x = i_f false y -> i_f true x = None /\ i_f false y = None.
Proof.
intros H. destruct (None_dec (i_f' true x)), (None_dec (i_f' false y)); try tauto; exfalso. all: unfold i_f'.
- symmetry in H. specialize (FIB_HF2 n0 H). intros [H1 H2]; congruence.
- specialize (FIB_HF2 n0 H). intros [H1 H2]; congruence.
- specialize (FIB_HF2 n0 H). intros [_ H']. discriminate.
Qed.
Lemma FIB_HF3 b x :
i_f b x <> None -> x <> None.
Proof.
destruct x as [ [s HS] |]; cbn; congruence.
Qed.
Lemma FIB_HI x y :
i_P x y -> (exists s t, s/t el R /\ x = ienc s /\ y = ienc t)
\/ (exists s t u v, s/t el R /\ x = iprep s u /\ y = iprep t v /\ i_P u v /\
((sub u x /\ v = y) \/ (sub v y /\ u = x) \/ (sub u x /\ sub v y))).
Proof.
destruct x as [ [x HX]|], y as [ [y HY]|]; cbn; auto. induction 1.
- left. exists x, y. repeat setoid_rewrite obstring_ienc. repeat split; trivial.
- assert (HU : |u| <= n). { rewrite app_length in HX. lia. }
assert (HV : |v| <= n). { rewrite app_length in HY. lia. }
destruct x as [|b x], y as [|c y].
+ cbn. apply IHderivable.
+ right. exists [], (c::y), (obcast HU), (obcast HV).
repeat setoid_rewrite obstring_iprep. repeat split; trivial.
right. left. repeat split; eauto using app_neq. f_equal. now apply bstring_eq.
+ right. exists (b::x), [], (obcast HU), (obcast HV).
repeat setoid_rewrite obstring_iprep. repeat split; trivial.
left. repeat split; eauto using app_neq. f_equal. now apply bstring_eq.
+ right. exists (b::x), (c::y), (obcast HU), (obcast HV).
repeat setoid_rewrite obstring_iprep. repeat split; trivial.
right. right. repeat split; eauto using app_neq.
Qed.
End Ax.
End FIB.
Section Conv.
Variable R : BSRS.
Variable D : Type.
Hypothesis HD : listable D.
Variable I : interp D.
Notation "x == y" := (i_equiv x y) (at level 50).
Notation "x =/= y" := (~ (i_equiv x y)) (at level 50).
Hypothesis HP : forall x y, i_P x y -> x =/= i_dum /\ y =/= i_dum.
Hypothesis HS1 : forall x, ~ i_less x x.
Hypothesis HS2 : forall x y z, i_less x y -> i_less y z -> i_less x z.
Hypothesis HF1 : forall b x, i_f b x =/= i_e.
Hypothesis HF2 : forall b1 b2 x y, i_f b1 x =/= i_dum -> i_f b1 x == i_f b2 y -> x == y /\ b1 = b2.
Hypothesis HF3 : forall b x, i_f b x =/= i_dum -> x =/= i_dum.
Hypothesis HE1 : forall x, x == x.
Hypothesis HE2 : forall x y, x == y -> y == x.
Hypothesis HE3 : forall x y z, x == y -> y == z -> x == z.
Hypothesis HER1 : forall x y b, x == y -> i_f b x == i_f b y.
Hypothesis HER3 : forall x1 x2 y1 y2, x1 == x2 -> y1 == y2 -> i_less x1 y1 -> i_less x2 y2.
Hypothesis HI :
forall x y, i_P x y -> (exists s t, s/t el R /\ x == ienc s /\ y == ienc t)
\/ (exists s t u v, s/t el R /\ x == iprep s u /\ y == iprep t v /\ i_P u v /\
((i_less u x /\ v == y) \/ (i_less v y /\ u == x) \/ (i_less u x /\ i_less v y))).
Lemma ienc_inj s t :
ienc s =/= i_dum -> ienc s == ienc t -> s = t.
Proof using HF3 HF2 HF1 HE2.
revert t. induction s; intros [|]; cbn; trivial.
- intros _ H. apply HE2 in H. now apply HF1 in H.
- intros _ H. now apply HF1 in H.
- intros H [H' ->] % HF2; trivial. f_equal.
apply IHs; trivial. apply HF3 in H. trivial.
Qed.
Definition sub' L x y :=
i_less x y /\ x el L.
Lemma sub_acc_pred L x y :
i_less y x -> Acc (sub' L) x -> Acc (sub' L) y.
Proof using HS2.
intros H H'. constructor. intros z [H1 H2].
apply H'. split; trivial. now apply (HS2 H1).
Qed.
Lemma sub_acc_cons L x y :
Acc (sub' L) x -> ~ i_less y x -> Acc (sub' (y::L)) x.
Proof using HS2 HD.
induction 1 as [x HX IH]. intros H.
constructor. intros z [H1[->|H2] ].
- contradiction.
- apply IH. 1: now split.
intros HH. now eapply H, HS2 with z.
Qed.
Lemma sub_acc_cons' L x y :
i_less y x -> Acc (sub' L) x -> Acc (sub' (y::L)) y.
Proof using HS2 HS1 HD.
intros H1 H2. apply sub_acc_cons; trivial.
now apply (sub_acc_pred H1).
Qed.
Lemma sub_acc_step L a x :
Acc (sub' L) x -> Acc (sub' (a::L)) x.
Proof using HS2 HS1 HD.
induction 1 as [x HX IH].
constructor. intros y [H [->|H'] ].
- now apply (sub_acc_cons' H).
- apply IH. now split.
Qed.
Lemma sub_acc' L x :
Acc (sub' L) x.
Proof using HS2 HS1 HD.
induction L.
- constructor. intros y [_ [] ].
- apply sub_acc_step, IHL.
Qed.
Lemma sub_acc x :
Acc (fun a b => i_less a b) x.
Proof using HS2 HS1 HD.
destruct HD as [L HL].
induction (sub_acc' L x) as [x _ IH].
constructor. intros y H. now apply IH.
Qed.
Inductive psub : D -> D -> D -> D -> Prop :=
| psub1 x u y y' : i_less u x -> y == y' -> psub u y x y'
| psub2 y u x x' : i_less u y -> x == x' -> psub x u x' y
| psub3 x y u v : i_less u x -> i_less v y -> psub u v x y.
Lemma psub_equiv a b c d a' b' c' d' :
a == a' -> b == b' -> c == c' -> d == d' ->
psub a b c d -> psub a' b' c' d'.
Proof using HE2 HE3 HER3.
intros Ha Hb Hc Hd Habcd. induction Habcd as [c a b d Hac Hbd|d b a c Hdb Hac|c d a b Hac Hdb] in Ha,Hb,Hc,Hd,a',b',c',d'|-*.
+ eapply psub1.
- now eapply HER3 with a c.
- eapply HE3 with b. 1: now eapply HE2.
now eapply HE3 with d.
+ eapply psub2.
- now eapply HER3 with b d.
- eapply HE3 with a. 1: now eapply HE2.
now eapply HE3 with c.
+ eapply psub3.
- now eapply HER3 with a c.
- now eapply HER3 with b d.
Qed.
Definition psub' : D * D -> D * D -> Prop := fun P1 P2 => let (a,b) := P1 in let (c,d) := P2 in psub a b c d.
Definition pequiv : D * D -> D * D -> Prop := fun P1 P2 => let (a,b) := P1 in let (c,d) := P2 in a == c /\ b == d.
Lemma pequiv_equiv : RelationClasses.Equivalence pequiv.
Proof using HE1 HE2 HE3.
split.
- intros [x y]. split; now apply HE1.
- intros [x1 y1] [x2 y2] [H1 H2]; split; now apply HE2.
- intros [x1 y1] [x2 y2] [x3 y3] [Hx1 Hx2] [Hy1 Hy2]; split; [eapply HE3 with x2 | eapply HE3 with y2]; easy.
Qed.
Lemma psub_acc p :
Acc psub' p.
Proof using HS2 HS1 HD HI HE1 HE2 HE3 HER3.
destruct p as [x y]. revert y.
induction (sub_acc x) as [x HX IHX]. intros y.
induction (sub_acc y) as [y HY IHY]. constructor.
intros [u v]. cbn. inversion 1; subst.
- now apply IHX.
- eapply (Morphisms_Prop.Acc_pt_morphism pequiv) with (x, v).
+ apply pequiv_equiv.
+ intros [a b] [a' b'] [Ha Hb] [c d] [c' d'] [Hc Hd]. split; apply psub_equiv; (try easy); apply HE2; easy.
+ now split.
+ apply IHY. easy.
- now apply IHX.
Qed.
Lemma ienc_iprep s t :
iprep s (ienc t) == ienc (s ++ t).
Proof using HER1 HE3 HE1.
induction s; cbn; trivial. apply HER1. apply (HE3 IHs). apply HE1.
Qed.
Lemma iprep_respectful s t t' : t == t' -> iprep s t == iprep s t'.
Proof using HER1.
intros Ht. induction s.
- cbn. easy.
- cbn. apply HER1. easy.
Qed.
Lemma P_drv' p :
i_P (fst p) (snd p) -> exists s t, derivable R s t /\ fst p == ienc s /\ snd p == ienc t.
Proof using HS2 HS1 HI HD HE1 HE2 HE3 HER1 HER3.
intros H. induction (psub_acc p) as [ [x' y'] _ IH]; cbn in *.
destruct (HI H) as [(s&t&H1&H2&H3)|(s&t&u&v&H1&H2&H3&H4&H5)]; subst.
- exists s, t. repeat split; trivial. now constructor.
- destruct (IH (u,v)) as (s'&t'&H6&H7&H'); cbn in *; trivial; subst.
+ destruct H5 as [ [H5 H5r]|[ [H5 H5r]|[] ] ].
* now apply psub1.
* now apply psub2.
* now apply psub3.
+ exists (s++s'), (t++t'). repeat split. 1: now right.
* apply (HE3 H2). eapply HE3. 2: apply ienc_iprep. apply iprep_respectful. easy.
* apply (HE3 H3). eapply HE3. 2: apply ienc_iprep. apply iprep_respectful. easy.
Qed.
Lemma P_drv x y :
i_P x y -> exists s t, derivable R s t /\ x == ienc s /\ y == ienc t.
Proof using HS2 HS1 HI HD HE1 HE2 HE3 HER1 HER3.
apply P_drv' with (p:=(x,y)).
Qed.
Lemma P_BPCP x :
i_P x x -> dPCPb R.
Proof using HS2 HS1 HP HI HF3 HF2 HF1 HD HE1 HE2 HE3 HER1 HER3.
intros H. destruct (P_drv H) as (s&t&H1&H2&H3); subst.
assert (ienc s == ienc t) as H4.
- apply HE3 with x. now apply HE2. easy.
- apply ienc_inj in H4. exists t. congruence. destruct (@HP x x) as [Hx _]. 1:easy.
intros Hcc. apply Hx. now apply HE3 with (ienc s).
Qed.
End Conv.
Section Reduction.
Notation t_f b x := (func (f b) (Vector.cons _ x _ (Vector.nil _))).
Notation t_e :=
(func e (Vector.nil _)).
Notation t_dum :=
(func dum (Vector.nil _)).
Notation f_P x y := (atom P (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Notation f_less x y := (atom less (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Notation f_equiv x y := (atom equiv (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Notation "x ≡ y" := (f_equiv x y) (at level 20).
Notation "x ≢ y" := (¬ (x ≡ y)) (at level 20).
Notation "x ≺ y" := (f_less x y) (at level 20).
Fixpoint tprep (x : list bool) (y : term) :=
match x with
| nil => y
| b::x => t_f b (tprep x y)
end.
Lemma tprep_eval D (I : interp D) rho x t :
eval rho (tprep x t) = iprep x (eval rho t).
Proof.
induction x; cbn.
- reflexivity.
- rewrite IHx. reflexivity.
Qed.
Lemma tprep_bounded x t n : bounded_t n t -> bounded_t n (tprep x t).
Proof.
intros H; induction x; solve_bounds. 1: apply H.
apply IHx.
Qed.
Definition tenc (x : list bool) := tprep x t_e.
Definition ax_P := ∀ ∀ f_P $1 $0 → ($1 ≢ t_dum) ∧ ($0 ≢ t_dum).
Definition ax_S1 := ∀ ¬ ($0 ≺ $0).
Definition ax_S2 := ∀ ∀ ∀ $2 ≺ $1 → $1 ≺ $0 → $2 ≺ $0.
Definition ax_HF1_true := ∀ t_f true $0 ≢ t_e.
Definition ax_HF1_false := ∀ t_f false $0 ≢ t_e.
Definition ax_HF2_true := ∀ ∀ t_f true $1 ≢ t_dum → t_f true $1 ≡ t_f true $0 → $1 ≡ $0.
Definition ax_HF2_false := ∀ ∀ t_f false $1 ≢ t_dum → t_f false $1 ≡ t_f false $0 → $1 ≡ $0.
Definition ax_HF2 := ∀ ∀ t_f true $1 ≡ t_f false $0 → (t_f true $1 ≡ t_dum ∧ t_f false $0 ≡ t_dum).
Definition ax_HF3_true := ∀ t_f true $0 ≢ t_dum → $0 ≢ t_dum.
Definition ax_HF3_false := ∀ t_f false $0 ≢ t_dum → $0 ≢ t_dum.
Definition ax_HE1 := ∀ $0 ≡ $0.
Definition ax_HE2 := ∀ ∀ $1 ≡ $0 → $0 ≡ $1.
Definition ax_HE3 := ∀ ∀ ∀ $2 ≡ $1 → $1 ≡ $0 → $2 ≡ $0.
Definition ax_HER1_true := ∀ ∀ $1 ≡ $0 → t_f true $1 ≡ t_f true $0.
Definition ax_HER1_false := ∀ ∀ $1 ≡ $0 → t_f false $1 ≡ t_f false $0.
Definition ax_HER3 := ∀ ∀ ∀ ∀ $3 ≡ $2 → $1 ≡ $0 → f_less $3 $1 → f_less $2 $0.
Definition ax_HI' c :=
($1 ≡ tenc (fst c) ∧ $0 ≡ tenc (snd c))
∨ (∃ ∃ $3 ≡ tprep (fst c) $1 ∧ $2 ≡ tprep (snd c) $0 ∧ f_P $1 $0
∧ (($1 ≺ $3 ∧ $0 ≡ $2) ∨ ($0 ≺ $2 ∧ $1 ≡ $3) ∨ ($1 ≺ $3 ∧ $0 ≺ $2))).
Fixpoint list_or (A : list form) : form :=
match A with
| nil => ⊥
| phi::A => phi ∨ list_or A
end.
Lemma list_or_spec A D (I : interp D) rho :
rho ⊨ list_or A <-> exists phi, phi el A /\ rho ⊨ phi.
Proof.
induction A; cbn; split; auto.
- firstorder.
- intros [H|H].
+ exists a. tauto.
+ apply IHA in H as [phi[H1 H2]]. exists phi. tauto.
- intros [phi [[->|H1] H]]; auto.
right. apply IHA. now exists phi.
Qed.
Lemma list_or_closed n A : (forall a, In a A -> bounded n a) -> bounded n (list_or A).
Proof.
intros H. induction A; solve_bounds.
- apply H. now left.
- apply IHA. intros a' Ha. apply H. now right.
Qed.
Definition ax_HI (R : BSRS) := ∀ ∀ f_P $1 $0 → list_or (map ax_HI' R).
Definition finsat_formula (R : BSRS) :=
ax_P ∧ ax_S1 ∧ ax_S2 ∧ ax_HF1_true ∧ ax_HF1_false ∧ ax_HF2_true ∧ ax_HF2_false
∧ ax_HF2 ∧ ax_HF3_true ∧ ax_HF3_false ∧ ax_HI R
∧ ax_HE1 ∧ ax_HE2 ∧ ax_HE3 ∧ ax_HER1_true ∧ ax_HER1_false ∧ ax_HER3
∧ ∃ f_P $0 $0.
Lemma finsat_closed R : closed (finsat_formula R).
Proof.
unfold closed. solve_bounds.
apply list_or_closed.
intros a [x [<- Hx2]]%in_map_iff.
solve_bounds. all: apply tprep_bounded; solve_bounds.
Qed.
Ltac rsplit n := let rec f n := match n with 0 => idtac | S ?nn => split; [f nn|idtac] end in f n.
Lemma obstring_eqdec n : eq_dec (obstring n).
Proof.
apply option_eq_dec. unfold bstring.
intros [a Ha] [b Hb]. destruct (list_eq_dec bool_eq_dec a b) as [Hn0|Hn0].
- subst. left. apply EqdepFacts.eq_dep_eq_sig. assert (Ha = Hb) as -> by (apply le_unique). constructor.
- right. intros H. eapply Hn0, EqdepFacts.eq_sig_fst. exact H.
Defined.
Definition cdrv_decider (R : BSRS) (n : nat) (s t : obstring n) : dec (cdrv R s t).
Proof.
destruct s as [[s Hs]|], t as [[t Ht]|].
- cbn. apply pcp_hand_dec. apply bool_eq_dec.
- cbn. now right.
- cbn. now right.
- cbn. now right.
Defined.
Definition sub_decider (n : nat) (s t : obstring n) : dec (sub s t).
Proof.
destruct s as [[s Hs]|], t as [[t Ht]|].
- cbn. destruct (list_eq_dec bool_eq_dec s t) as [Hl|Hr].
+ right. intros [H _]. tauto.
+ destruct (is_a_tail_dec bool_eq_dec t s) as [Hl2|Hr2].
* left. split; try easy. destruct Hl2 as [x Hx]. exists x. congruence.
* right. intros [_ [x Hx]]. apply Hr2. exists x. congruence.
- cbn. now right.
- cbn. now right.
- cbn. now right.
Defined.
Lemma signature_is_decidable n R : (forall p : syms_pred, decidable (fun v : Vector.t (obstring n) (ar_preds p) => @i_atom _ _ (obstring n) (@FIB R n) p v)).
Proof.
intros [| |]; cbn.
- exists (fun X => if cdrv_decider R (Vector.hd X) (Vector.hd (Vector.tl X)) then true else false).
intros X. destruct (cdrv_decider R (Vector.hd X) (Vector.hd (Vector.tl X))) as [Ht|Hf]; now split.
- exists (fun X => if sub_decider (Vector.hd X) (Vector.hd (Vector.tl X)) then true else false).
intros X. destruct (sub_decider (Vector.hd X) (Vector.hd (Vector.tl X))) as [Ht|Hf]; now split.
- exists (fun X => if obstring_eqdec (Vector.hd X) (Vector.hd (Vector.tl X)) then true else false).
intros X. destruct (obstring_eqdec (Vector.hd X) (Vector.hd (Vector.tl X))) as [Ht|Hf]; now split.
Qed.
Theorem finsat_reduction_1 R :
dPCPb R -> FSATd (finsat_formula R).
Proof.
intros H.
- apply BPCP_P in H as [n [s H]]. exists (obstring n), (@FIB R n), (fun _ => None).
split; try apply listable_obstring. cbn.
split. 2:split. 2: apply signature_is_decidable.
1: {exists (fun '(a,b) => if obstring_eqdec a b then true else false).
intros [a b]. destruct (obstring_eqdec a b) as [Ht|Hf]; now split. }
rsplit 17.
+ apply (@FIB_HP R).
+ apply FIB_HS1.
+ apply FIB_HS2.
+ intros x. apply (@FIB_HF1 R _ true x).
+ intros x. apply (@FIB_HF1 R _ false x).
+ intros x y H1 H2. now destruct (FIB_HF2 (R:=R) H1 H2).
+ intros x y H1 H2. now destruct (FIB_HF2 (R:=R) H1 H2).
+ apply (@FIB_HF2' R).
+ intros x. apply (@FIB_HF3 R _ true x).
+ intros x. apply (@FIB_HF3 R _ false x).
+ intros u v [[a[b[H1 H2]]]|[a[b[a'[b'[H1 H2]]]]]] % (@FIB_HI R _ u v); apply list_or_spec.
* exists (ax_HI' (a/b)). split; try now apply in_map.
left. cbn. now rewrite !tprep_eval.
* exists (ax_HI' (a/b)). split; try now apply in_map.
right. exists a', b'. cbn. rewrite !tprep_eval. tauto.
+ congruence.
+ congruence.
+ congruence.
+ congruence.
+ congruence.
+ congruence.
+ try now exists s.
Qed.
Theorem finsat_reduction_2 R :
FSAT (finsat_formula R) -> dPCPb R.
Proof.
intros H.
- destruct H as (D & (I & rho & HF & HE & (((((((((((((((((H1 & H2) & H3) & H4) &
H5) & H6) & H7) & H8) & H9) & H10) & H11) & H12) & H13) & H14) & H15) & H16) & H17) & s & H18))).
cbn in *.
eapply P_BPCP with (x:=s); trivial; unfold not in *; cbn in *.
+ intros [|]. apply H4. apply H5.
+ intros [|] [|] d1 d2 Hi1 Hi2.
1: split; try easy; now apply H6.
3: split; try easy; now apply H7.
all: exfalso. 2: apply H13 in Hi2. all: destruct (H8 _ _ Hi2) as [Hi3 Hi4]. all:easy.
+ intros [|]. apply H9. apply H10.
+ intros d1 d2 [|]. apply H15. apply H16.
+ cbn in H11. intros x y H. specialize (H11 x y H).
apply list_or_spec in H11 as [c[[[u v][<- HR]] % in_map_iff [H'|[a[b H']]]]].
* left. exists u, v. split; trivial. cbn in H'. rewrite !tprep_eval in H'. apply H'.
* right. exists u, v, a, b. split; trivial. cbn in H'. rewrite !tprep_eval in H'. tauto.
Qed.
Theorem FSATd_reduction R :
dPCPb R <-> FSATd (finsat_formula R).
Proof.
split; intros H. 1: now apply finsat_reduction_1.
destruct H as (D & I & rho & Hlis & Hdis & HH).
apply finsat_reduction_2. exists D, I, rho. now split.
Qed.
Theorem FSAT_reduction R :
dPCPb R <-> FSAT (finsat_formula R).
Proof.
split; intros H. 2: now apply finsat_reduction_2.
destruct (finsat_reduction_1 H) as (D & I & rho & Hlis & Hdis & HH).
exists D, I, rho. now split.
Qed.
Theorem FSATdc_reduction R :
dPCPb R <-> FSATdc (exist _ (finsat_formula R) (finsat_closed R)).
Proof.
split; intros H. 1: now apply finsat_reduction_1.
destruct H as (D & I & rho & Hlis & Hdis & HH).
apply finsat_reduction_2. exists D, I, rho. now split.
Qed.
End Reduction.
Require Import Undecidability.PCP.PCP.
Require Import Undecidability.PCP.Util.PCP_facts.
Require Import Undecidability.Synthetic.DecidabilityFacts.
From Undecidability Require Import FOL.FullSyntax.
From Undecidability Require FOL.Semantics.FiniteTarski.Fragment.
From Undecidability Require Import FOL.Undecidability.FSAT.
Require Import Undecidability.Shared.ListAutomation.
Import ListAutomationNotations.
Set Default Proof Using "Type".
Local Unset Strict Implicit.
Local Notation "| s |" := (length s) (at level 100).
Definition bstring n :=
{ s : string bool | | s | <= n}.
Lemma string_nil (s : string bool) :
|s| <= 0 <-> s = nil.
Proof.
destruct s; cbn.
- split; trivial; lia.
- split; try congruence. intros H. lia.
Qed.
Definition bnil n : bstring n := exist _ nil (Nat.le_0_l n).
Definition bcons n (b : bool) (H : bstring n) : bstring (S n) :=
match H with
exist _ bs Hs => exist _ (b::bs) (le_n_S (|bs|) n Hs) end.
Lemma bstring_eq n (s t : bstring n) :
proj1_sig s = proj1_sig t <-> s = t.
Proof.
split; try now intros ->.
destruct s as [s H1], t as [t H2]; cbn.
intros ->. now rewrite (le_unique _ _ H1 H2).
Qed.
Lemma bstring_eq' n (s t : bstring n) :
proj1_sig s = proj1_sig t -> s = t.
Proof.
apply bstring_eq.
Qed.
Definition bstring_step n (L : list (bstring n)) :=
[bnil (S n)] ++ map (bcons true) L ++ map (bcons false) L.
Definition bcast n s (H : |s| <= n) : bstring n :=
exist _ s H.
Lemma listable_bstring n :
listable (bstring n).
Proof.
induction n.
- exists [bnil 0]. intros [s H].
assert (s = nil) as -> by now apply string_nil.
left. now apply bstring_eq.
- destruct IHn as [L HL]. exists (bstring_step L).
intros [ [|[] s] H]; apply in_app_iff; cbn in H.
+ left. left. now apply bstring_eq.
+ right. apply in_app_iff. left. apply in_map_iff.
assert (H' : |s| <= n) by lia. exists (bcast H').
split; trivial. now apply bstring_eq.
+ right. apply in_app_iff. right. apply in_map_iff.
assert (H' : |s| <= n) by lia. exists (bcast H').
split; trivial. now apply bstring_eq.
Qed.
Notation i_f b x := (@i_func _ _ _ _ (f b) (Vector.cons _ x _ (Vector.nil _))).
Definition i_f' {domain:Type} {i:interp domain} (b:bool) (x:domain) := i_f b x.
Notation i_e := (@i_func _ _ _ _ e (Vector.nil _)).
Notation i_dum := (@i_func _ _ _ _ dum (Vector.nil _)).
Notation i_P x y := (@i_atom _ _ _ _ P (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Notation i_less x y := (@i_atom _ _ _ _ less (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Notation i_equiv x y := (@i_atom _ _ _ _ equiv (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Fixpoint iprep domain {I : interp domain} (x : list bool) (y : domain) :=
match x with
| nil => y
| b::x => i_f b (iprep x y)
end.
Definition ienc domain {I : interp domain} (x : list bool) := iprep x i_e.
Local Definition BSRS := list (card bool).
Local Notation "x / y" := (x, y).
Section FIB.
Variable R : BSRS.
Definition obstring n :=
option (bstring n).
Lemma listable_obstring n :
listable (obstring n).
Proof.
destruct (listable_bstring n) as [L HL]. exists (None :: map Some L).
intros [x|].
- right. apply in_map, HL.
- cbn. eauto.
Qed.
Notation obcast H := (Some (bcast H)).
Definition ccons n b (s : obstring n) : obstring n :=
match s with
| Some (exist _ s _) => match (le_dec (|b::s|) n) with
| left H => obcast H
| right _ => None
end
| None => None
end.
Definition cdrv n (s t : obstring n) :=
match s, t with
| Some (exist _ s _), Some (exist _ t _) => derivable R s t
| _, _ => False
end.
Definition sub n (x y : obstring n) :=
match x, y with
| Some (exist _ s _), Some (exist _ t _) => s <> t /\ exists s', t = s'++s
| _, _ => False
end.
Global Instance FIB n : interp (obstring n).
Proof using R.
split.
- intros k; cbn. destruct k as [b | |].
+ intros v. exact (ccons b (Vector.hd v)).
+ intros _. exact (Some (bnil n)).
+ intros _. exact None.
- intros k; cbn. destruct k.
+ intros v. exact (cdrv (Vector.hd v) (Vector.hd (Vector.tl v))).
+ intros v. exact (sub (Vector.hd v) (Vector.hd (Vector.tl v))).
+ intros v. exact (eq (Vector.hd v) (Vector.hd (Vector.tl v))).
Defined.
Lemma app_bound n (s t : string bool) :
|t| <= n -> |s++t| <= n + |s|.
Proof.
intros H. rewrite app_length. lia.
Qed.
Lemma obstring_iprep n x u (HX : |x++u| <= n) (HU : |u| <= n) :
iprep x (obcast HU) = obcast HX.
Proof.
induction x; cbn.
- f_equal. now apply bstring_eq.
- assert (H : |x++u| <= n).
{ rewrite app_length in *. cbn in HX. lia. }
rewrite (IHx H). unfold ccons, bcast at 1. destruct le_dec.
+ f_equal. now apply bstring_eq.
+ exfalso. cbn in *. rewrite app_length in *. lia.
Qed.
Lemma obstring_ienc n s (H : |s| <= n) :
ienc s = obcast H.
Proof.
unfold ienc. cbn.
setoid_rewrite obstring_iprep.
f_equal. apply bstring_eq, app_nil_r.
Unshelve. rewrite app_length. cbn. lia.
Qed.
Lemma obstring_ienc' n s (H : ~ |s| <= n) :
@ienc _ (FIB n) s = None.
Proof.
induction s; cbn in *; try lia.
change (@ccons n a (ienc s) = None).
destruct (le_dec (|s|) n) as [H'|H'].
- setoid_rewrite (obstring_ienc H'). cbn.
destruct le_dec; tauto.
- now rewrite IHs.
Qed.
Lemma crdv_iff n (x y : obstring n) :
i_P x y <-> exists s t, derivable R s t /\ x = ienc s /\ y = ienc t /\ |s| <= n /\ |t| <= n.
Proof.
destruct x as [ [x HX]|], y as [ [y HY]|]; split; cbn; auto.
{ intros H. exists x, y. repeat setoid_rewrite obstring_ienc. now repeat split. }
all: intros (s&t&H1&H2&H3&H4&H5). all: try unshelve setoid_rewrite obstring_ienc in H2; try unshelve setoid_rewrite obstring_ienc in H3; auto.
all: try discriminate.
revert H2 H3. now intros [= ->] [= ->].
Qed.
Definition obembed n (s : obstring n) : obstring (S n) :=
match s with
| Some (exist _ s H) => Some (exist _ s (le_S _ _ H))
| None => None
end.
Lemma cdrv_mon n (s t : obstring n) :
cdrv s t -> @cdrv (S n) (obembed s) (obembed t).
Proof.
now destruct s as [ [s HS]|], t as [ [t HT]|].
Qed.
Lemma cdrv_mon' n s t :
@cdrv n (ienc s) (ienc t) -> @cdrv (S n) (ienc s) (ienc t).
Proof.
destruct (le_dec (|s|) n) as [H|H], (le_dec (|t|) n) as [H'|H'].
- repeat unshelve setoid_rewrite obstring_ienc; trivial; lia.
- setoid_rewrite (obstring_ienc H). setoid_rewrite (obstring_ienc' H'). cbn. tauto.
- rewrite (obstring_ienc' H). cbn. tauto.
- rewrite (obstring_ienc' H). cbn. tauto.
Qed.
Lemma drv_cdrv s t :
derivable R s t <-> @cdrv (max (|s|) (|t|)) (ienc s) (ienc t).
Proof.
repeat unshelve setoid_rewrite obstring_ienc; try reflexivity; lia.
Qed.
Lemma drv_cdrv' s :
derivable R s s <-> @cdrv (|s|) (ienc s) (ienc s).
Proof.
repeat unshelve setoid_rewrite obstring_ienc; try reflexivity; lia.
Qed.
Lemma BPCP_P :
dPCPb R <-> exists n x, @i_atom _ _ _ (FIB n) P ((Vector.cons _ x _ (Vector.cons _ x _ (Vector.nil _)))).
Proof.
split.
- intros [s H]. exists (|s|), (ienc s). cbn. now apply drv_cdrv'.
- intros [n[ [ [s H]|] H'] ].
+ cbn in H'. now exists s.
+ destruct H'.
Qed.
Section Ax.
Variable n : nat.
Implicit Type x y : obstring n.
Lemma app_eq_nil' (s t : string bool) :
s = t++s -> t = nil.
Proof.
destruct t; trivial. intros H. exfalso.
assert (H' : |s| = |(b :: t) ++ s|) by now rewrite H at 1.
cbn in H'. rewrite app_length in H'. lia.
Qed.
Lemma app_neq b (s t : string bool) :
s <> (b :: t) ++ s.
Proof.
intros H. apply app_eq_nil' in H. discriminate.
Qed.
Lemma FIB_HP x y :
i_P x y -> x <> None /\ y <> None.
Proof.
destruct x as [ [s HS] |], y as [ [t HT]|]; auto.
intros _. split; discriminate.
Qed.
Lemma FIB_HS1 x :
~ sub x x.
Proof.
destruct x as [ [s HS]|]; cbn; firstorder.
Qed.
Lemma FIB_HS2 x y z :
sub x y -> sub y z -> sub x z.
Proof.
destruct x as [ [s HS]|], y as [ [t HT]|], z as [ [u HU]|]; cbn; auto.
intros [H1[s' HS'] ] [H2[t' HT'] ]. subst. split.
- rewrite app_assoc. intros H % app_eq_nil'.
apply app_eq_nil in H as [-> ->]. now apply H1.
- exists (t'++s'). apply app_assoc.
Qed.
Lemma FIB_HF1 b x :
i_f b x <> i_e.
Proof.
destruct x as [ [s H]|]; cbn; try congruence.
destruct le_dec; try congruence. injection. congruence.
Qed.
Lemma FIB_HF2 b1 b2 x y :
i_f b1 x <> None -> i_f b1 x = i_f b2 y -> x = y /\ b1 = b2.
Proof.
destruct x as [ [s HS] |], y as [ [t HT]|]; cbn.
all: repeat destruct le_dec; cbn. all: try congruence.
intros _ [= -> ->]. split; trivial. f_equal. now apply bstring_eq.
Qed.
Lemma None_dec X (x : option X) :
{x = None} + {x <> None}.
Proof.
destruct x; auto. right. discriminate.
Qed.
Lemma FIB_HF2' x y :
i_f true x = i_f false y -> i_f true x = None /\ i_f false y = None.
Proof.
intros H. destruct (None_dec (i_f' true x)), (None_dec (i_f' false y)); try tauto; exfalso. all: unfold i_f'.
- symmetry in H. specialize (FIB_HF2 n0 H). intros [H1 H2]; congruence.
- specialize (FIB_HF2 n0 H). intros [H1 H2]; congruence.
- specialize (FIB_HF2 n0 H). intros [_ H']. discriminate.
Qed.
Lemma FIB_HF3 b x :
i_f b x <> None -> x <> None.
Proof.
destruct x as [ [s HS] |]; cbn; congruence.
Qed.
Lemma FIB_HI x y :
i_P x y -> (exists s t, s/t el R /\ x = ienc s /\ y = ienc t)
\/ (exists s t u v, s/t el R /\ x = iprep s u /\ y = iprep t v /\ i_P u v /\
((sub u x /\ v = y) \/ (sub v y /\ u = x) \/ (sub u x /\ sub v y))).
Proof.
destruct x as [ [x HX]|], y as [ [y HY]|]; cbn; auto. induction 1.
- left. exists x, y. repeat setoid_rewrite obstring_ienc. repeat split; trivial.
- assert (HU : |u| <= n). { rewrite app_length in HX. lia. }
assert (HV : |v| <= n). { rewrite app_length in HY. lia. }
destruct x as [|b x], y as [|c y].
+ cbn. apply IHderivable.
+ right. exists [], (c::y), (obcast HU), (obcast HV).
repeat setoid_rewrite obstring_iprep. repeat split; trivial.
right. left. repeat split; eauto using app_neq. f_equal. now apply bstring_eq.
+ right. exists (b::x), [], (obcast HU), (obcast HV).
repeat setoid_rewrite obstring_iprep. repeat split; trivial.
left. repeat split; eauto using app_neq. f_equal. now apply bstring_eq.
+ right. exists (b::x), (c::y), (obcast HU), (obcast HV).
repeat setoid_rewrite obstring_iprep. repeat split; trivial.
right. right. repeat split; eauto using app_neq.
Qed.
End Ax.
End FIB.
Section Conv.
Variable R : BSRS.
Variable D : Type.
Hypothesis HD : listable D.
Variable I : interp D.
Notation "x == y" := (i_equiv x y) (at level 50).
Notation "x =/= y" := (~ (i_equiv x y)) (at level 50).
Hypothesis HP : forall x y, i_P x y -> x =/= i_dum /\ y =/= i_dum.
Hypothesis HS1 : forall x, ~ i_less x x.
Hypothesis HS2 : forall x y z, i_less x y -> i_less y z -> i_less x z.
Hypothesis HF1 : forall b x, i_f b x =/= i_e.
Hypothesis HF2 : forall b1 b2 x y, i_f b1 x =/= i_dum -> i_f b1 x == i_f b2 y -> x == y /\ b1 = b2.
Hypothesis HF3 : forall b x, i_f b x =/= i_dum -> x =/= i_dum.
Hypothesis HE1 : forall x, x == x.
Hypothesis HE2 : forall x y, x == y -> y == x.
Hypothesis HE3 : forall x y z, x == y -> y == z -> x == z.
Hypothesis HER1 : forall x y b, x == y -> i_f b x == i_f b y.
Hypothesis HER3 : forall x1 x2 y1 y2, x1 == x2 -> y1 == y2 -> i_less x1 y1 -> i_less x2 y2.
Hypothesis HI :
forall x y, i_P x y -> (exists s t, s/t el R /\ x == ienc s /\ y == ienc t)
\/ (exists s t u v, s/t el R /\ x == iprep s u /\ y == iprep t v /\ i_P u v /\
((i_less u x /\ v == y) \/ (i_less v y /\ u == x) \/ (i_less u x /\ i_less v y))).
Lemma ienc_inj s t :
ienc s =/= i_dum -> ienc s == ienc t -> s = t.
Proof using HF3 HF2 HF1 HE2.
revert t. induction s; intros [|]; cbn; trivial.
- intros _ H. apply HE2 in H. now apply HF1 in H.
- intros _ H. now apply HF1 in H.
- intros H [H' ->] % HF2; trivial. f_equal.
apply IHs; trivial. apply HF3 in H. trivial.
Qed.
Definition sub' L x y :=
i_less x y /\ x el L.
Lemma sub_acc_pred L x y :
i_less y x -> Acc (sub' L) x -> Acc (sub' L) y.
Proof using HS2.
intros H H'. constructor. intros z [H1 H2].
apply H'. split; trivial. now apply (HS2 H1).
Qed.
Lemma sub_acc_cons L x y :
Acc (sub' L) x -> ~ i_less y x -> Acc (sub' (y::L)) x.
Proof using HS2 HD.
induction 1 as [x HX IH]. intros H.
constructor. intros z [H1[->|H2] ].
- contradiction.
- apply IH. 1: now split.
intros HH. now eapply H, HS2 with z.
Qed.
Lemma sub_acc_cons' L x y :
i_less y x -> Acc (sub' L) x -> Acc (sub' (y::L)) y.
Proof using HS2 HS1 HD.
intros H1 H2. apply sub_acc_cons; trivial.
now apply (sub_acc_pred H1).
Qed.
Lemma sub_acc_step L a x :
Acc (sub' L) x -> Acc (sub' (a::L)) x.
Proof using HS2 HS1 HD.
induction 1 as [x HX IH].
constructor. intros y [H [->|H'] ].
- now apply (sub_acc_cons' H).
- apply IH. now split.
Qed.
Lemma sub_acc' L x :
Acc (sub' L) x.
Proof using HS2 HS1 HD.
induction L.
- constructor. intros y [_ [] ].
- apply sub_acc_step, IHL.
Qed.
Lemma sub_acc x :
Acc (fun a b => i_less a b) x.
Proof using HS2 HS1 HD.
destruct HD as [L HL].
induction (sub_acc' L x) as [x _ IH].
constructor. intros y H. now apply IH.
Qed.
Inductive psub : D -> D -> D -> D -> Prop :=
| psub1 x u y y' : i_less u x -> y == y' -> psub u y x y'
| psub2 y u x x' : i_less u y -> x == x' -> psub x u x' y
| psub3 x y u v : i_less u x -> i_less v y -> psub u v x y.
Lemma psub_equiv a b c d a' b' c' d' :
a == a' -> b == b' -> c == c' -> d == d' ->
psub a b c d -> psub a' b' c' d'.
Proof using HE2 HE3 HER3.
intros Ha Hb Hc Hd Habcd. induction Habcd as [c a b d Hac Hbd|d b a c Hdb Hac|c d a b Hac Hdb] in Ha,Hb,Hc,Hd,a',b',c',d'|-*.
+ eapply psub1.
- now eapply HER3 with a c.
- eapply HE3 with b. 1: now eapply HE2.
now eapply HE3 with d.
+ eapply psub2.
- now eapply HER3 with b d.
- eapply HE3 with a. 1: now eapply HE2.
now eapply HE3 with c.
+ eapply psub3.
- now eapply HER3 with a c.
- now eapply HER3 with b d.
Qed.
Definition psub' : D * D -> D * D -> Prop := fun P1 P2 => let (a,b) := P1 in let (c,d) := P2 in psub a b c d.
Definition pequiv : D * D -> D * D -> Prop := fun P1 P2 => let (a,b) := P1 in let (c,d) := P2 in a == c /\ b == d.
Lemma pequiv_equiv : RelationClasses.Equivalence pequiv.
Proof using HE1 HE2 HE3.
split.
- intros [x y]. split; now apply HE1.
- intros [x1 y1] [x2 y2] [H1 H2]; split; now apply HE2.
- intros [x1 y1] [x2 y2] [x3 y3] [Hx1 Hx2] [Hy1 Hy2]; split; [eapply HE3 with x2 | eapply HE3 with y2]; easy.
Qed.
Lemma psub_acc p :
Acc psub' p.
Proof using HS2 HS1 HD HI HE1 HE2 HE3 HER3.
destruct p as [x y]. revert y.
induction (sub_acc x) as [x HX IHX]. intros y.
induction (sub_acc y) as [y HY IHY]. constructor.
intros [u v]. cbn. inversion 1; subst.
- now apply IHX.
- eapply (Morphisms_Prop.Acc_pt_morphism pequiv) with (x, v).
+ apply pequiv_equiv.
+ intros [a b] [a' b'] [Ha Hb] [c d] [c' d'] [Hc Hd]. split; apply psub_equiv; (try easy); apply HE2; easy.
+ now split.
+ apply IHY. easy.
- now apply IHX.
Qed.
Lemma ienc_iprep s t :
iprep s (ienc t) == ienc (s ++ t).
Proof using HER1 HE3 HE1.
induction s; cbn; trivial. apply HER1. apply (HE3 IHs). apply HE1.
Qed.
Lemma iprep_respectful s t t' : t == t' -> iprep s t == iprep s t'.
Proof using HER1.
intros Ht. induction s.
- cbn. easy.
- cbn. apply HER1. easy.
Qed.
Lemma P_drv' p :
i_P (fst p) (snd p) -> exists s t, derivable R s t /\ fst p == ienc s /\ snd p == ienc t.
Proof using HS2 HS1 HI HD HE1 HE2 HE3 HER1 HER3.
intros H. induction (psub_acc p) as [ [x' y'] _ IH]; cbn in *.
destruct (HI H) as [(s&t&H1&H2&H3)|(s&t&u&v&H1&H2&H3&H4&H5)]; subst.
- exists s, t. repeat split; trivial. now constructor.
- destruct (IH (u,v)) as (s'&t'&H6&H7&H'); cbn in *; trivial; subst.
+ destruct H5 as [ [H5 H5r]|[ [H5 H5r]|[] ] ].
* now apply psub1.
* now apply psub2.
* now apply psub3.
+ exists (s++s'), (t++t'). repeat split. 1: now right.
* apply (HE3 H2). eapply HE3. 2: apply ienc_iprep. apply iprep_respectful. easy.
* apply (HE3 H3). eapply HE3. 2: apply ienc_iprep. apply iprep_respectful. easy.
Qed.
Lemma P_drv x y :
i_P x y -> exists s t, derivable R s t /\ x == ienc s /\ y == ienc t.
Proof using HS2 HS1 HI HD HE1 HE2 HE3 HER1 HER3.
apply P_drv' with (p:=(x,y)).
Qed.
Lemma P_BPCP x :
i_P x x -> dPCPb R.
Proof using HS2 HS1 HP HI HF3 HF2 HF1 HD HE1 HE2 HE3 HER1 HER3.
intros H. destruct (P_drv H) as (s&t&H1&H2&H3); subst.
assert (ienc s == ienc t) as H4.
- apply HE3 with x. now apply HE2. easy.
- apply ienc_inj in H4. exists t. congruence. destruct (@HP x x) as [Hx _]. 1:easy.
intros Hcc. apply Hx. now apply HE3 with (ienc s).
Qed.
End Conv.
Section Reduction.
Notation t_f b x := (func (f b) (Vector.cons _ x _ (Vector.nil _))).
Notation t_e :=
(func e (Vector.nil _)).
Notation t_dum :=
(func dum (Vector.nil _)).
Notation f_P x y := (atom P (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Notation f_less x y := (atom less (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Notation f_equiv x y := (atom equiv (Vector.cons _ x _ (Vector.cons _ y _ (Vector.nil _)))).
Notation "x ≡ y" := (f_equiv x y) (at level 20).
Notation "x ≢ y" := (¬ (x ≡ y)) (at level 20).
Notation "x ≺ y" := (f_less x y) (at level 20).
Fixpoint tprep (x : list bool) (y : term) :=
match x with
| nil => y
| b::x => t_f b (tprep x y)
end.
Lemma tprep_eval D (I : interp D) rho x t :
eval rho (tprep x t) = iprep x (eval rho t).
Proof.
induction x; cbn.
- reflexivity.
- rewrite IHx. reflexivity.
Qed.
Lemma tprep_bounded x t n : bounded_t n t -> bounded_t n (tprep x t).
Proof.
intros H; induction x; solve_bounds. 1: apply H.
apply IHx.
Qed.
Definition tenc (x : list bool) := tprep x t_e.
Definition ax_P := ∀ ∀ f_P $1 $0 → ($1 ≢ t_dum) ∧ ($0 ≢ t_dum).
Definition ax_S1 := ∀ ¬ ($0 ≺ $0).
Definition ax_S2 := ∀ ∀ ∀ $2 ≺ $1 → $1 ≺ $0 → $2 ≺ $0.
Definition ax_HF1_true := ∀ t_f true $0 ≢ t_e.
Definition ax_HF1_false := ∀ t_f false $0 ≢ t_e.
Definition ax_HF2_true := ∀ ∀ t_f true $1 ≢ t_dum → t_f true $1 ≡ t_f true $0 → $1 ≡ $0.
Definition ax_HF2_false := ∀ ∀ t_f false $1 ≢ t_dum → t_f false $1 ≡ t_f false $0 → $1 ≡ $0.
Definition ax_HF2 := ∀ ∀ t_f true $1 ≡ t_f false $0 → (t_f true $1 ≡ t_dum ∧ t_f false $0 ≡ t_dum).
Definition ax_HF3_true := ∀ t_f true $0 ≢ t_dum → $0 ≢ t_dum.
Definition ax_HF3_false := ∀ t_f false $0 ≢ t_dum → $0 ≢ t_dum.
Definition ax_HE1 := ∀ $0 ≡ $0.
Definition ax_HE2 := ∀ ∀ $1 ≡ $0 → $0 ≡ $1.
Definition ax_HE3 := ∀ ∀ ∀ $2 ≡ $1 → $1 ≡ $0 → $2 ≡ $0.
Definition ax_HER1_true := ∀ ∀ $1 ≡ $0 → t_f true $1 ≡ t_f true $0.
Definition ax_HER1_false := ∀ ∀ $1 ≡ $0 → t_f false $1 ≡ t_f false $0.
Definition ax_HER3 := ∀ ∀ ∀ ∀ $3 ≡ $2 → $1 ≡ $0 → f_less $3 $1 → f_less $2 $0.
Definition ax_HI' c :=
($1 ≡ tenc (fst c) ∧ $0 ≡ tenc (snd c))
∨ (∃ ∃ $3 ≡ tprep (fst c) $1 ∧ $2 ≡ tprep (snd c) $0 ∧ f_P $1 $0
∧ (($1 ≺ $3 ∧ $0 ≡ $2) ∨ ($0 ≺ $2 ∧ $1 ≡ $3) ∨ ($1 ≺ $3 ∧ $0 ≺ $2))).
Fixpoint list_or (A : list form) : form :=
match A with
| nil => ⊥
| phi::A => phi ∨ list_or A
end.
Lemma list_or_spec A D (I : interp D) rho :
rho ⊨ list_or A <-> exists phi, phi el A /\ rho ⊨ phi.
Proof.
induction A; cbn; split; auto.
- firstorder.
- intros [H|H].
+ exists a. tauto.
+ apply IHA in H as [phi[H1 H2]]. exists phi. tauto.
- intros [phi [[->|H1] H]]; auto.
right. apply IHA. now exists phi.
Qed.
Lemma list_or_closed n A : (forall a, In a A -> bounded n a) -> bounded n (list_or A).
Proof.
intros H. induction A; solve_bounds.
- apply H. now left.
- apply IHA. intros a' Ha. apply H. now right.
Qed.
Definition ax_HI (R : BSRS) := ∀ ∀ f_P $1 $0 → list_or (map ax_HI' R).
Definition finsat_formula (R : BSRS) :=
ax_P ∧ ax_S1 ∧ ax_S2 ∧ ax_HF1_true ∧ ax_HF1_false ∧ ax_HF2_true ∧ ax_HF2_false
∧ ax_HF2 ∧ ax_HF3_true ∧ ax_HF3_false ∧ ax_HI R
∧ ax_HE1 ∧ ax_HE2 ∧ ax_HE3 ∧ ax_HER1_true ∧ ax_HER1_false ∧ ax_HER3
∧ ∃ f_P $0 $0.
Lemma finsat_closed R : closed (finsat_formula R).
Proof.
unfold closed. solve_bounds.
apply list_or_closed.
intros a [x [<- Hx2]]%in_map_iff.
solve_bounds. all: apply tprep_bounded; solve_bounds.
Qed.
Ltac rsplit n := let rec f n := match n with 0 => idtac | S ?nn => split; [f nn|idtac] end in f n.
Lemma obstring_eqdec n : eq_dec (obstring n).
Proof.
apply option_eq_dec. unfold bstring.
intros [a Ha] [b Hb]. destruct (list_eq_dec bool_eq_dec a b) as [Hn0|Hn0].
- subst. left. apply EqdepFacts.eq_dep_eq_sig. assert (Ha = Hb) as -> by (apply le_unique). constructor.
- right. intros H. eapply Hn0, EqdepFacts.eq_sig_fst. exact H.
Defined.
Definition cdrv_decider (R : BSRS) (n : nat) (s t : obstring n) : dec (cdrv R s t).
Proof.
destruct s as [[s Hs]|], t as [[t Ht]|].
- cbn. apply pcp_hand_dec. apply bool_eq_dec.
- cbn. now right.
- cbn. now right.
- cbn. now right.
Defined.
Definition sub_decider (n : nat) (s t : obstring n) : dec (sub s t).
Proof.
destruct s as [[s Hs]|], t as [[t Ht]|].
- cbn. destruct (list_eq_dec bool_eq_dec s t) as [Hl|Hr].
+ right. intros [H _]. tauto.
+ destruct (is_a_tail_dec bool_eq_dec t s) as [Hl2|Hr2].
* left. split; try easy. destruct Hl2 as [x Hx]. exists x. congruence.
* right. intros [_ [x Hx]]. apply Hr2. exists x. congruence.
- cbn. now right.
- cbn. now right.
- cbn. now right.
Defined.
Lemma signature_is_decidable n R : (forall p : syms_pred, decidable (fun v : Vector.t (obstring n) (ar_preds p) => @i_atom _ _ (obstring n) (@FIB R n) p v)).
Proof.
intros [| |]; cbn.
- exists (fun X => if cdrv_decider R (Vector.hd X) (Vector.hd (Vector.tl X)) then true else false).
intros X. destruct (cdrv_decider R (Vector.hd X) (Vector.hd (Vector.tl X))) as [Ht|Hf]; now split.
- exists (fun X => if sub_decider (Vector.hd X) (Vector.hd (Vector.tl X)) then true else false).
intros X. destruct (sub_decider (Vector.hd X) (Vector.hd (Vector.tl X))) as [Ht|Hf]; now split.
- exists (fun X => if obstring_eqdec (Vector.hd X) (Vector.hd (Vector.tl X)) then true else false).
intros X. destruct (obstring_eqdec (Vector.hd X) (Vector.hd (Vector.tl X))) as [Ht|Hf]; now split.
Qed.
Theorem finsat_reduction_1 R :
dPCPb R -> FSATd (finsat_formula R).
Proof.
intros H.
- apply BPCP_P in H as [n [s H]]. exists (obstring n), (@FIB R n), (fun _ => None).
split; try apply listable_obstring. cbn.
split. 2:split. 2: apply signature_is_decidable.
1: {exists (fun '(a,b) => if obstring_eqdec a b then true else false).
intros [a b]. destruct (obstring_eqdec a b) as [Ht|Hf]; now split. }
rsplit 17.
+ apply (@FIB_HP R).
+ apply FIB_HS1.
+ apply FIB_HS2.
+ intros x. apply (@FIB_HF1 R _ true x).
+ intros x. apply (@FIB_HF1 R _ false x).
+ intros x y H1 H2. now destruct (FIB_HF2 (R:=R) H1 H2).
+ intros x y H1 H2. now destruct (FIB_HF2 (R:=R) H1 H2).
+ apply (@FIB_HF2' R).
+ intros x. apply (@FIB_HF3 R _ true x).
+ intros x. apply (@FIB_HF3 R _ false x).
+ intros u v [[a[b[H1 H2]]]|[a[b[a'[b'[H1 H2]]]]]] % (@FIB_HI R _ u v); apply list_or_spec.
* exists (ax_HI' (a/b)). split; try now apply in_map.
left. cbn. now rewrite !tprep_eval.
* exists (ax_HI' (a/b)). split; try now apply in_map.
right. exists a', b'. cbn. rewrite !tprep_eval. tauto.
+ congruence.
+ congruence.
+ congruence.
+ congruence.
+ congruence.
+ congruence.
+ try now exists s.
Qed.
Theorem finsat_reduction_2 R :
FSAT (finsat_formula R) -> dPCPb R.
Proof.
intros H.
- destruct H as (D & (I & rho & HF & HE & (((((((((((((((((H1 & H2) & H3) & H4) &
H5) & H6) & H7) & H8) & H9) & H10) & H11) & H12) & H13) & H14) & H15) & H16) & H17) & s & H18))).
cbn in *.
eapply P_BPCP with (x:=s); trivial; unfold not in *; cbn in *.
+ intros [|]. apply H4. apply H5.
+ intros [|] [|] d1 d2 Hi1 Hi2.
1: split; try easy; now apply H6.
3: split; try easy; now apply H7.
all: exfalso. 2: apply H13 in Hi2. all: destruct (H8 _ _ Hi2) as [Hi3 Hi4]. all:easy.
+ intros [|]. apply H9. apply H10.
+ intros d1 d2 [|]. apply H15. apply H16.
+ cbn in H11. intros x y H. specialize (H11 x y H).
apply list_or_spec in H11 as [c[[[u v][<- HR]] % in_map_iff [H'|[a[b H']]]]].
* left. exists u, v. split; trivial. cbn in H'. rewrite !tprep_eval in H'. apply H'.
* right. exists u, v, a, b. split; trivial. cbn in H'. rewrite !tprep_eval in H'. tauto.
Qed.
Theorem FSATd_reduction R :
dPCPb R <-> FSATd (finsat_formula R).
Proof.
split; intros H. 1: now apply finsat_reduction_1.
destruct H as (D & I & rho & Hlis & Hdis & HH).
apply finsat_reduction_2. exists D, I, rho. now split.
Qed.
Theorem FSAT_reduction R :
dPCPb R <-> FSAT (finsat_formula R).
Proof.
split; intros H. 2: now apply finsat_reduction_2.
destruct (finsat_reduction_1 H) as (D & I & rho & Hlis & Hdis & HH).
exists D, I, rho. now split.
Qed.
Theorem FSATdc_reduction R :
dPCPb R <-> FSATdc (exist _ (finsat_formula R) (finsat_closed R)).
Proof.
split; intros H. 1: now apply finsat_reduction_1.
destruct H as (D & I & rho & Hlis & Hdis & HH).
apply finsat_reduction_2. exists D, I, rho. now split.
Qed.
End Reduction.