Small fixes (#3)

Author: yforster

README.md

@@ -24,6 +24,7 @@
   - [Synthetic Kolmogorov Complexity in Coq](https://drops.dagstuhl.de/opus/volltexte/2022/16721/) doi:[10.4230/LIPIcs.ITP.2022.12](https://doi.org/10.4230/LIPIcs.ITP.2022.12)
   - [Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-One and Truth-Table Reducibility in Coq](https://doi.org/10.4230/LIPIcs.CSL.2023.21) doi:[10.4230/LIPIcs.CSL.2023.21](https://doi.org/10.4230/LIPIcs.CSL.2023.21)
   - [A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl)](https://hal.inria.fr/hal-03891390/file/myhill-cantor-cpp23.pdf) doi:[10.1145/3573105.3575690](https://doi.org/10.1145/3573105.3575690)
+  - [Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions](https://arxiv.org/abs/2307.15543) doi:[10.48550/arXiv.2307.15543](https://doi.org/10.48550/arXiv.2307.15543)
 
 ## Description
 

theories/PostsTheorem/ArithmeticalHierarchySemantic.v

@@ -685,13 +685,50 @@ Section ArithmeticalHierarchySemantic.
     eapply H. now eapply isΣΠn_In_ΠΣSn.
   Qed.
 
-  Goal DNE_Π 1.
-  Proof.
-    intros k p H x. depelim H. depelim H.
-    cbn in *. rewrite H0. setoid_rewrite H.
-    firstorder. destruct (f (x0 :: x)) eqn:E; eauto.
-    contradiction H1. intros HE.
-    rewrite HE in E. congruence.
+  From SyntheticComputability Require Import principles.
+
+  Lemma level1 :
+    DNE_Σ 0
+    /\ (LEM_Σ 1 <-> LPO)
+    /\ (DNE_Σ 1 <-> MP)
+    /\ (LEM_Π 1 <-> WLPO)
+    /\ DNE_Π 1.
+  Proof.
+    repeat split.
+    - intros k p H v. depelim H. cbn in H.
+      rewrite H. destruct (f v); firstorder congruence.
+    - intros H f. destruct (H 0 (fun _ => exists n, f n = true)) as [ | ];
+        firstorder.
+      eapply (isΣsemS (p := fun v => f (Vector.hd v) = true)).
+      eapply isΠsem0. exact Vector.nil.
+    - intros H k p Hp v. depelim Hp. depelim H0.
+      cbn in *. rewrite H1. setoid_rewrite H0.
+      destruct (H (fun x => f (x :: v))); firstorder.
+    - intros H f. eapply (H 0 (fun _ => exists n, f n = true)).
+      eapply (isΣsemS (p := fun v => f (Vector.hd v) = true)).
+      eapply isΠsem0. exact Vector.nil.
+    - intros H k p Hp v. depelim Hp. depelim H0.
+      cbn in *. rewrite H1. setoid_rewrite H0.
+      eapply (H (fun x => f (x :: v))).
+    - intros H f. destruct (H 0 (fun _ => forall n, f n = false)) as [ | ];
+        firstorder.
+      eapply (isΠsemS (p := fun v => f (Vector.hd v) = false)).
+      eapply isΣsem0_ with (f := fun v => negb (f (Vector.hd v))).
+      intros. destruct (f (Vector.hd v)); cbn; firstorder congruence.
+      exact Vector.nil.
+    - intros H k p Hp v. depelim Hp. depelim H0.
+      cbn in *. rewrite H1. setoid_rewrite H0.
+      red in H. destruct (H (fun x => negb (f (x :: v)))).
+      + left. intros. specialize (H2 x).
+        destruct (f (x :: v)); cbn in *; congruence.
+      + right. intros ?. eapply H2. intros x.
+        specialize (H3 x).
+        destruct (f (x :: v)); cbn in *; congruence.
+    - intros k p H x. depelim H. depelim H.
+      cbn in *. rewrite H0. setoid_rewrite H.
+      firstorder. destruct (f (x0 :: x)) eqn:E; eauto.
+      contradiction H1. intros HE.
+      rewrite HE in E. congruence.
   Qed.
 
   Definition ArithmeticHierarchyNegation n :=

theories/PostsTheorem/TuringJump.v

@@ -308,6 +308,7 @@ Section jump.
       eapply not_semidecidable_compl_J; eassumption.
   Qed.
 
+  (** # <a id="J_self_J_m_red" /> #*)
   Lemma J_self_𝒥_m_red:
     forall Q, (J Q) ⪯ₘ (𝒥 Q).
   Proof.
@@ -380,10 +381,10 @@ Section jump.
 
   Notation "P ⪯ᴛ Q" := (red_Turing P Q) (at level 50).
 
-  Lemma red_T_imp_red_T_jumps  (P : nat -> Prop) (Q : nat -> Prop): 
-    P ⪯ᴛ Q -> (J P) ⪯ᴛ (J Q).
+  Lemma red_T_imp_red_m_jumps  (P : nat -> Prop) (Q : nat -> Prop): 
+    P ⪯ᴛ Q -> (J P) ⪯ₘ (J Q).
   Proof.
-    intros rT. apply red_m_impl_red_T, red_m_iff_semidec_jump.
+    intros rT. apply red_m_iff_semidec_jump.
     eapply Turing_transports_sdec; [apply semidecidable_J|apply rT].
   Qed.