Several problems on sequences of nats or Booleans

theories/MuRec/RA_UNIV_HALT.v

@@ -19,23 +19,55 @@ Set Implicit Arguments.
 
 Local Notation "'⟦' f '⟧'" := (@ra_rel _ f) (at level 0).
 
+(* We build a primitive µ-recursive algorithm
+
+     ra_pr_univ : recalg 2
+
+   with two argument (n##k##ø)
+     - n encodes a finitary valuation nat -> nat
+     - k encodes a finite list of H10C constraints
+
+   1) ra_pr_univ always terminates (it is primitive recursive)
+   2) ra_pr_univ outputs 0 iff the valuation n solves the equations k
+
+*)
+
+Definition ra_pr_univ := ra_h10c_eval.
+
+Theorem ra_pr_univ_pr : prim_rec ra_pr_univ.
+Proof. apply ra_h10c_eval_pr. Qed.
+
+Definition PRIMEREC_UNIV_PROBLEM := nat.
+Definition PRIMEREC_UNIV_MEETS_ZERO (n : PRIMEREC_UNIV_PROBLEM) := exists k, ⟦ra_pr_univ⟧ (k##n##vec_nil) 0.
+
 (* We build a universal µ-recusive algorithm of size 8708
 
       ra_univ : recalg 1
 
     which is just a particular µ-recursive algorithm. It is
     universal w.r.t. elementary Diophantine constraints 
-    as established in Reductions/H10C_RA_UNIV.v
+    as established in Reductions/H10C_SAT_to_RA_UNIV_HALT.v
 
     Basically, its termination predicate RA_UNIV_HALT 
     can simulate the solvability of any list of elementary 
     Diophantine constraints, making it undecidable *)
 
+Definition ra_univ := ra_min_univ ra_pr_univ.
+
+Definition RA_UNIV_PROBLEM := nat.
+Definition RA_UNIV_HALT (n : RA_UNIV_PROBLEM) : Prop := ex (⟦ra_univ⟧ (n##vec_nil)).
+Definition RA_UNIV_AD_HALT (n : RA_UNIV_PROBLEM) : Prop := ex (⟦ra_univ_ad⟧ (n##vec_nil)).
+
 (* Check ra_size ra_univ. *)
 (* Eval compute in ra_size ra_univ. *)
 (* Check ra_size ra_univ_ad. *)
 (* Eval compute in ra_size ra_univ_ad. *)
 
-Definition RA_UNIV_PROBLEM := nat.
-Definition RA_UNIV_HALT (n : RA_UNIV_PROBLEM) : Prop := ex (⟦ra_univ⟧ (n##vec_nil)).
-Definition RA_UNIV_AD_HALT (n : RA_UNIV_PROBLEM) : Prop := ex (⟦ra_univ_ad⟧ (n##vec_nil)).
+Definition PRIMESEQ_PROBLEM := { f : recalg 1 | prim_rec f }.
+Definition PRIMESEQ_MEETS_ZERO (P : PRIMESEQ_PROBLEM) := exists n, ⟦proj1_sig P⟧ (n##vec_nil) 0.
+
+Definition NATSEQ_PROBLEM := nat -> nat.
+Definition NATSEQ_MEETS_ZERO (f : NATSEQ_PROBLEM) : Prop := exists n, f n = 0.
+
+Definition BOOLSEQ_PROBLEM := nat -> bool.
+Definition BOOLSEQ_MEETS_TRUE (f : BOOLSEQ_PROBLEM) : Prop := exists n, f n = true.

theories/MuRec/RA_UNIV_HALT_undec.v

@@ -7,14 +7,60 @@ Require Import Undecidability.Synthetic.Undecidability.
 
 Require Import Undecidability.MuRec.RA_UNIV_HALT.
 
-Require Undecidability.MuRec.Reductions.H10C_SAT_to_RA_UNIV_HALT.
+Require Import Undecidability.MuRec.Reductions.H10C_SAT_to_RA_UNIV_HALT.
 Require Import Undecidability.DiophantineConstraints.H10C_undec.
 
 (* Undecidability of Universal µ-recusive Algorithm Halting *)
-Theorem RA_UNIV_HALT_undec : undecidable RA_UNIV_HALT.
+
+Theorem PRIMEREC_UNIV_MEETS_ZERO_undec : undecidable PRIMEREC_UNIV_MEETS_ZERO.
 Proof.
   apply (undecidability_from_reducibility H10C_SAT_undec).
-  exact H10C_SAT_to_RA_UNIV_HALT.H10C_SAT_RA_UNIV_HALT.
+  apply H10C_SAT_PRIMEREC_UNIV_MEETS_ZERO.
+Qed.
+
+Check PRIMEREC_UNIV_MEETS_ZERO_undec.
+
+Theorem PRIMESEQ_MEETS_ZERO_undec : undecidable PRIMESEQ_MEETS_ZERO.
+Proof.
+  apply (undecidability_from_reducibility PRIMEREC_UNIV_MEETS_ZERO_undec).
+  apply PRIMEREC_PRIMESEQ_MEETS_ZERO.
+Qed.
+
+Check PRIMESEQ_MEETS_ZERO_undec.
+
+Theorem NATSEQ_MEETS_ZERO_undec : undecidable NATSEQ_MEETS_ZERO.
+Proof.
+  apply (undecidability_from_reducibility PRIMESEQ_MEETS_ZERO_undec).
+  apply PRIMESEQ_NATSEQ_MEETS_ZERO.
+Qed.
+
+Check NATSEQ_MEETS_ZERO_undec.
+
+Theorem BOOLSEQ_MEETS_TRUE_undec : undecidable BOOLSEQ_MEETS_TRUE.
+Proof.
+  apply (undecidability_from_reducibility NATSEQ_MEETS_ZERO_undec).
+  apply reduces_dependent; exists.
+  intros f.
+  exists (fun n => match f n with 0 => true | _ => false end).
+  split; intros (n & Hn); exists n.
+  + now rewrite Hn.
+  + now destruct (f n).
+Qed.
+
+Check BOOLSEQ_MEETS_TRUE_undec.
+
+Theorem RA_UNIV_HALT_undec : undecidable RA_UNIV_HALT.
+Proof.
+  apply (undecidability_from_reducibility PRIMEREC_UNIV_MEETS_ZERO_undec).
+  exact H10C_SAT_to_RA_UNIV_HALT.PRIMEREC_UNIV_MEETS_ZERO_RA_UNIV_HALT.
 Qed.
 
 Check RA_UNIV_HALT_undec.
+
+Theorem RA_UNIV_AD_HALT_undec : undecidable RA_UNIV_AD_HALT.
+Proof.
+  apply (undecidability_from_reducibility H10UC_SAT_undec).
+  exact H10C_SAT_to_RA_UNIV_HALT.H10UC_SAT_RA_UNIV_AD_HALT.
+Qed.
+
+Check RA_UNIV_AD_HALT_undec.

theories/MuRec/Reductions/H10C_SAT_to_RA_UNIV_HALT.v

@@ -9,12 +9,16 @@
 
 Require Import List.
 
+From Undecidability.Shared 
+  Require Import pos vec.
+
 From Undecidability.MuRec 
-  Require Import recalg ra_univ ra_univ_andrej.
+  Require Import recalg beta ra_univ ra_univ_andrej.
 
 Require Import Undecidability.MuRec.RA_UNIV_HALT.
 
-Require Import Undecidability.DiophantineConstraints.H10C.
+From Undecidability.DiophantineConstraints
+ Require Import H10C Util.h10c_utils.
 
 Require Import Undecidability.Synthetic.Undecidability.
 
@@ -38,23 +42,58 @@ Local Notation "'⟦' f '⟧'" := (@ra_rel _ f) (at level 0).
      * lc is an instance of the H10C problem, ie a list of 
        h10c constraints *)
 
-Definition H10C_RA_UNIV : list h10c -> RA_UNIV_PROBLEM.
+Definition H10C_PRIMEREC_UNIV : list h10c -> PRIMEREC_UNIV_PROBLEM.
 Proof.
   intros lc.
-  destruct (nat_h10lc_surj lc) as (k & Hk).
+  destruct (nat_h10lc_surj lc) as (k & _).
   exact k.
 Defined.
 
-Theorem H10C_SAT_RA_UNIV_HALT : H10C_SAT ⪯  RA_UNIV_HALT.
+Theorem H10C_SAT_PRIMEREC_UNIV_MEETS_ZERO : H10C_SAT ⪯  PRIMEREC_UNIV_MEETS_ZERO.
 Proof.
-  exists H10C_RA_UNIV; intros lc.
-  unfold H10C_RA_UNIV.
+  exists H10C_PRIMEREC_UNIV; intros lc.
+  unfold H10C_PRIMEREC_UNIV.
   destruct (nat_h10lc_surj lc) as (k & Hk).
-  symmetry; apply ra_univ_spec; auto.
+  split.
+  + intros (phi & Hphi).
+    destruct (beta_fun_inv (h10lc_bound lc) phi) as (n & Hn).
+    generalize (h10lc_bound_prop _ _ Hn); clear Hn; intros Hn.
+    exists n; unfold ra_pr_univ; rewrite ra_h10c_eval_spec; eauto.
+    intros; apply Hn; auto.
+  + intros (n & Hn).
+    exists (beta n).
+    revert Hn; apply ra_h10c_eval_spec; auto.
 Qed.
 
-Check H10C_SAT_RA_UNIV_HALT.
+Theorem PRIMEREC_UNIV_MEETS_ZERO_RA_UNIV_HALT : PRIMEREC_UNIV_MEETS_ZERO ⪯  RA_UNIV_HALT.
+Proof.
+  apply reduces_dependent; exists.
+  intros n; exists n.
+  symmetry; apply ra_min_univ_spec.
+  apply ra_pr_univ_pr.
+Qed.
 
+Theorem PRIMEREC_PRIMESEQ_MEETS_ZERO : PRIMEREC_UNIV_MEETS_ZERO ⪯ PRIMESEQ_MEETS_ZERO.
+Proof.
+  apply reduces_dependent; exists.
+  unfold PRIMEREC_UNIV_PROBLEM, PRIMESEQ_PROBLEM.
+  intros n. 
+  exists (exist _ _ (ra_prime_seq_univ_pr _ ra_pr_univ_pr n)).
+  unfold PRIMESEQ_MEETS_ZERO, proj1_sig.
+  symmetry; apply ra_prime_seq_univ_spec.
+Qed.
+
+Theorem PRIMESEQ_NATSEQ_MEETS_ZERO : PRIMESEQ_MEETS_ZERO ⪯ NATSEQ_MEETS_ZERO.
+Proof.
+  apply reduces_dependent; exists.
+  intros (f & Hf).
+  destruct (prim_rec_reif _ Hf) as (g & Hg).
+  exists (fun n => g (n##vec_nil)).
+  unfold PRIMESEQ_MEETS_ZERO, proj1_sig, NATSEQ_MEETS_ZERO.
+  split; intros (n & Hn); exists n.
+  + revert Hn; apply ra_rel_fun; auto.
+  + rewrite <- Hn; auto.
+Qed.
 
 (* We build a similar one based on Andrej Dudenhefner
     type of H10 constraints, ie 1+x+y*y = z *)
@@ -75,5 +114,3 @@ Proof.
 Qed.
 
 Check H10UC_SAT_RA_UNIV_AD_HALT.
-
-

theories/MuRec/ra_univ.v

@@ -346,9 +346,14 @@ End iter_h10c.
 Local Hint Resolve ra_iter_h10c_prim_rec : core.
 Opaque ra_iter_h10c.
 
-Section ra_univ.
+Section ra_h10c_eval.
 
-  Let f : recalg 2.
+  (* Given a list of H10C constraints encoded using nat_h10lc
+     and a valuation phi : var (* nat *) -> nat encoded using
+     Gödel beta, test if the constraints are simultaneously
+     sastisfied or not *) 
+
+  Definition ra_h10c_eval : recalg 2.
   Proof.
     ra root ra_iter_h10c.
     + ra root ra_decomp_l.
@@ -358,16 +363,23 @@ Section ra_univ.
     + ra arg pos0.
   Defined.
 
-  Let Hf_pr : prim_rec f.
+  Fact ra_h10c_eval_pr : prim_rec ra_h10c_eval.
   Proof. ra prim rec. Qed.
 
+  Let h10c_eval := proj1_sig (prim_rec_reif _ ra_h10c_eval_pr).
+
+  Let h10c_eval_spec : forall v, ⟦ra_h10c_eval⟧ v (h10c_eval v).
+  Proof. apply (proj2_sig (prim_rec_reif _ ra_h10c_eval_pr)). Qed.
+
   Variables (lc : list h10c) (k : nat)
             (Hlc : lc = nat_h10lc k).
 
-  Let Hf_val_0 v : 
+  Hint Resolve ra_h10c_eval_pr : core.
+
+  Fact ra_h10c_eval_yes v : 
         (forall c, In c lc -> h10c_sem c (beta v))
-     -> ⟦f⟧ (v##k##vec_nil) 0.
-  Proof.
+     -> ⟦ra_h10c_eval⟧ (v##k##vec_nil) 0.
+  Proof using Hlc.
     intros H2.
     exists (decomp_l k##decomp_r k##v##vec_nil); split.
     + apply ra_iter_h10c_val_0.
@@ -385,10 +397,10 @@ Section ra_univ.
         pos split; simpl; auto.
   Qed.
 
-  Let Hf_val_1 v : 
+  Fact ra_h10c_eval_no v : 
         (exists c, In c lc /\ ~ h10c_sem c (beta v))
-     -> ⟦f⟧ (v##k##vec_nil) 1.
-  Proof.
+     -> ⟦ra_h10c_eval⟧ (v##k##vec_nil) 1.
+  Proof using Hlc.
     intros H2.
     exists (decomp_l k##decomp_r k##v##vec_nil); split.
     + apply ra_iter_h10c_val_1.
@@ -407,40 +419,83 @@ Section ra_univ.
         pos split; simpl; auto.
   Qed.
 
-  Let Hf_tot v : ⟦f⟧ (v##k##vec_nil) 0 \/ ⟦f⟧ (v##k##vec_nil) 1.
-  Proof.
+  Fact ra_h10c_eval_total v : ⟦ra_h10c_eval⟧ (v##k##vec_nil) 0 \/ ⟦ra_h10c_eval⟧ (v##k##vec_nil) 1.
+  Proof using Hlc.
     destruct (h10lc_sem_dec lc (beta v))
       as [ (c & H) | H ].
-    + right; apply Hf_val_1; exists c; auto.
-    + left; apply Hf_val_0; auto.
+    + right; apply ra_h10c_eval_no; exists c; auto.
+    + left; apply ra_h10c_eval_yes; auto.
+  Qed.
+
+  Hint Resolve ra_h10c_eval_yes : core.
+
+  Fact ra_h10c_eval_spec n : ⟦ra_h10c_eval⟧ (n##k##vec_nil) 0 <-> forall c, In c lc -> h10c_sem c (beta n).
+  Proof using Hlc.
+    split; auto; intros H.
+    destruct (h10lc_sem_dec lc (beta n))
+      as [ (c & H2 & H3) | ]; auto.
+    assert (exists c, In c lc /\ ~ h10c_sem c (beta n)) as H4 by eauto.
+    apply ra_h10c_eval_no in H4.
+    now generalize (ra_rel_fun _ _ _ _ H H4).
   Qed.
 
-  Definition ra_univ : recalg 1.
-  Proof. apply ra_min, f. Defined.
+End ra_h10c_eval.
+
+Opaque ra_h10c_eval.
 
-  Opaque f.
+Section ra_min_univ.
 
-  Theorem ra_univ_spec : ex (⟦ra_univ⟧ (k##vec_nil)) 
-                     <-> exists φ, forall c, In c lc -> h10c_sem c φ.
-  Proof using Hf_tot.
+  Variables (f : recalg 2) (Hf : prim_rec f).
+
+  Definition ra_min_univ : recalg 1.
+  Proof using f. apply ra_min, f. Defined.
+
+  Theorem ra_min_univ_spec k : 
+             ex (⟦ra_min_univ⟧ (k##vec_nil)) 
+         <-> exists n, ⟦f⟧ (n##k##vec_nil) 0.
+  Proof using Hf.
     split.
     + intros (v & Hv).
       simpl in Hv; red in Hv.
       destruct Hv as (H1 & H2).
-      destruct (h10lc_sem_dec lc (beta v))
-        as [ (c & H) | H ].
-      * assert (⟦ f ⟧ (v ## k ## vec_nil) 1) as C.
-        { apply Hf_val_1; exists c; auto. }
-        generalize (ra_rel_fun _ _ _ _ H1 C); discriminate.
-      * exists (beta v); auto.
-    + intros (phi & Hphi).
-      destruct (beta_fun_inv (h10lc_bound lc) phi)
-        as (v & Hv).
-      generalize (h10lc_bound_prop _ _ Hv); clear Hv; intros Hv.
-      apply ra_min_ex; auto.
-      exists v; simpl.
-      apply Hf_val_0.
-      intros c Hc; apply Hv; auto.
+      exists v; auto.
+    + intros (n & Hn).
+      apply ra_min_extra; eauto.
+      intros; apply prim_rec_tot; auto.
+  Qed.
+
+End ra_min_univ.
+
+Section ra_prime_seq_univ.
+
+  Variables (f : recalg 2) (Hf : prim_rec f) (n : nat).
+
+  Definition ra_prime_seq_univ : recalg 1.
+  Proof using f n.
+    ra root f.
+    + ra arg pos0.
+    + ra root (ra_cst n).
+  Defined.
+
+  Fact ra_prime_seq_univ_pr : prim_rec ra_prime_seq_univ.
+  Proof using Hf. ra prim rec. Qed.
+
+  Theorem ra_prime_seq_univ_spec : (exists k, ⟦ra_prime_seq_univ⟧ (k##vec_nil) 0)
+                               <->  exists k, ⟦f⟧ (k##n##vec_nil) 0.
+  Proof.
+    split; intros (k & Hk); exists k.
+    + destruct Hk as (v & H1 & H2).
+      generalize (H2 pos0) (H2 pos1); clear H2; rew vec.
+      revert H1.
+      vec split v with a; vec split v with b; vec nil v.
+      simpl; intros H1 <- (w & H3 & H4).
+      simpl in H3; subst; auto.
+    + exists (k##n##vec_nil); split; auto.
+      intros p; invert pos p; auto.
+      invert pos p; simpl; auto.
+      * exists vec_nil; split; simpl; auto.
+        intros p; invert pos p. 
+      * invert pos p.
   Qed.
 
-End ra_univ.
+End ra_prime_seq_univ.