Kleene-Post and Post's theorem (#2)

Co-authored-by: dominik-kirst <[email protected]>

Author: yforster

README.md

@@ -37,14 +37,15 @@ This library contains results on synthetic computability theory.
 - A definition of oracle computability and Turing reducibility in `TuringReducibility/OracleComputability.v`
 - A proof of Post's theorem (`PT`) in `TuringReducibility/SemiDec.v`
 - A proof of Post's theorem about the arithmetical hierarchy in `PostsTheorem/PostsTheorem.v`
+- A proof of the Kleene-Post theorem in `PostsTheorem/KleenePostTheorem.v`
 
 ## Installation
 
 ```sh
 opam switch create coq-synthetic-computability --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda
 eval $(opam env)
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq.8.17 coq-stdpp.1.8.0
+opam install coq.8.17.0 coq-equations.1.3+8.17 coq-stdpp.1.8.0
 cd theories
 make
 make install

theories/ArithmeticHierarchy/ArithmeticalHierarchyEquiv.v

@@ -36,6 +36,7 @@ Section ArithmeticalHierarchyEquiv.
     - exfalso. inversion nQ.
   Qed.
 
+  (** # <a id="isSigmasyn_in_isSigmasem" /> #*)
   Lemma isΣnsyn_in_isΣsem:
     (forall n k (p: vec nat k -> Prop), isΣsyn n p -> isΣsem n p)
  /\ (forall n k (p: vec nat k -> Prop), isΠsyn n p -> isΠsem n p).
@@ -83,8 +84,10 @@ Section ArithmeticalHierarchyEquiv.
   (* Rückrichtung annehmen entscheidbar -> Δ1 *)
 
   Definition decΔ1syn := forall k (f: vec nat k -> bool), isΔsyn 1 (fun v => f v = true).
+  (** # <a id="decSigma1syn" /> #*)
   Definition decΣ1syn := forall k (f: vec nat k -> bool), isΣsyn 1 (fun v => f v = true).
 
+  (** # <a id="decSigma1syn_decDelta1syn" /> #*)
   Lemma decΣ1syn_decΔ1syn : decΣ1syn <-> decΔ1syn.
   Proof.
     unfold decΣ1syn, decΔ1syn.
@@ -95,6 +98,7 @@ Section ArithmeticalHierarchyEquiv.
     - intros H k f. apply H. 
   Qed.
 
+  (** # <a id="decSigma1syn_incl_1" /> #*)
   Lemma decΣ1syn_incl_1 :
     decΣ1syn <->
       (forall k (p : vec nat k -> Prop), isΣsem 1 p -> isΣsyn 1 p)
@@ -118,7 +122,8 @@ Section ArithmeticalHierarchyEquiv.
       intros H k f. apply H. apply isΣΠsem0.
     }
   Qed.
-  
+
+  (** # <a id="isSigmasem_in_isSigmasyn" /> #*)
   Lemma isΣsem_in_isΣsyn :
   decΣ1syn ->
     (forall n k (p: vec nat k -> Prop), isΣsem n p -> n <> 0 -> isΣsyn n p)

theories/Axioms/EPF.v

@@ -49,16 +49,19 @@ Proof.
     destruct seval; congruence.
 Qed.
 
+Import EmbedNatNotations.
+
 Lemma EPF_iff_nonparametric {Part : partiality} :
   EPF ↔ EPF_nonparam.    
 Proof.
   split.
   - intros [θ H]. exists θ. intros f. destruct (H (fun _ => f)) as [c Hc].
     exists (c 0). eapply Hc.
-  - intros [θ EPF]. exists (fun ic x => let (i, c) := unembed ic in θ c (embed (i, x))). intros f.
-    destruct (EPF (fun x => let (k, l) := unembed x in f k l)) as [c Hc].
-    exists (fun i => embed (i, c)). intros i x. rewrite embedP.
-    rewrite (Hc ⟨i,x⟩). rewrite embedP. reflexivity.
+  - intros [θ' EPF]. exists (fun! ⟨c, i⟩ => fun x => θ' c (embed (i, x))). intros f.
+    pose (g := (fun! ⟨i, x⟩ => f i x)).
+    destruct (EPF g) as [c Hc].
+    exists (fun i => ⟨c, i⟩). intros i x. rewrite embedP.
+    subst g. rewrite (Hc ⟨i,x⟩). rewrite embedP. reflexivity.
 Qed.
 
 Definition EPF_bool `{partiality} :=