From Undecidability.FOL Require Import MarkovPost.
From Undecidability.L Require Import Synthetic Lists LOptions Seval.
From Undecidability Require Import SR.SR_undec PCP.PCP_undec.
From Undecidability.Reductions Require Import L_to_mTM mTM_to_TM.
From Undecidability Require Import Reductions.PCPb_iff_BPCP.
Lemma MP_enum_stable_iff :
MP <-> (forall X (p : X -> Prop), enumerable p -> discrete X -> forall x, stable (p x)).
Proof.
split.
- intros MP X p [f Hf] [d Hd] x. eapply MP_to_decMP with (p := fun n => f n = Some x) in MP.
+ intros H. rewrite Hf in *. now eapply MP.
+ exists (fun n => match f n with Some x' => d (x, x') | _ => false end).
intros x0. destruct (f x0). rewrite <- (Hd (x,x1)). split. inversion 1. eauto. intros ->. eauto.
split; inversion 1.
- intros H f.
unshelve eapply (H unit (fun _ => exists n, f n = true) _ _ tt).
+ exists (fun n => if f n then Some tt else None).
intros []. split; intros [n Hn]; exists n; destruct (f n); congruence.
+ eapply decidable_iff. econstructor. intros []. red. decide equality.
Qed.
Definition MPL := forall s, stable (L.converges s).
Instance enumT_term : enumT term.
Proof.
exists (fix f n := match n with
| 0 => []
| S n => f n ++ [ var m | m ∈ L_T n]
++ [ lam s | s ∈ f n ]
++ [ app s t | (s,t) ∈ (f n × f n) ]
end).
- eauto.
- intros. induction x.
+ destruct (el_T n) as [m]. exists (S m). cbn. in_app 2.
in_collect n. eapply cum_ge'; eauto; omega.
+ destruct (IHx1) as [m1]. destruct (IHx2) as [m2].
exists (1 + m1 + m2). cbn. in_app 4.
in_collect (x1, x2). eapply cum_ge'; eauto; omega.
eapply cum_ge'; eauto; omega.
+ destruct (IHx) as [m1].
exists (1 + m1). cbn. in_app 3.
in_collect x. eapply cum_ge'; eauto; omega.
Qed.
Instance eq_dec_term : eq_dec L.term.
Proof.
intros ? ?. hnf. repeat decide equality.
Qed.
Instance help : forall n s, Prelim.dec (eva n s <> None).
Proof.
intros. eapply not_dec. eapply option_eq_dec. exact _.
Qed.
Fixpoint f n :=
match n with
| 0 => []
| S n => f n ++ [ s | (s, m) ∈ (@L_T _ enumT_term n × @L_T _ enumT_nat n), eva m s <> None ]
end.
Lemma converges_eva s : L.converges s <-> exists n, eva n s <> None.
Proof.
split.
- intros [t [n H % seval_eva] % eval_seval] % Eval.eval_converges. exists n. congruence.
- intros [n H]. destruct (eva n s) eqn:Ht; try congruence.
eapply eval_converges. eapply seval_eval. eapply eva_seval. eauto.
Qed.
Lemma enum_halt : enumerable L.converges.
Proof.
eapply enum_count with f. econstructor.
- eauto.
- intros s. split.
+ intros [n H] % converges_eva.
destruct (el_T n) as [m1], (el_T s) as [m2]. exists (1 + m1 + m2).
cbn. in_app 2. in_collect (s, n).
eapply cum_ge'; eauto; omega.
eapply cum_ge'; eauto; omega.
+ intros [m H]. induction m.
* inv H.
* cbn in *. inv_collect.
eapply converges_eva. eauto.
Qed.
Lemma MP_MPL :
MP -> MPL.
Proof.
intros. unfold MPL. intros. eapply MP_enum_stable.
- eassumption.
- eapply enum_halt.
- unfold discrete. eapply decidable_iff. econstructor.
intros []. hnf. repeat decide equality.
Qed.
Definition IP := forall (X : Prop) (P : nat -> Prop), (X -> exists n, P n) -> exists n, X -> P n.
Definition halting_dec := forall s, (L.converges s) \/ ~ (L.converges s).
Lemma MPL_independent : IP -> MPL -> halting_dec.
Proof.
intros H1 H2 s.
assert (exists n, forall k, eva k s <> None -> eva n s <> None) as [n Hn].
- specialize (H2 s). unfold stable in H2. rewrite converges_eva in H2. apply H1 in H2 as [n Hn].
exists n. intros k H. apply Hn. intros H'. apply H'. now exists k.
- destruct (eva n s) eqn : H.
+ left. eapply converges_eva. exists n. congruence.
+ right. intros [k Hk % Hn] % converges_eva. congruence.
Qed.
From Undecidability.FOLC Require Import Extend BPCP_CND LEnum.
Definition enumerable_sig (Sigma : Signature) := (enumT Funcs * enumT Preds) % type.
Definition discrete_sig (Sigma : Signature) := ((eq_dec Funcs) * (eq_dec Preds)) % type.
Definition cprv (a : {Sigma & (discrete_sig Sigma * enumerable_sig Sigma * {A : list form & {phi : form | List.Forall closed A /\ closed phi }})}%type) : Prop :=
let (Sigma, p) := a in let (_, s) := p in let (Gamma, s0) := s in let (phi, _) := s0 in Gamma ⊢CE phi.
Lemma halt_cprv :
L.converges ⪯ cprv.
Proof.
eapply reduces_transitive with (Q := cbvLambda.HaltL).
exists (fun s => s). firstorder. subst. unfold cbvLambda.HaltL.
exists (L.lam x1). rewrite H. econstructor. reflexivity. econstructor. reflexivity.
eapply reduces_transitive.
eapply HaltL_HaltTM.
eapply reduces_transitive.
eapply nTM_to_MTM.
eapply reduces_transitive.
eapply MTM_to_stM.
eapply reduces_transitive.
eapply Undecidability.PCP.PCP_undec.dPCPb_undec.
eapply reduces_transitive.
eapply PCPb_iff_dPCPb.reductionRL.
eapply reduces_transitive.
eapply reductionLR.
unshelve eexists.
- intros R. exists min_sig. split.
+ split.
* econstructor. exact _. exact _.
* econstructor.
-- exists (fun n => [t_f' true; t_f' false; t_e']). eauto.
intros. exists 0. destruct x; try destruct b; eauto.
-- exists (fun n => [BPCP_FOL.P; Q]). eauto.
intros. exists 0. destruct x; eauto.
+ exists []. exists (F R). split. econstructor.
now eapply closed_F.
- cbn. eapply BPCP_CND.
Qed.
Fact stable_red X Y (p : X -> Prop) (q : Y -> Prop) :
p ⪯ q -> (forall y, stable (q y)) -> (forall x, stable (p x)).
Proof.
intros [f H] H' x. unfold stable.
repeat rewrite H. apply H'.
Qed.
Corollary halt_cprv_stable :
(forall x, stable (cprv x)) -> MPL.
Proof.
unfold MPL. apply stable_red.
eapply halt_cprv.
Qed.
Definition iprv (a : {Sigma & (discrete_sig Sigma * enumerable_sig Sigma * {A : list form & {phi : form | List.Forall closed A /\ closed phi }})}%type) : Prop :=
let (Sigma, p) := a in let (_, s) := p in let (Gamma, s0) := s in let (phi, _) := s0 in @prv Sigma intu expl Gamma phi.
Lemma cprv_iprv :
cprv ⪯ iprv.
Proof.
unshelve eexists.
- intros (Sigma & [[H1 H2] (Gamma & phi & HGamma & Hphi)]).
exists Sigma. split. eauto.
exists (List.map dnt Gamma).
exists (dnt phi). split.
+ eapply Forall_forall.
rewrite Forall_forall in HGamma.
intros ? (? & <- & ?) % in_map_iff n.
eapply dnt_unused. eapply HGamma. eauto.
+ intros n. now eapply dnt_unused, Hphi.
- intros (Sigma & [[H1 H2] (Gamma & phi & HGamma & Hphi)]).
split.
eapply dnt_to_IE.
eapply dnt_to_CE.
Qed.
Corollary cprv_iprv_stable :
(forall x, stable (iprv x)) -> (forall x, stable (cprv x)).
Proof.
apply stable_red. eapply cprv_iprv.
Qed.
Require Import ConstructiveEpsilon.
Section enum_inj.
Variable (X : Type) (XD : eq_dec X) (H : enumT X).
Definition ofNat n :=
match R_nat_nat n with Some (n, m) => nthe n (L_T m) | None => None end.
Lemma ofNat_correct x :
exists n, ofNat n = Some x.
Proof.
destruct (el_T x) as [n Hn].
eapply In_nth_error in Hn as [m].
destruct (pairs_retract (m, n)) as [k].
exists k. unfold ofNat. now rewrite H1.
Qed.
Definition mu (p : nat -> Prop) :
(forall x, dec (p x)) -> ex p -> sig p.
Proof.
apply constructive_indefinite_ground_description_nat_Acc.
Defined.
Definition natinj x :=
proj1_sig (mu _ (ofNat_correct x)).
Lemma natinj_inj x y :
natinj x = natinj y -> x = y.
Proof.
unfold natinj.
destruct mu as [k Hk], mu as [l Hl].
cbn. congruence.
Qed.
Lemma ofnat_natinj x :
ofNat (natinj x) = Some x.
Proof.
unfold natinj. apply proj2_sig.
Qed.
End enum_inj.
Section inj_enum.
Variable Sigma : Signature.
Variable e : enumerable_sig Sigma.
Variable d : discrete_sig Sigma.
Definition inj : Signature_inj Sigma max.
Proof.
destruct e as [e1 e2], d as [d1 d2]. unshelve econstructor; cbn.
- exact (fun f => (natinj d1 e1 f, fun_ar f)).
- exact (fun p => ofNat e1 (fst p)).
- exact (fun P => (natinj d2 e2 P, pred_ar P)).
- exact (fun p => ofNat e2 (fst p)).
- apply ofnat_natinj.
- reflexivity.
- apply ofnat_natinj.
- reflexivity.
Qed.
End inj_enum.
Definition isprv (a : {Sigma & (discrete_sig Sigma * enumerable_sig Sigma * list form * form)%type }) := match a with (existT Sigma (H1, H2, Gamma, phi)) => @sprv Sigma expl Gamma None phi end.
Lemma iprv_maxprv :
iprv ⪯ (fun '(A, phi) => @prv max intu expl A phi).
Proof.
unshelve eexists.
- intros (Sigma & [[H1 H2] (Gamma & phi & HGamma & Hphi)]).
exact (List.map (embed (inj H2 H1)) Gamma, embed (inj H2 H1) phi).
- intros (Sigma & [[H1 H2] (Gamma & phi & HGamma & Hphi)]).
split; intros.
+ now eapply prv_embed.
+ eapply prv_back in H; eauto. eapply H1. eapply H1.
Qed.
Lemma maxprv_sprv :
(fun '(A, phi) => @prv max intu expl A phi) ⪯ (fun '(A,psi,phi) => @sprv max expl A psi phi).
Proof.
unshelve eexists.
- intros [A phi]. exact (A, None, phi).
- intros [A phi]. eapply sprv_prv_iff.
Qed.
Lemma sprv_sprvie :
(fun '(A,psi,phi) => @sprv max expl A psi phi) ⪯ (fun '(A, psi, phi) => sprvie A psi phi).
Proof.
unshelve eexists (fun '(A,psi,phi) => (List.map of_form A, option_map of_form psi, of_form phi)).
intros [[A psi] phi].
split.
- intros. now eapply prv_prvie.
- intros. now eapply prvie_prv.
Qed.
Lemma iprv_halt :
iprv ⪯ L.converges.
Proof.
eapply reduces_transitive. eapply iprv_maxprv.
eapply reduces_transitive. eapply maxprv_sprv.
eapply reduces_transitive. eapply sprv_sprvie.
eapply L_enumerable_halt.
- exists enum_eqb. split. econstructor. exact _.
intros [[[A psi] phi] [[A' psi'] phi']]. cbn.
unfold list_form_eqb, option_form_eqb.
destruct (list_eqb_spec form_eqb_spec A A'), (option_eqb_spec form_eqb_spec psi psi'), (form_eqb_spec phi phi'); subst.
all: split; intros; cbn in *; try firstorder congruence.
- eapply L_enumerable_enum.
exists L_sprvie. split. econstructor. exact _.
eapply enum_sprvie.
Qed.
Corollary iprv_halt_stable :
MPL -> (forall x, stable (iprv x)).
Proof.
unfold MPL. apply stable_red.
eapply iprv_halt.
Qed.