Formalizing computability theory in Coq

Question

I'm trying to teach myself Coq by formalizing formalize a mathematical theorem I'm familiar with: the undecidability of the halting problem various theorems in computability theory.

Since I'm not interested in formalizing the details of computational models (e.g., Turing machines, register machines, lambda calculi, etc.), I'm trying to do this by "teaching Coq Church-Turing thesis", namely, assuming Axioms that state properties of functions that Coq thinks to be computable (i.e., definable functions of type nat -> nat).

For example, if I wanted to tell Coq that there is an effective enumeration of the partial computable functions, I could say

Definition partial := nat -> nat -> option nat.
Axiom Phi : nat -> partial.

Here partial computable functions are thought of as (total) computable functions that, given a first argument s, simulate the computation of the original partial computable functions for s many steps. I could also add other Axioms, like Padding Lemma, and I might be able to prove the undecidability of the halting problem, and some other theorems in computability theory.

My first questions is whether or not I'm on the right track so far. Isn't it the case that what I'm trying to do is obviously impossible for incompleteness phenomena or the nature of the type system of Coq?

My second question is about relativization. If I tried to prove more serious things in computability theory, I would want to consider computation in oracles. Since oftentimes oracles are constructed as limits of partial two-valued functions, it seems (at least naively) natural to make oracles having type nat -> bool. At the same time, for oracles to be nontrivial they have to be non-computable. Considering this, does an oracle having type nat -> bool make sense?

Here is another question about oracles: it would be really nice if, for each oracle, there were the type of partial computable functions relative to that particular oracle. Can I do this by exploiting dependent type system in Coq? Does this possibility depend on the choice some of formalization oracles as discussed in the paragraph above?

EDIT: The approach above surely doesn't work as is, since I need an additional axiom:

Axiom Phi_inverse: partial -> nat.

which should not be true for oracles. Is there an approach like the one I described above (I mean, the one not involving the formalization of computational models) at all?

EDIT: To clarify my intention, I edited the problem statement above. Also, to present the style of formalization I had in mind, I present an incomplete proof of the unsolvability of the halting problem here:

Require Import Arith.
Require Import Classical.
Definition ext_eq (A B : Set) (f g : A -> B) := forall (x : A), f x = g x.
Definition partial := nat -> nat -> option nat.
Axiom Phi : nat -> partial.
Axiom Phi_inverse : partial -> nat.
Axiom effective_enumeration :
  forall (f : partial) (e : nat),
    Phi e = f <-> Phi_inverse f = e.
Axiom modulus : partial -> nat -> nat.
Axiom persistence :
  forall (f : partial) n s,
    s >= modulus f n -> f s n = f (modulus f n) n.
Definition limit (f : partial) n := f (modulus f n) n.
Definition total (f : partial)
  := forall n, exists s, exists m, f s n = Some m.
Definition flip n := match n with O => 1 | S _ => 0 end.
Definition K e := exists n, limit (Phi e) e = Some n.
Theorem K_is_undecidable :
  ~ exists e,
      total (Phi e)
      /\ forall e', limit (Phi e) e' = Some 0 <-> ~K e'. 
Proof.
  intro.
  destruct H as [e].
  destruct H.
  pose proof (H0 (Phi_inverse (fun s e' =>
                                match (Phi e s e') with
                                  | Some n => Some (flip n)
                                  | None => None end))).
(* to be continued *)

Answer 1

First, some clarification:

Functions that Coq thinks to be computable (i.e., definable functions of type nat -> nat)

Strictly speaking, Coq does not think that functions are computable. Coq's logic assert that there are certain functions can be defined, and that you can do certain things with them, but an arbitrary function is a black box as far as Coq is concerned. In particular, it is consistent to postulate the existence of a non-computable function.

Now, to the actual questions. Here's a solution that more or less follows Atsby's answer. We will represent a Turing machine function by a Coq function of type nat -> nat -> option bool. The idea is that the first argument is the input, and the second one is a maximum number of steps we'll run for. The output is None if we fail to produce an answer, and Some b if the computation terminates with producing b as an answer. I took the liberty of using Ssreflect to make the code a bit simpler:

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.choice.

Section Halting.

(* [code f c] holds if [f] is representable by some
   Turing machine code [c]. Notice that we don't assume that
   [code] is computable, nor do we assume that all functions 
   [nat -> nat -> option bool] can be represented by some code, 
   which means that we don't rule out the existence of
   non-computable functions. *)
Variable code : (nat -> nat -> option bool) -> nat -> Prop.

(* We assume that we have a [decider] for the halting problem, with
   its specification given by [deciderP]. Specifically, when running
   on a number [m] that represents a pair [(c, n)], where [c] is the
   code for some Turing machine [f] and [n] some input for [f], we
   know that [decider m] will halt at some point, producing [true] iff
   [f] halts on input [n].

   This definition uses a few convenience features from Ssreflect to
   make our lives simpler, namely, the [pickle] function, that
   converts from [nat * nat] to [nat], and the implicit coercion from
   [option] to [bool] ([Some] is mapped to [true], [None] to [false]) *)
Variable decider : nat -> nat -> option bool.
Hypothesis deciderP :
  forall f c, code f c ->
  forall (n : nat),
     (forall s,
        match decider (pickle (c, n)) s with
        | Some true  => exists s', f n s'
        | Some false => forall s', negb (f n s')
        | None => True
        end) /\
     exists s, decider (pickle (c, n)) s.

(* Finally, we define the usual diagonal function, and postulate that
   it is representable by some code [f_code]. *)
Definition f (n : nat) s :=
  match decider (pickle (n, n)) s with
  | Some false => Some false
  | _ => None
  end.
Variable f_code : nat.
Hypothesis f_codeP : code f f_code.

(* The actual proof is straightforward (8 lines long). 
   I'm omitting it to avoid spoiling the fun. *)
Lemma pandora : False.
Proof. (* ... *) Qed.

End Halting.

In summary, it is perfectly reasonable to use Coq functions to talk about the Halting problem, and the result is quite simple. Notice that the above theorem doesn't force code to be related to Turing machines at all -- for instance, you could interpret the above theorem as saying that the halting problem for oracle Turing machines cannot be solved by an oracle Turing machine. In the end, what makes these results different from each other is the formalization of the underlying computation model, which is exactly what you wanted to avoid.

As for the template you were trying to start with, assuming that Phi exists and has an inverse already results in a contradiction. This is the usual diagonal argument:

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.choice.

Definition partial := nat -> nat -> option nat.
Axiom Phi : nat -> partial.
Axiom Phi_inverse : partial -> nat.
Axiom effective_enumeration :
  forall (f : partial) (e : nat),
    Phi e = f <-> Phi_inverse f = e.

Lemma pandora : False.
Proof.
pose f n (m : nat) :=
  if Phi n n n is Some p then None
  else Some 0.
pose f_code := Phi_inverse f.
move/effective_enumeration: (erefl f_code) => P.
move: (erefl (f f_code f_code)).
rewrite {1}/f P.
by case: (f _ _).
Qed.

The problem is that even though externally we know that Coq-definable functions are in bijection with nat, we cannot assert this fact internally. Asserting the existence of a non-effective code relation solves this issue.

As for oracles, having an oracle be a function of type nat -> bool does make sense, but you need to make sure that you are not violating other assumptions that you have in the proof by doing this. For instance, you can postulate that all nat -> nat functions are computable, by axiomatizing that you have a function like your Phi, but that would mean that your oracle would also be computable. Using a relation like code above allows you to have somewhat the best of both worlds.

Finally, as for relativization results, it depends a lot on what you want to prove. For instance, if you just want to show that certain functions over oracles can be written, you can write a parametric function and show that it has a certain property when the oracle has a certain behavior, without the need for dependent types. E.g.

Definition foo (oracle : nat -> bool) (n : nat) : bool :=
  (* some definition ... *).

Definition oracle_spec (oracle : nat -> bool) : Prop :=
  (* some definition ... *).

Lemma fooP oracle :
  oracle_spec oracle ->
  (* some property of [foo oracle]. *)

Finally, here's an interesting link discussing Church's thesis in dependent type theory, which you may find interesting: https://existentialtype.wordpress.com/2012/08/09/churchs-law/

Answer 2

Here's how you would introduce a meaningful axiom (I'm still learning Coq myself so hopefully if I've done this wrong someone will correct me).

With Parameter we are stipulating the existence of a function called compute without giving a definition. With Axiom we are fixing some of its properties (hopefully without introducing a contradiction). Allegedly, Parameter and Axiom do the same thing internally.

Likewise to the declaration of compute, your Axiom Phi stipulates the existence of a function Phi from nat to partial, but you can't do anything with it in Coq yet because it has no known properties. Note that the existence of Phi doesn't imply anything like "there is an effective enumeration of the partial computable functions".

Here the axiom states that, when called with a greater number of allowed steps of computation, compute never changes an ACCEPT into a REJECT or vice versa or backs up to NOTYET. With these definitions, I've checked that it is possible to prove the trivial lemma test as a starter.

Obviously, I haven't carried this through to see if you can prove the undecidability of the halting problem but it should be possible by adding an axiom asserting the existence of a nat representing a program that computes equivalently to the construction required in proof of the halting problem. Of course, largely the entire point of the proof is lost by doing things this way but there'd still be a little bit left to prove.

Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.

Definition narrowing a b : Prop :=
(match a with
| ACCEPT => b = ACCEPT
| REJECT => b = REJECT
| NOTYET => True
end).

Parameter compute : nat (* program *) -> nat (* argument *) -> nat (* steps *) -> result.

Axiom compute_narrowing:
forall program input steps steps',
(steps' >= steps) ->
(narrowing (compute program input steps) (compute program input steps')).

Lemma test: ~ exists program input steps, (compute program input steps) = ACCEPT /\ (compute program input (steps + 1)) = NOTYET

EDIT: Here's a bit more. After thinking about the problem a bit, I realize I was definitely wrong that such a proof would necessarily have to axiomize the interesting constructions. One can plug in axioms that allow only simple low-level constructions and build higher-level ones on top of them. I'm assuming the goal is to follow Minsky's proof, as it seems simpler to formalize:

http://www.cs.odu.edu/~toida/nerzic/390teched/computability/unsolv-1.html

Here, additional axioms assert 1) the existence of a program that always accept 2) the existence of a program that always rejects and 3) for any three programs conditional when_accept when_reject, the existence of a program that first runs conditional and then based on that runs when_accept or when_reject (all the subprogram invocations are on the same input given to the composed program). With these axioms, it is possible to prove, for any program target the existence of a program that runs target and then outputs the opposite result (but also looping forever if target loops forever). This "negation" construction is just a simple example, and not one of the constructions used in Minsky's proof.

To follow Minsky's proof, one would need to add further axioms for the existence of a program that loops, and for the copier construction. Then add a definition for when a program is a decider, and prove that there is no decider for the halting problem. The codec axiom saves having to define functions encode_pair and decode_pair in Coq and prove codec as a Lemma. I think the properties of encode_pair and decode_pair will be needed for the copier construction and in the final proof (certainly the definition of a decider for the halting problem would need it as the machine input is a pair).

Require Import List.
Require Import Arith.
Require Import Omega.

Ltac mp_cancel :=
  repeat match goal with
  | [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
  end.

Ltac mp_cancel_reflexivity :=
  repeat match goal with
  | [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
  end.

Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result
.

Definition narrowing a b : Prop :=
  (match a with
  | ACCEPT => b = ACCEPT
  | REJECT => b = REJECT
  | NOTYET => True
  end)
.

Parameter encode_pair : (nat * nat) -> nat.
Parameter decode_pair : nat -> (nat * nat).

Axiom codec:
  forall a b,
  (decode_pair (encode_pair (a, b))) = (a, b).

Parameter compute : nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.

Axiom compute_narrowing:
  forall program input steps steps',
  (steps' >= steps) -> (narrowing (compute program input steps) (compute program input steps')).

Axiom exists_always_accept:
  exists program_always_accept,
  forall input,
  exists steps,
  (compute program_always_accept input steps) = ACCEPT.

Axiom exists_always_reject:
  exists program_always_reject,
  forall input,
  exists steps,
  (compute program_always_reject input steps) = REJECT.

Definition result_compose_conditional (result_conditional : result) (result_when_accept : result) (result_when_reject : result) : result :=
  (match result_conditional with
  | ACCEPT => result_when_accept
  | REJECT => result_when_reject
  | NOTYET => NOTYET
  end).

Axiom exists_compose_conditional:
  forall program_conditional program_when_accept program_when_reject,
  exists program_composition,
  forall input steps_control steps_when result_conditional result_when_accept result_when_reject,
  (
    ((compute program_conditional input steps_control) = result_conditional) ->
    ((compute program_when_accept input steps_when) = result_when_accept) ->
    ((compute program_when_reject input steps_when) = result_when_reject) ->
    (exists steps_composition, (compute program_composition input steps_composition) = (result_compose_conditional result_conditional result_when_accept result_when_reject))
  ).

Definition result_negation (result_target : result) : result :=
  (match result_target with
  | ACCEPT => REJECT
  | REJECT => ACCEPT
  | NOTYET => NOTYET
  end).

Lemma exists_negation:
  forall program_target,
  exists program_negation,
  forall input steps_target result_target,
  (
    ((compute program_target input steps_target) = result_target) ->
    (exists steps_negation, (compute program_negation input steps_negation) = (result_negation result_target))
  ).
intros.
elim exists_always_accept; intros program_always_accept H_always_accept.
elim exists_always_reject; intros program_always_reject H_always_reject.
elim exists_compose_conditional with (program_conditional := program_target) (program_when_accept := program_always_reject) (program_when_reject := program_always_accept); intros program_negation H_program_negation.
exists program_negation.
intros.
specialize H_always_accept with input. elim H_always_accept; clear H_always_accept; intros steps_accept H_always_accept.
specialize H_always_reject with input. elim H_always_reject; clear H_always_reject; intros steps_reject H_always_reject.
pose (steps_when := (steps_accept + steps_reject)).
specialize H_program_negation with input steps_target steps_when result_target (compute program_always_reject input steps_when) (compute program_always_accept input steps_when).
mp_cancel.
mp_cancel_reflexivity.
elim H_program_negation; clear H_program_negation; intros steps_negation H_program_negation.
exists (steps_negation).
rewrite H_program_negation; clear H_program_negation.
replace (compute program_always_reject input steps_when) with REJECT; symmetry.
replace (compute program_always_accept input steps_when) with ACCEPT; symmetry.
unfold result_compose_conditional.
unfold result_negation.
reflexivity.
assert (T := (compute_narrowing program_always_accept input steps_accept steps_when)).
assert (steps_when >= steps_accept).
unfold steps_when.
omega.
mp_cancel.
unfold narrowing in T.
rewrite H_always_accept in T.
assumption.
assert (T := (compute_narrowing program_always_reject input steps_reject steps_when)).
assert (steps_when >= steps_reject).
unfold steps_when.
omega.
mp_cancel.
unfold narrowing in T.
rewrite H_always_reject in T.
assumption.
Qed.

EDIT#2: I had sort of understood that you wanted to be able to program the constructions in Coq but I hadn't figured out how that could be done at the time of my previous edit. In the following snippet it's done using the axiom exists_program_of_procedure, which asserts that there exists a nat representing a program that has the same behavior as any given procedure (at least for well-behaved procedures that are "narrowing" in their computation). Included is a straightforward formalization of Minsky's proof. Your approach has certainly cleaner axioms and will probably result in shorter proof due to the use of modulus to oracle-ify the steps to stabilization rather than dealing with narrowing. Most interesting to see is whether your approach can be carried out without the use of Classical. Update: It appears that your axioms introduce a contradiction since modulus isn't supposed to be computable (?).

Require Import List.
Require Import Arith.
Require Import Omega.

Ltac mp_cancel :=
  repeat match goal with
  | [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
  end.

Ltac mp_cancel_reflexivity :=
  repeat match goal with
  | [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
  end.

Parameter encode_pair: (nat * nat) -> nat.
Parameter decode_pair: nat -> (nat * nat).

Axiom decode_encode: forall a b, (decode_pair (encode_pair (a, b))) = (a, b).

Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.

Definition result_narrowing (a : result) (b : result) : Prop :=
  (match a with
  | ACCEPT => b = ACCEPT
  | REJECT => b = REJECT
  | NOTYET => True
  end).

Lemma result_narrowing_trans: forall a b c, result_narrowing a b -> result_narrowing b c -> result_narrowing a c.
intros until 0.
destruct a; destruct b; destruct c;
  unfold result_narrowing;
  intros;
  try discriminate;
  reflexivity.
Qed.

Parameter compute: nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.

Axiom compute_narrowing:
  forall program input steps steps',
  (steps' >= steps) -> (result_narrowing (compute program input steps) (compute program input steps')).

Require Import Classical.

Lemma compute_non_divergent:
  forall program input steps steps',
  (compute program input steps) = ACCEPT ->
  (compute program input steps') = REJECT ->
  False.
intros.
assert (T := (classic (steps' >= steps))).
destruct T.
assert (T := (compute_narrowing program input steps steps')).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate T.
unfold not in H1.
assert (T := (classic (steps' = steps))).
destruct T.
rewrite H2 in H0.
rewrite H in H0.
discriminate.
assert (steps >= steps').
omega.
assert (T := (compute_narrowing program input steps' steps)).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate.
Qed.

Definition procedure_type := nat (* input *) -> nat (* depth *) -> result.

Definition procedure_narrowing (procedure : procedure_type) : Prop :=
  forall input depth depth',
  (depth' >= depth) -> (result_narrowing (procedure input depth) (procedure input depth')).

Axiom exists_program_of_procedure:
  forall procedure : procedure_type,
  (procedure_narrowing procedure) ->
  exists program,
  forall input,
  (
    forall depth,
    exists steps,
    (result_narrowing (procedure input depth) (compute program input steps))
  ) /\
  (
    forall steps,
    exists depth,
    (result_narrowing (compute program input steps) (procedure input depth))
  ).

Definition program_halts_on_input (program : nat) (input : nat) : Prop :=
  (exists steps, (compute program input steps) <> NOTYET).

Definition program_is_decider (program : nat) : Prop :=
  forall input,
  exists steps,
  (compute program input steps) <> NOTYET.

Definition program_solves_halting_problem_partially (program : nat) : Prop :=
  forall input,
  forall steps,
  (
       ((compute program input steps) = ACCEPT)
    -> (match (decode_pair input) with | (target_program, target_input) => (  (program_halts_on_input target_program target_input)) end)
  ) /\
  (
       ((compute program input steps) = REJECT)
    -> (match (decode_pair input) with | (target_program, target_input) => (~ (program_halts_on_input target_program target_input)) end)
  ).

Lemma minsky: (~ (exists halts, (program_is_decider halts) /\ (program_solves_halting_problem_partially halts))).
unfold not.
intros H_ph.
elim H_ph; clear H_ph; intros invocation_halts [H_ph_d H_ph_b].
pose
  (procedure_modified := (fun (input : nat) (depth : nat) =>
    (match (compute invocation_halts input depth) with
    | ACCEPT => NOTYET
    | REJECT => REJECT
    | NOTYET => NOTYET
    end))).
pose
  (procedure_wrapper := (fun (input : nat) (depth : nat) =>
    (procedure_modified (encode_pair (input, input)) depth))).
unfold procedure_modified in procedure_wrapper.
clear procedure_modified.
assert (T1 := (exists_program_of_procedure procedure_wrapper)).
assert (T2 : (procedure_narrowing procedure_wrapper)).
{
  clear T1.
  unfold procedure_narrowing, procedure_wrapper.
  intros.
  unfold result_narrowing.
  case_eq (compute invocation_halts (encode_pair (input, input)) depth); try intuition.
  assert (T := (compute_narrowing invocation_halts (encode_pair (input, input)) depth depth')).
  mp_cancel.
  rewrite H0 in T.
  unfold result_narrowing in T.
  rewrite T.
  reflexivity.
}
mp_cancel.
clear T2.
elim T1; clear T1; intros program_wrapper H_pw.
unfold procedure_wrapper in H_pw.
clear procedure_wrapper.
specialize (H_pw program_wrapper).
destruct H_pw as [H_pw_fwd H_pw_rev].
unfold program_is_decider in H_ph_d.
specialize (H_ph_d (encode_pair (program_wrapper, program_wrapper))).
elim H_ph_d; clear H_ph_d; intros steps_inner H_ph_d.
unfold program_solves_halting_problem_partially in H_ph_b.
specialize (H_ph_b (encode_pair (program_wrapper, program_wrapper)) steps_inner).
destruct H_ph_b as [H_ph_b_1 H_ph_b_2].
case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) steps_inner).
{
  intros.
  rewrite H in *.
  mp_cancel_reflexivity.
  unfold program_halts_on_input in H_ph_b_1.
  rewrite decode_encode in H_ph_b_1.
  elim H_ph_b_1; clear H_ph_b_1; intros steps_outer H_ph_b_1.
  specialize (H_pw_rev steps_outer).
  case_eq (compute program_wrapper program_wrapper steps_outer).
  {
    intros.
    rewrite H0 in *.
    unfold result_narrowing in H_pw_rev.
    elim H_pw_rev; clear H_pw_rev; intros depth H_pw_rev.
    case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) depth); intros Hx; rewrite Hx in *; try discriminate.
  }
  {
    intros.
    rewrite H0 in *.
    unfold result_narrowing in H_pw_rev.
    elim H_pw_rev; clear H_pw_rev; intros depth H_pw_rev.
    case_eq (compute invocation_halts (encode_pair (program_wrapper, program_wrapper)) depth); intros Hx; rewrite Hx in *; try discriminate.
    assert (T := (compute_non_divergent invocation_halts (encode_pair (program_wrapper, program_wrapper)) steps_inner depth)).
    mp_cancel.
    assumption.
  }
  {
    intros.
    intuition.
  }
}
{
  intros.
  rewrite H in *.
  mp_cancel_reflexivity.
  unfold not, program_halts_on_input in H_ph_b_2.
  specialize (H_pw_fwd steps_inner).
  rewrite H in H_pw_fwd.
  unfold result_narrowing in H_pw_fwd.
  elim H_pw_fwd; intros.
  rewrite decode_encode in H_ph_b_2.
  contradict H_ph_b_2.
  exists x.
  unfold not.
  intros.
  rewrite H0 in H1.
  discriminate.
}
{
  intros.
  unfold not in H_ph_d.
  mp_cancel.
  assumption.
}
Qed.

Answer 3

I thought I'd add a new answer to flesh out the details of the scheme I proposed in comments to OP's post regarding the handling of oracles.

I'm not sure if DeAmorim's scheme for handling oracles can be made to work quite as well. The philosophy here is that one should avoid postulating the existence of constructions with various properties, and simply define them instead (e.g., as Coq functions) and show that they have the required properties. Because we don't want to handle actual descriptions of Turing machines down to the level of state machines, the hack used is to postulate a mapping from Coq functions to programs. When it is assumed the Coq functions can be mapped to programs, the logic necessarily becomes inconsistent when one introduces an uncomputable oracle in the form of a Coq function (even though one would evidently not be supplying a constructive definition of it). While it is unlikely that one would exploit such-arising inconsistency of the logic in a manual proof, it is more reassuring to avoid inconsistent logic altogether.

(However, it is not clear if the proposed strategy achieves this. The article linked in DeAmorim's answer says "The claim is that Church’s Law, stated as a type (proposition) within ETT, is false, which is to say that it entails a contradiction." The maths behind this seems to be quite a bit above my level; it is not clear to me whether it applies.)

The example problem considered here is solving H_TM assuming we have an oracle for A_TM. H_TM tells us if a Turing machine ("program") halts for a particular input, while A_TM tells us if a Turing machine accepts a particular input.

Clearly, the reverse case of having an oracle for H_TM and trying to solve A_TM is completely trivial. Simply query the oracle to determine if the program halts, and if so, the program can be run to termination to determine if it accepts.

Somewhat less trivially, H_TM can be decided if we are given an oracle for A_TM. Clearly, if the machine would accept the input, an oracle query can determine this. Now the trick is to construct a modified program that does the opposite of the original program (exchanges ACCEPT and REJECT), and an oracle query on this modified program now determines whether the original program would reject the input. If the oracle rejected both cases, the original program loops on the given input, and we reject (in the other cases we accepted).

The "machinery" implemented here allows definition of oracle verifiers of the type nat (* query *) -> nat (* wisdom *) -> bool (* advice *). The real oracle corresponding to a verifier will output true iff there exists a value of wisdom that causes the verifier to output true. The clever bit is that uncomputable oracles can be generated from computable verifiers, and a single existential quantifier is sufficient to generate fairly powerful oracles.

A "procedure with oracle" (pwo) must be implemented in terms of looped state, as one cannot simply use function application to invoke an oracle in this setup.

The inductive pwo_entails basically defines the evaluation of pwos, similar to the way evaluation of Imp programs are defined by ceval in Software Foundations.

The oracle verifier for A_TM orv_atm simply executes the program for wisdom steps to determine if it accepts, while pwo_hfa makes up to two oracle calls to decide H_TM. The lemma H_from_A shows that this works.

One big change from the previous answer involving the Halting problem is that the basic axiom allowing conversion of Coq functions into programs that can be passed to compute has been strengthened, it is now assumed that a computable function exists to perform such conversion. Previously, only the existence of a corresponding program was postulated. This change is needed because pwo_hfa needs to generate a program "programmatically".

Require Import List.
Require Import Arith.
Require Import Omega.

Ltac mp_cancel :=
  repeat match goal with
  | [ H2 : ?P -> ?Q , H1 : ?P |- _ ] => specialize (H2 H1)
  end.

Ltac mp_cancel_reflexivity :=
  repeat match goal with
  | [ H1 : ?P = ?P -> ?Q |- _ ] => assert (H_mp_cancel_reflexivity : P = P) by reflexivity; specialize (H1 H_mp_cancel_reflexivity); clear H_mp_cancel_reflexivity
  end.

Parameter encode_pair: (nat * nat) -> nat.
Parameter decode_pair: nat -> (nat * nat).

Axiom decode_encode: forall a b, (decode_pair (encode_pair (a, b))) = (a, b).
Axiom encode_decode: forall x,   (encode_pair (decode_pair x)) = x.

Inductive result :=
| ACCEPT : result
| REJECT : result
| NOTYET : result.

Definition result_narrowing (a : result) (b : result) : Prop :=
  (match a with
  | ACCEPT => b = ACCEPT
  | REJECT => b = REJECT
  | NOTYET => True
  end).

Lemma result_narrowing_trans: forall a b c, result_narrowing a b -> result_narrowing b c -> result_narrowing a c.
intros until 0.
destruct a; destruct b; destruct c;
  unfold result_narrowing;
  intros;
  try discriminate;
  reflexivity.
Qed.

Lemma result_push_accept: forall x, result_narrowing ACCEPT x -> x = ACCEPT.
unfold result_narrowing.
intuition.
Qed.

Lemma result_push_reject: forall x, result_narrowing REJECT x -> x = REJECT.
unfold result_narrowing.
intuition.
Qed.

Parameter compute: nat (* program *) -> nat (* input *) -> nat (* steps *) -> result.

Axiom compute_narrowing:
  forall program input steps steps',
  (steps' >= steps) -> (result_narrowing (compute program input steps) (compute program input steps')).

Require Import Classical.

Lemma compute_non_divergent:
  forall program input steps steps',
  (compute program input steps) = ACCEPT ->
  (compute program input steps') = REJECT ->
  False.
intros.
assert (T := (classic (steps' >= steps))).
destruct T.
assert (T := (compute_narrowing program input steps steps')).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate T.
unfold not in H1.
assert (T := (classic (steps' = steps))).
destruct T.
rewrite H2 in H0.
rewrite H in H0.
discriminate.
assert (steps >= steps').
omega.
assert (T := (compute_narrowing program input steps' steps)).
mp_cancel.
rewrite H, H0 in T.
unfold result_narrowing in T.
discriminate.
Qed.

Definition procedure_type := nat (* input *) -> nat (* depth *) -> result.

Definition procedure_narrowing (procedure : procedure_type) : Prop :=
  forall input depth depth',
  (depth' >= depth) -> (result_narrowing (procedure input depth) (procedure input depth')).

Parameter program_of_procedure: procedure_type (* procedure *) -> nat (* program *).

Axiom program_of_procedure_behavior:
  forall procedure : procedure_type,
  (procedure_narrowing procedure) ->
  forall input,
  (
    forall depth,
    exists steps,
    (result_narrowing (procedure input depth) (compute (program_of_procedure procedure) input steps))
  ) /\
  (
    forall steps,
    exists depth,
    (result_narrowing (compute (program_of_procedure procedure) input steps) (procedure input depth))
  ).

Definition program_halts_on_input (program : nat) (input : nat) : Prop :=
  (exists steps, (compute program input steps) <> NOTYET).

(* orv = oracle verifier *)

Definition orv_type := nat (* query *) -> nat (* wisdom *) -> bool (* advice *).

Definition oracle_accepts (oracle : orv_type) (query : nat) :=
  exists wisdom, (oracle query wisdom) = true.

Definition oracle_rejects (orv : orv_type) (inp : nat) := (~ (oracle_accepts orv inp)).

(* pwo = procedure with oracle *)

Inductive pwo_out :=
| PWO_RESULT : bool (* result *) -> pwo_out
| PWO_ORACLE : nat (* state *) -> nat (* query *) -> pwo_out
.

Definition pwo_type := nat (* input *) -> nat (* state *) -> bool (* advice *) -> pwo_out.

Inductive pwo_entails: orv_type (* oracle *) -> pwo_type (* procedure *) -> nat (* input *) -> nat (* state *) -> bool (* advice *) -> bool (* result *) -> Prop :=
| PwoEntailsResult:
forall oracle procedure input state advice result,
(procedure input state advice) = (PWO_RESULT result) ->
(pwo_entails oracle procedure input state advice result)
| PwoEntailsOracleAccept:
forall oracle procedure input state advice result state' query,
(procedure input state advice) = (PWO_ORACLE state' query) ->
(oracle_accepts oracle query) ->
(pwo_entails oracle procedure input state' true   result) ->
(pwo_entails oracle procedure input state  advice result)
| PwoEntailsOracleReject:
forall oracle procedure input state advice result state' query,
(procedure input state advice) = (PWO_ORACLE state' query) ->
(oracle_rejects oracle query) ->
(pwo_entails oracle procedure input state' false  result) ->
(pwo_entails oracle procedure input state  advice result)
.

Definition pwo_decider_relative (orv : orv_type) (pwo : pwo_type) :=
  forall input,
  (pwo_entails orv pwo input 0 false false) \/
  (pwo_entails orv pwo input 0 false true).

(* define oracle for A_TM (turing machine accepts a particular input) *)

Definition orv_atm (pair_program_input : nat) (wisdom : nat) : bool :=
  (match (decode_pair pair_program_input) with
  | (target_program, target_input) =>
      (match (compute target_program target_input wisdom) with
      | ACCEPT => true
      | _ => false
      end)
  end).

(* define procedure for H_TM (turing machine halts on a particular input) relative to an oracle for A_TM *)

Definition pwo_hfa_construction (target_program : nat) :=
  (fun input depth =>
    (match (compute target_program input depth) with
    | ACCEPT => REJECT
    | REJECT => ACCEPT
    | NOTYET => NOTYET
  end)).

Lemma pwo_hfa_construction_narrowing: forall target_program, (procedure_narrowing (pwo_hfa_construction target_program)).
intros.
unfold procedure_narrowing, result_narrowing, pwo_hfa_construction.
intros.
case_eq (compute target_program input depth); intro; try
(
case_eq (compute target_program input depth'); intro; try reflexivity; try
(
assert (T := (compute_narrowing target_program input depth depth'));
mp_cancel;
unfold result_narrowing in T;
rewrite H0 in T;
rewrite H1 in T;
discriminate
)
).
Qed.

Definition pwo_hfa (input : nat) (state : nat) (advice : bool) : pwo_out :=
  (match (decode_pair input) with
  | (target_program, target_input) =>
      (match state with
      | O =>
        (PWO_ORACLE 1 (encode_pair (target_program, target_input)))
      | (S O) =>
        (if advice
         then (PWO_RESULT true)
         else (PWO_ORACLE 2 (encode_pair ((program_of_procedure (pwo_hfa_construction target_program)), target_input))))
      | _ =>
        (PWO_RESULT advice)
      end)
  end).

Lemma H_from_A:
  exists pwo_hfa,
  (pwo_decider_relative orv_atm pwo_hfa) /\
  (
    forall input,
      (pwo_entails orv_atm pwo_hfa input 0 false true  ->
        (match (decode_pair input) with | (target_program, target_input) => (  (program_halts_on_input target_program target_input)) end)) /\
      (pwo_entails orv_atm pwo_hfa input 0 false false ->
        (match (decode_pair input) with | (target_program, target_input) => (~ (program_halts_on_input target_program target_input)) end))
  )
.
exists pwo_hfa.
split.
{
  unfold pwo_decider_relative.
  intros.
  pose (pair := (decode_pair input)).
  case_eq (pair); intros target_program target_input H_pair.
  replace input with (encode_pair (target_program, target_input)).
  Focus 2.
  {
    rewrite <- H_pair.
    unfold pair.
    apply encode_decode.
  }
  Unfocus.
  assert (T1 := (classic (oracle_accepts orv_atm (encode_pair (target_program, target_input))))).
  destruct T1 as [T1 | T1].
  {
    right.
    eapply PwoEntailsOracleAccept.
    Focus 2.
    eexact T1.
    unfold pwo_hfa.
    rewrite decode_encode.
    instantiate (1 := 1).
    reflexivity.
    apply PwoEntailsResult.
    unfold pwo_hfa.
    rewrite decode_encode.
    reflexivity.
  }
  {
    assert (T2 := (classic (oracle_accepts orv_atm (encode_pair ((program_of_procedure (pwo_hfa_construction target_program)), target_input))))).
    destruct T2 as [T2 | T2].
    {
      right.
      eapply PwoEntailsOracleReject.
      Focus 2.
      unfold oracle_rejects.
      eexact T1.
      unfold pwo_hfa.
      rewrite decode_encode.
      instantiate (1 := 1).
      reflexivity.
      eapply PwoEntailsOracleAccept.
      Focus 2.
      eexact T2.
      unfold pwo_hfa.
      rewrite decode_encode.
      instantiate (1 := 2).
      reflexivity.
      apply PwoEntailsResult.
      unfold pwo_hfa.
      rewrite decode_encode.
      reflexivity.
    }
    {
      left.
      eapply PwoEntailsOracleReject.
      Focus 2.
      unfold oracle_rejects.
      eexact T1.
      unfold pwo_hfa.
      rewrite decode_encode.
      instantiate (1 := 1).
      reflexivity.
      eapply PwoEntailsOracleReject.
      Focus 2.
      eexact T2.
      unfold pwo_hfa.
      rewrite decode_encode.
      instantiate (1 := 2).
      reflexivity.
      apply PwoEntailsResult.
      unfold pwo_hfa.
      rewrite decode_encode.
      reflexivity.
    }
  }
}
{
  intros.
  case_eq (decode_pair input); intros target_program target_input H_input.
  replace input with (encode_pair (target_program, target_input)).
  Focus 2.
  {
    rewrite <- H_input.
    rewrite encode_decode.
    reflexivity.
  }
  Unfocus.
  clear H_input.
  split.
  {
    intros.
    inversion H; subst.
    {
      unfold pwo_hfa in H0.
      rewrite decode_encode in H0.
      discriminate H0.
    }
    {
      unfold pwo_hfa in H0.
      rewrite decode_encode in H0.
      injection H0.
      intros.
      rewrite <- H3 in H1.
      unfold oracle_accepts in H1.
      unfold program_halts_on_input.
      elim H1; intros.
      exists x.
      unfold orv_atm in H5.
      rewrite decode_encode in H5.
      destruct (compute target_program target_input x); try intuition; try discriminate.
    }
    {
      unfold pwo_hfa in H0.
      rewrite decode_encode in H0.
      injection H0.
      intros.
      rewrite <- H4 in *.
      inversion H2; subst.
      {
        unfold pwo_hfa in H5.
        rewrite decode_encode in H5.
        discriminate.
      }
      {
        unfold pwo_hfa in H5.
        rewrite decode_encode in H5.
        injection H5; intros.
        subst.
        unfold oracle_accepts in H6.
        unfold program_halts_on_input.
        elim H6; intros.
        unfold orv_atm in H3.
        rewrite decode_encode in H3.
        case_eq (compute (program_of_procedure (pwo_hfa_construction target_program)) target_input x); intros; rewrite H4 in H3; try discriminate.
        assert
          (T :=
            (program_of_procedure_behavior
              (pwo_hfa_construction target_program)
              (pwo_hfa_construction_narrowing target_program)
              target_input
            )).
        destruct T.
        specialize H9 with x.
        elim H9; intros.
        assert ((pwo_hfa_construction target_program target_input x0) = ACCEPT).
        eapply result_push_accept.
        rewrite <- H4.
        assumption.
        unfold pwo_hfa_construction in H11.
        case_eq (compute target_program target_input x0); intros; rewrite H12 in H11; try discriminate.
        exists x0.
        unfold not.
        intros.
        rewrite H12 in H13.
        discriminate.
      }
      {
        unfold pwo_hfa in H5.
        rewrite decode_encode in H5.
        injection H5; intros.
        subst.
        inversion H7.
        unfold pwo_hfa in H3.
        rewrite decode_encode in H3.
        discriminate H3.
        unfold pwo_hfa in H3.
        rewrite decode_encode in H3.
        discriminate H3.
        unfold pwo_hfa in H3.
        rewrite decode_encode in H3.
        discriminate H3.
      }
    }
  }
  {
    intros.
    unfold not.
    intros.
    inversion H; subst; unfold pwo_hfa in H1; rewrite decode_encode in H1; try discriminate; injection H1; intros; subst.
    {
      inversion H3; subst; unfold pwo_hfa in H4; rewrite decode_encode in H4; try discriminate; injection H4; intros; subst.
    }
    {
      inversion H3; subst; unfold pwo_hfa in H4; rewrite decode_encode in H4; try discriminate; injection H4; intros; subst.
      {
        inversion H6; subst; unfold pwo_hfa in H7; rewrite decode_encode in H7; try discriminate.
      }
      {
        (* oracle rejected both on a program that halts *)
        clear H H3 H1 H6 H4.
        unfold program_halts_on_input in H0.
        elim H0; clear H0; intros.
        unfold not in H.
        case_eq (compute target_program target_input x); intros; try ( solve [ intuition ] ).
        {
          rename H2 into HH.
          unfold oracle_rejects, not in HH.
          apply HH.
          clear HH.
          unfold oracle_accepts.
          exists x.
          unfold orv_atm.
          rewrite decode_encode.
          rewrite H0.
          reflexivity.
        }
        {
          rename H5 into HH.
          unfold oracle_rejects, not in HH.
          apply HH.
          clear HH.
          unfold oracle_accepts.
          assert
          (T :=
            (program_of_procedure_behavior
              (pwo_hfa_construction target_program)
              (pwo_hfa_construction_narrowing target_program)
              target_input
            )).
          destruct T.
          assert ((pwo_hfa_construction target_program target_input x) = ACCEPT).
          unfold pwo_hfa_construction.
          rewrite H0.
          reflexivity.
          specialize H1 with x.
          elim H1; intros.
          rewrite H4 in H5.
          unfold result_narrowing in H5.
          exists x0.
          unfold orv_atm.
          rewrite decode_encode.
          rewrite H5.
          reflexivity.
        }
      }
    }
  }
}
Qed.