From SyntheticComputability Require Import ArithmeticalHierarchySemantic reductions SemiDec TuringJump OracleComputability Definitions StepIndex Limit simple.
Require Import SyntheticComputability.Synthetic.DecidabilityFacts.
Require Export SyntheticComputability.Shared.FinitenessFacts.
Require Export SyntheticComputability.Shared.Pigeonhole.
Require Export SyntheticComputability.Shared.ListAutomation.
Require Import Arith Arith.Compare_dec Lia Coq.Program.Equality List.
Require Import SyntheticComputability.PostsProblem.priority_method.
Require Import SyntheticComputability.PostsProblem.simple_extension.
(* ##################################### *)
Require Import SyntheticComputability.Synthetic.DecidabilityFacts.
Require Export SyntheticComputability.Shared.FinitenessFacts.
Require Export SyntheticComputability.Shared.Pigeonhole.
Require Export SyntheticComputability.Shared.ListAutomation.
Require Import Arith Arith.Compare_dec Lia Coq.Program.Equality List.
Require Import SyntheticComputability.PostsProblem.priority_method.
Require Import SyntheticComputability.PostsProblem.simple_extension.
(* ##################################### *)
(* ##################################### *)
Definition inf_exists (P: nat → Prop) := ∀ n, ∃ m, n ≤ m ∧ P m.
Notation "'∞∃' x .. y , p" :=
(inf_exists (λ x, .. (inf_exists (λ y, p)) ..))
(at level 200, x binder, right associativity,
format "'[' '∞∃' '/ ' x .. y , '/ ' p ']'")
: type_scope.
Notation "f ↓" := (f = Some ()) (at level 30).
Global Instance dec_le: ∀ m n, dec (m ≤ n).
Proof. intros n m; destruct (le_gt_dec n m); [by left|right; lia]. Qed.
Section Requirements_Lowness_Correctness.
Variable P: nat → Prop.
Variable f: nat → nat → bool.
Hypothesis S_P: stable_semi_decider P f.
Definition Φ_ := (Φ_ f).
Fact Φ_spec e x: Ξ e (char_rel P) x → ∞∀ n, Φ_ e x n ↓.
Proof. intro H. unfold Φ_. apply (Φ_spec S_P H). Qed.
Definition Ω e n := Φ_ e e n.
Section classic_logic.
Definition inf_exists (P: nat → Prop) := ∀ n, ∃ m, n ≤ m ∧ P m.
Notation "'∞∃' x .. y , p" :=
(inf_exists (λ x, .. (inf_exists (λ y, p)) ..))
(at level 200, x binder, right associativity,
format "'[' '∞∃' '/ ' x .. y , '/ ' p ']'")
: type_scope.
Notation "f ↓" := (f = Some ()) (at level 30).
Global Instance dec_le: ∀ m n, dec (m ≤ n).
Proof. intros n m; destruct (le_gt_dec n m); [by left|right; lia]. Qed.
Section Requirements_Lowness_Correctness.
Variable P: nat → Prop.
Variable f: nat → nat → bool.
Hypothesis S_P: stable_semi_decider P f.
Definition Φ_ := (Φ_ f).
Fact Φ_spec e x: Ξ e (char_rel P) x → ∞∀ n, Φ_ e x n ↓.
Proof. intro H. unfold Φ_. apply (Φ_spec S_P H). Qed.
Definition Ω e n := Φ_ e e n.
Section classic_logic.
Hypothesis N_requirements: ∀ e, (∞∃ n, Ω e n ↓) → Ξ e (char_rel P) e.
Definition limit_decider e n: bool := Dec (Ω e n ↓).
Section with_LEM_2.
Hypothesis LEM_Σ_2:
∀ (P: nat → nat → Prop), (∀ n m, dec (P n m)) → (∃ n, ∀ m, P n m) ∨ ¬ (∃ n, ∀ m, P n m).
Hypothesis LEM_Π_2:
∀ (P: nat → nat → Prop), (∀ n m, dec (P n m)) → (∀ n, ∃ m, P n m) ∨ ¬ (∀ n, ∃ m, P n m).
Lemma limit_case e: (∞∀ n, Ω e n ↓) ∨ (∞∀ n, ¬ Ω e n ↓).
Proof.
assert (∀ m n, dec (m ≤ n → ¬ Ω e n ↓)) as H by eauto.
destruct (LEM_Σ_2 H); first by right.
left. apply Φ_spec, N_requirements. intros i.
assert (∀ n, dec (n ≤ i ∧ Ω e n ↓)) as H'' by eauto.
destruct (@LEM_Σ_2 (λ n _, i ≤ n ∧ Ω e n ↓) ) as [[w Hw]|h1]; first eauto.
exists w; apply Hw; exact 42.
assert (∀ n, i ≤ n → ~ Ω e n ↓).
{ intros m Hm HM. eapply h1. exists m; eauto. }
exfalso. eapply H0. by exists i.
Qed.
Lemma Jump_limit : limit_computable (P´).
Proof.
exists limit_decider; split; intros.
- unfold J. split.
intros [w Hw]%Φ_spec; exists w; intros??.
apply Dec_auto. by eapply Hw.
intros [N HN]. eapply N_requirements.
intros m. exists (S N + m); split; first lia.
eapply Dec_true. eapply HN. lia.
- unfold J. split; intros H.
destruct (limit_case x) as [[k Hk]|h2].
enough (Ξ x (char_rel P) x) by easy.
eapply N_requirements. intros m. exists (S k + m).
split; first lia. eapply Hk. lia.
destruct h2 as [w Hw]. exists w.
intros. specialize (Hw n H0). unfold limit_decider.
destruct (Dec _); eauto.
destruct H as [w Hw].
intros [k Hneg]%Φ_spec.
set (N := S (max w k)).
assert (Ω x N ↓). { eapply Hneg. lia. }
enough (¬ Ω x N ↓) by eauto.
eapply Dec_false. eapply Hw. lia.
Qed.
End with_LEM_2.
Section with_LEM_1.
Hypothesis convergent: ∀ e, (∞∀ n, Ω e n ↓) ∨ (∞∀ n, ¬ Ω e n ↓).
Lemma Jump_limit_1 : limit_computable (P´).
Proof.
exists limit_decider; split; intros.
- unfold J. split.
intros [w Hw]%Φ_spec; exists w; intros??.
apply Dec_auto. by eapply Hw.
intros [N HN]. eapply N_requirements.
intros m. exists (S N + m); split; first lia.
eapply Dec_true. eapply HN. lia.
- unfold J. split; intros H.
destruct (convergent x) as [[k Hk]|h2].
enough (Ξ x (char_rel P) x) by easy.
eapply N_requirements. intros m. exists (S k + m).
split; first lia. eapply Hk. lia.
destruct h2 as [w Hw]. exists w.
intros. specialize (Hw n H0). unfold limit_decider.
destruct (Dec _); eauto.
destruct H as [w Hw].
intros [k Hneg]%Φ_spec.
set (N := S (max w k)).
assert (Ω x N ↓). { eapply Hneg. lia. }
enough (¬ Ω x N ↓) by eauto.
eapply Dec_false. eapply Hw. lia.
Qed.
End with_LEM_1.
End classic_logic.
(*
Section intuitionistic_logic.
Hypothesis N_requirements: ∀ e, (∞∃ n, Ω e n ↓) → ¬¬ Ξ e (char_rel P) e.
Lemma N_requirements': ∀ e, ¬¬ ((∞∃ n, Ω e n ↓) → Ξ e (char_rel P) e).
Proof. firstorder. Qed.
Fact dn_or (R Q: Prop): (¬¬ R ∨ ¬¬ Q) → ¬¬ (R ∨ Q).
Proof. firstorder. Qed.
Lemma not_not_limit_case e: ~ ~ ((∞∀ n, Ω e n ↓) ∨ (∞∀ n, ¬ Ω e n ↓)).
Proof.
ccase (∃ n, ∀ m, n ≤ m → ¬ Ω e m ↓) as H1|H1.
apply dn_or. { right. eauto. }
ccase (∀ i, ∃ n, i ≤ n ∧ Ω e n ↓) as H2|H2.
intros H_. apply (@N_requirements' e).
intros N_requirements'.
apply H_. left. apply Φ_spec, N_requirements'. intros i.
{ destruct (H2 i) as w Hw. exists w. apply Hw. }
exfalso. clear P S_P N_requirements.
apply H2. intros i.
Admitted.
Definition not_not_limit_computable {X} (P: X -> Prop) :=
exists f: X -> nat -> bool,
forall x, ~~
((P x <-> exists N, forall n, n >= N -> f x n = true) /\
(~ P x <-> exists N, forall n, n >= N -> f x n = false)).
Fact dn_and (R Q: Prop): (¬¬ R ∧ ¬¬ Q) → ¬¬ (R ∧ Q).
Proof. firstorder. Qed.
Lemma not_not_Jump_limit : not_not_limit_computable (P´).
Proof.
exists limit_decider; intro x.
apply dn_and.
split; intros.
- unfold J. intros H_.
eapply (@N_requirements' x). intros N_requirements'.
apply H_. split.
intros w HwΦ_spec.
set (N := S (max w k')).
assert (Ω x N ↓). { eapply Hneg. lia. }
enough (¬ Ω x N ↓) by eauto.
eapply Dec_false. eapply Hw. lia.
apply H_. split.
destruct h2 as w Hw. exists w.
intros. specialize (Hw n H0). unfold limit_decider.
destruct (Dec _); eauto.
intro H. destruct H as w Hw.
intros k Hneg*)
End Requirements_Lowness_Correctness.
Section Wall.
Instance wall_instance: Wall := λ e L n, φ (λ x, Dec (In x L)) e e n.
Definition P := P wall.
Definition P_func := P_func wall.
Instance E: Extension := simple_extension wall.
Fact P_semi_decidable: semi_decidable P.
Proof. eapply P_semi_decidable. Qed.
Definition χ := χ (simple_extension wall).
Definition P_Φ := (Φ_ χ).
Definition P_Ω := (Ω χ).
Section Verifiction.
Hypothesis Σ_1_lem: LEM_Σ 1.
Lemma attend_at_most_once_bound_constructive:
∀ k, ∃ s, ∀ e, e < k -> ∀ s', s < s' -> ~ attend wall e s'.
Proof. by apply attend_at_most_once_bound_test. Qed.
Lemma eventally_wall:
∀ e, (∞∀ s, ∀ x, extendP (P_func s) s x → wall e (P_func s) s < x).
Proof.
intros e.
destruct (@attend_at_most_once_bound_constructive (S e)) as [s Hs].
exists (S s). intros m Hm x [e_ [He_ He_']].
destruct (Dec (e_ < e)) as [E|E].
{ exfalso. enough (attend wall e_ m).
unshelve eapply (Hs e_ _ m); eauto; lia.
split; first lia. destruct He_' as [H _].
apply H. }
assert (e ≤ e_) by lia; clear E.
destruct He_', H1, H1, H1, H1, H3.
by eapply H5.
Qed.
Fact wall_convergence e : ∃ b : nat, lim_to wall (wall e) b.
Proof.
destruct (@eventally_wall e) as [N HN].
assert (∀ m, dec (wall e (P_func m) m = 0)) as HD by eauto.
assert (pdec (∀ x, N ≤ x → wall e (P_func x) x = 0)) as [H'|H'].
{ apply assume_Π_1_lem. apply Σ_1_lem. intros x. eauto. }
(* ccase (∀ x, N ≤ x → wall e (P_func x) x = 0) as H'|H'. *)
- exists 0. exists N. intros. by apply H'.
- enough (∃ x, N ≤ x ∧ wall e (P_func x) x ≠ 0) as H''.
clear H'. destruct H'' as [x [H1 H2]].
destruct (wall e (P_func x) x) as [|k] eqn: H; first done; clear H2.
exists (S k), x. intros t Ht. induction Ht; first done.
rewrite <- (@φ_spec1 χ _ _ _ _ IHHt).
reflexivity.
intros; split.
+ intros K%Dec_true. apply Dec_auto.
enough (incl (F_func (simple_extension wall) m) (F_func (simple_extension wall) (S m))).
eauto. eapply F_mono; [apply F_func_correctness|apply F_func_correctness|lia].
+ intros K%Dec_true. specialize (F_func_correctness (simple_extension wall) (S m)) as HE.
inv HE.
* assert (wall e (P_func m) m < a).
{ eapply HN. lia. enough (P_func m = l) as ->. apply H5.
eapply F_uni; [apply F_func_correctness|apply H4]. }
assert (wall e (P_func m) m = S k). { rewrite <-IHHt. reflexivity. }
rewrite H6 in H2. destruct (Dec (a = x0)).
lia. apply Dec_auto. rewrite <- H3 in K.
destruct K; first done.
enough ((F_func (simple_extension wall) m) = l) as -> by done.
eapply F_uni; last apply H4; apply F_func_correctness.
* apply Dec_auto.
enough (F_func (simple_extension wall) m = F_func (simple_extension wall) (S m)) as -> by eauto.
eapply F_uni; first apply F_func_correctness.
assumption.
+ eapply assume_Σ_1_dne. apply Σ_1_lem.
{ intro x. eauto. }
intro H. apply H'. intros x Hx.
assert (∀ n m: nat, ~~n=m → n=m).
{ intros n m Hnm. destruct (Dec (n=m)); eauto.
exfalso. by apply Hnm. }
apply H0. intros Hmn.
apply H. now exists x; split.
Qed.
Lemma N_requirements: ∀ e, (∞∃ n, P_Ω e n ↓) → Ξ e (char_rel P) e.
Proof.
intros e He.
destruct (@eventally_wall e) as [N HN].
destruct (@wall_convergence e) as [B [b Hb]].
set (M := max N b). destruct (He M) as [k [Hk Hk']].
eapply (@φ_spec χ e e k); first apply Hk'.
intros x Hx. unfold P, simple_extension.P.
rewrite F_with_top. split.
- intros (L & m & HL & HLs &HP).
assert (L = P_func m) as E. { eapply F_uni. apply HL. apply F_func_correctness. }
assert (x::L = P_func (S m)) as E'. { eapply F_uni. apply HLs. apply F_func_correctness. }
apply Dec_auto. destruct (Dec (S m ≤ k)) as [E_|E_].
enough (incl (P_func (S m)) (P_func k)). rewrite <-E' in H.
eauto. eapply F_mono; last apply E_; apply F_func_correctness.
assert (N ≤ m) as Em by lia. rewrite E in HP. specialize (HN m Em x HP).
assert (k ≤ m) as Ek by lia. enough (x ≤ φ (χ m) e e m).
exfalso. assert (φ (χ m) e e m < x).
apply HN. lia. enough (φ (χ m) e e m = φ (χ k) e e k) by congruence.
assert (φ (χ m) e e m = B).
{ rewrite <- (Hb m). reflexivity. lia. }
assert (φ (χ k) e e k = B).
{ rewrite <- (Hb k). reflexivity. lia. }
congruence.
- intros H%Dec_true.
eapply F_with_top. exists (F_func _ k), k; split; eauto.
eapply F_func_correctness.
Qed.
Lemma convergent e : (∞∀ n, P_Ω e n ↓) ∨ (∞∀ n, ¬ P_Ω e n ↓).
Proof.
destruct (@eventally_wall e) as [N HN].
assert (pdec (∃ k, N ≤ k ∧ P_Ω e k ↓)) as [[k [Hk HNk]]|H'] by (apply assume_Σ_1_lem; eauto).
- left. exists k. intros n Hm.
induction Hm; first done.
unfold P_Ω, Ω, Φ_ in *.
destruct (φ (χ m) e e m) eqn: E.
{ eapply φ_spec0' in E. congruence. }
(* Check φ_spec2. *)
eapply (@φ_spec2 χ _ ); eauto.
intros x Hx; split.
+ intros K%Dec_true. apply Dec_auto.
enough (incl (F_func (simple_extension wall) m) (F_func (simple_extension wall) (S m))).
eauto. eapply F_mono; [apply F_func_correctness|apply F_func_correctness|lia].
+ intros K%Dec_true. specialize (F_func_correctness (simple_extension wall) (S m)) as HE.
inv HE.
* assert (wall e (P_func m) m < a).
{ eapply HN. lia. enough (P_func m = l) as ->. apply H2.
eapply F_uni; [apply F_func_correctness|apply H1]. }
assert (wall e (P_func m) m = S n). { unfold wall, wall_instance.
rewrite <-E. reflexivity. }
rewrite H3 in H. destruct (Dec (a = x)).
lia. apply Dec_auto. rewrite <- H0 in K.
destruct K; first done.
enough ((F_func (simple_extension wall) m) = l) as -> by done.
eapply F_uni; last apply H1; apply F_func_correctness.
* apply Dec_auto.
enough (F_func (simple_extension wall) m = F_func (simple_extension wall) (S m)) as -> by eauto.
eapply F_uni; first apply F_func_correctness.
assumption.
- right. exists N. intros m Hm.
destruct (Dec (P_Ω e m ↓)); eauto.
Qed.
Fact P_simple: simple P.
Proof. eapply P_simple. intro e.
intros H. apply H. apply wall_convergence.
Qed.
Hypothesis Σ_2_LEM:
∀ (P: nat → nat → Prop),
(∀ n m, dec (P n m)) → (∃ n, ∀ m, P n m) ∨ ¬ (∃ n, ∀ m, P n m).
Fact jump_P_limit_test: limit_computable (P´).
Proof.
eapply Jump_limit; last done. apply F_with_χ.
intros e He. eapply N_requirements; eauto.
Qed.
End Verifiction.
Lemma eventally_wall_db e:
¬¬ (∞∀ s, ∀ x, extendP (P_func s) s x → wall e (P_func s) s < x).
Proof.
intros H_. eapply (@attend_at_most_once_bound wall (S e)).
intros [s Hs]. eapply H_; clear H_.
exists (S s). intros m Hm x [e_ [He_ He_']].
destruct (Dec (e_ < e)) as [E|E].
{ exfalso. enough (attend wall e_ m).
unshelve eapply (Hs e_ _ m); eauto; lia.
split; first lia. destruct He_' as [H _].
apply H. }
assert (e ≤ e_) by lia; clear E.
destruct He_', H1, H1, H1, H1, H3.
by eapply H5.
Qed.
Fact wall_convergence_db e : ¬¬ ∃ b : nat, lim_to wall (wall e) b.
Proof.
intros H_.
destruct (@eventally_wall_db e). intros [N HN].
assert (∀ m, dec (wall e (P_func m) m = 0)) as HD by eauto.
ccase (∀ x, N ≤ x → wall e (P_func x) x = 0) as [H'|H'].
- apply H_; clear H_. exists 0. exists N. intros. by apply H'.
- enough (~~∃ x, N ≤ x ∧ wall e (P_func x) x ≠ 0) as H__.
apply H__. intros H''.
clear H'. destruct H'' as [x [H1 H2]].
apply H_; clear H_.
destruct (wall e (P_func x) x) as [|k] eqn: H; first done; clear H2.
exists (S k), x. intros t Ht. induction Ht; first done.
rewrite <- (@φ_spec1 χ _ _ _ _ IHHt).
reflexivity.
intros; split.
+ intros K%Dec_true. apply Dec_auto.
enough (incl (F_func (simple_extension wall) m) (F_func (simple_extension wall) (S m))).
eauto. eapply F_mono; [apply F_func_correctness|apply F_func_correctness|lia].
+ intros K%Dec_true. specialize (F_func_correctness (simple_extension wall) (S m)) as HE.
inv HE.
* assert (wall e (P_func m) m < a).
{ eapply HN. lia. enough (P_func m = l) as ->. apply H5.
eapply F_uni; [apply F_func_correctness|apply H4]. }
assert (wall e (P_func m) m = S k). { rewrite <-IHHt. reflexivity. }
rewrite H6 in H2. destruct (Dec (a = x0)).
lia. apply Dec_auto. rewrite <- H3 in K.
destruct K; first done.
enough ((F_func (simple_extension wall) m) = l) as -> by done.
eapply F_uni; last apply H4; apply F_func_correctness.
* apply Dec_auto.
enough (F_func (simple_extension wall) m = F_func (simple_extension wall) (S m)) as -> by eauto.
eapply F_uni; first apply F_func_correctness.
assumption.
+ intro H.
apply H'. intros x Hx.
assert (∀ n m: nat, ~~n=m → n=m).
{ intros n m Hnm. destruct (Dec (n=m)); eauto.
exfalso. by apply Hnm. }
apply H0. intros Hmn.
apply H. now exists x; split.
Qed.
Lemma N_requirements_db: ∀ e, (∞∃ n, P_Ω e n ↓) → ¬ ¬ Ξ e (char_rel P) e.
Proof.
intros e He H_.
apply (@eventally_wall_db e). intros [N HN].
apply (@wall_convergence_db e). intros [B [b Hb]].
apply H_; clear H_.
set (M := max N b). destruct (He M) as [k [Hk Hk']].
eapply (@φ_spec χ e e k); first apply Hk'.
intros x Hx. unfold P, simple_extension.P.
rewrite F_with_top. split.
- intros (L & m & HL & HLs &HP).
assert (L = P_func m) as E. { eapply F_uni. apply HL. apply F_func_correctness. }
assert (x::L = P_func (S m)) as E'. { eapply F_uni. apply HLs. apply F_func_correctness. }
apply Dec_auto. destruct (Dec (S m ≤ k)) as [E_|E_].
enough (incl (P_func (S m)) (P_func k)). rewrite <-E' in H.
eauto. eapply F_mono; last apply E_; apply F_func_correctness.
assert (N ≤ m) as Em by lia. rewrite E in HP. specialize (HN m Em x HP).
assert (k ≤ m) as Ek by lia. enough (x ≤ φ (χ m) e e m).
exfalso. assert (φ (χ m) e e m < x).
apply HN. lia. enough (φ (χ m) e e m = φ (χ k) e e k) by congruence.
assert (φ (χ m) e e m = B).
{ rewrite <- (Hb m). reflexivity. lia. }
assert (φ (χ k) e e k = B).
{ rewrite <- (Hb k). reflexivity. lia. }
congruence.
- intros H%Dec_true.
eapply F_with_top. exists (F_func _ k), k; split; eauto.
eapply F_func_correctness.
Qed.
(* Should be enough if we use DNE_Σ_2 to drop out ¬¬ for both
eventally_wall and wall_convergence *)
Section with_LEM_2.
Hypothesis LEM_Σ_2:
∀ (P: nat → nat → Prop), (∀ n m, dec (P n m)) → (∃ n, ∀ m, P n m) ∨ ¬ (∃ n, ∀ m, P n m).
Hypothesis DN: ∀ P, ¬ ¬ P → P.
Fact jump_P_limit: limit_computable (P´).
Proof.
eapply Jump_limit; last done. apply F_with_χ.
intros e He. eapply DN, N_requirements_db; eauto.
Qed.
End with_LEM_2.
Section with_LEM_1.
Hypothesis LEM_Σ_1: LEM_Σ 1.
Fact jump_P_limit_2: limit_computable (P´).
Proof.
eapply Jump_limit_1; first apply F_with_χ.
- intros e He. eapply N_requirements; eauto.
- eapply convergent; eauto.
Qed.
End with_LEM_1.
End Wall.
(* Check jump_P_limit_2. *)