Several problems on sequences of nats or Booleans

[DmxLarchey]

This PR intends to answer a request from Yves Bertot concerning the undecidability of equality testing between (constructive) real numbers. For the moment, the PR implements the following problems, but it is open for comments or improvements:

1. we build a primitive µ-recursive universal algorithm ra_pr_univ with 2 parameters such that the following problem is undecidable: given n, does the sequence k => ra_pr_univ(n,k) meet 0?
2. the following problem is undecidable: given a primitive µ-recursive sequence nat -> nat, does it meet 0?
3. the following problem is undecidable: given Coq sequence (ie a term) nat -> nat, does it meet 0?
4. the following problem is undecidable: given a term nat -> bool, does it meet true?
5. we build a µ-recursive universal (partial) algorithm ra_univ with one parameter such that the following problem is undecidable: given n, does ra_univ(n) terminate?

As already said, this PR is open for discussion but Yves was a bit surprised that a problem such as 3 or 4 was absent from the library.

[yforster]

Regarding 3 and 4 I can say that they are considered in my CSL paper discussing CT, and also cover them extensively in the thesis. I would say the reason they are not in the library (yet) is that the library focuses on problems on datatypes / enumerable types, and nat -> nat is neither. But that's no fundamental rule, so I'm happy to include them.

There are easier undecidability proofs though. We have that

datatype X -> forall p : X -> Prop, enumerable p <-> p <=m (fun (f : nat -> bool) => exists n, f n = true)

and thus every problem which is established as enumerable reduces to problem 4, and problem 4 easily reduces to problem 3 similar to the converse direction you have in your code.

It's also interesting to cover other forms of halting, totally etc for mu-recursive functions like you do, so I'm very much in favour of merging the PR, but would argue that we use a simpler proof for 4, e.g. directly reduce HaltTM 1 to problem 4 by the theorem mentioned above.

[DmxLarchey]

Sorry I think I modified your message instead of replying ... I think I managed to revert to your original one.

[DmxLarchey]

There are easier undecidability proofs though. We have that

I very much agree that going through H10 is not the simpler path to show 4 undecidable ;-) However for 1 or 5, ie universal problems where the computer is fixed and its input encodes unsolvable problems, I thought that µ-programming a solver for H10c or H10uc constraints was much, much simpler that implementing a simulator for MM or TM or L.

Clearly I am in favour of having as many reduction paths as one wishes so there is no problem in including the below reduction. Does the m in <=m stand for many-one ?

datatype X -> forall p : X -> Prop, enumerable p <-> p <=m (fun (f : nat -> bool) => exists n, f n = true)

Considering (fun (f : nat -> bool) => exists n, f n = true) however, I do not think we can close the loop from there because we have no information on how f is built, ie I doubt it could be proved many-one equivalent to TM_HALTING. What would happen with CT?

[yforster]

Yes, I meant many-one reducibility with <=m.

Standard formulations of CT wont' help I think. With CT you get that the TM-halting problem is many-one complete, i.e. that

datatype X -> forall p : X -> Prop, enumerable p <-> p <=m HaltTM 1

But the problem K := fun f : nat -> bool => exists n, f n = true we're considering is not on a datatype.

You can even prove that CT does not imply K <=m HaltTM 1 I think:

Definition LPO := forall f : nat -> bool, (exists n, f n = true) \/ ~ (exists n, f n = true).

Meta-theoretical Lemma 1: Funext /\ CT /\ ~ LPO is consistent.
Proof: Since Funext /\ CT /\ UniqueChoice are consistent, and CT /\ UniqueChoice -> ~ LPO (see my CSL paper for references)

Lemma 2: Funext /\ K <=m HaltTM 1 -> LPO
Proof: Assume Fext and a many-one reduction function F reducing K to HaltTM 1. Let c := F (fun x => false). Now G f := if F f ?= c then false else true decides whether exists n, f n = true. (similar to the inconsistency proof of 1-0-Choice, Fext, and CT)

Meta-theoretical Theorem: CT does not imply K <=m HaltTM 1
Proof: If it would , then Funext /\ CT -> LPO by Lemma 2, which is impossible by Lemma 1.

Edit: I didn't check the details, maybe one has to replace LPO with WLPO := forall f : nat -> bool, ~~ (exists n, f n = true) \/ ~ (exists n, f n = true), but the argument should be unchanged by this.

[yforster]

Indeed, you need to use WLPO, but then Lemma 2 is easy to prove:

Definition K (f : nat -> bool) := exists n, f n = true.

Goal forall p : nat -> Prop, K ⪯ₘ p -> (forall f g : nat -> bool, (forall x, f x = g x) -> f = g) ->
                  forall f : nat -> bool, ~~ (exists n, f n = true) \/ ~ (exists n, f n = true).
Proof.
  intros p [F HF] FunExt f.
  destruct (PeanoNat.Nat.eq_dec (F f) (F (fun _ => false))) as [E | E].
  - right. intros H % HF. rewrite E in H. eapply HF in H as [n [=]].
  - left. intros H. eapply E. f_equal. eapply FunExt.
    intros n. destruct (f n) eqn:E'; firstorder congruence.
Qed.

[yforster]

Sorry, wrong button, I wanted to comment, not comment & close.

[DmxLarchey]

So this statement says that if K reduces to at least one predicate over nat (whichever it is), then assuming FunExt nat bool, we can prove that WLPO holds ?

Definition K (f : nat -> bool) := exists n, f n = true.

Goal forall p : nat -> Prop, K ⪯ₘ p -> (forall f g : nat -> bool, (forall x, f x = g x) -> f = g) ->
                  forall f : nat -> bool, ~~ (exists n, f n = true) \/ ~ (exists n, f n = true).

[yforster]

Yes, exactly. And since we know that funext does not imply WLPO (by a model of Coq in constructive set theory) and that CT together with funext does not imply WLPO (by an adapted sheaf model, similar to the sheaf model by Swan and Uemura for HoTT) we know that neither without axioms nor with CT K will ever be many one equivalent to one of the problems we consider in the library