[Agda] Proof irrelevance and self-realizing formulas

[Andrej Bauer]

Dear Conor and Peter,

I probably don't know what you're really talking about, but it sounds
to me like "self-realizing" propositions might be worth a look.

Let us temporarily forget the interpretation

"P is proof irrelevant" = "all proofs of P are equal"

because we don't like equality of proofs. An alternative
interpretation of "P is proof irrelevant" is:

"Anything that can be computed using a proof p : P, can also be
computed without it."

The extreme case of this is that an inhabitant of P can be computed
without using p, i.e., an inhabitant of P can be constructed out of
thin air, provided P has inhabitants. Just to make discussion less
prone to misunderstanding let us not use the phrase "proof
irrelevant". Call a proposition P "self-realizing" if an inhabitant of
P can be computed, provided one exists.

Self-realizing propositions are closed under false, truth,
conjunction, universal quantification and implication. Furthermore,
decidable propositions are self-realizing. A function rz computing a
proof of a self-realizing proposition can be defined as follows (it
takes an environment mapping free variables to their values and a
proposition):

rz env false = do some magic, this can't happen
rz env true = *
rz env (p and q) = (rz env p, rz env q)
rz env (forall x, p) = lambda x', rz ((x,x')::env) p
rz env (p -> q) = lambda _, rz env q

Please excuse my non-Agda notation. If p : A -> Prop is a decidable
proposition and d inhabits forall x : A, p x or not (p x) then

rz env (p t) =
  match d (eval env t) with
    Left r -> r
    Right _ -> "not (p x)" cannot happen, do some magic

So we have covered Pi01 propositions. I am being pretty vague here, I
hope you can see what the idea is. Perhaps an example can help.

Goldbach's conjecture is of the form:

forall n : nat, exists j, k <= n, prime j /\ prime k /\ 2 * n + 4 = j  + k.

The inner "exists" is decidable. Let check_goldbach be the obvious
algorithm which takes n and looks for prime j, k <= n such that j + k
= 2 * n + 4. Now, if Goldbach's conjecture has any inhabitants, then

lambda n : nat, check_goldbach n

inhabits it as well.

But I don't know if Agda can deal with this sort of thinking (which
comes from realizability). It seems to me that some meta-level support
is needed (i.e., in the Agda engine), especially for the "do some
magic" part above.

Am I making any sense to you?

Andrej