[Agda] Proof irrelevance and self-realizing formulas

[Peter Hancock]

Andrej Bauer wrote:
> I always thought
> it was a bit strange that Coq wants me to tell which things are
> computationally irrelevant--it should know by itself.

I doubt this is always possible.  Let f(n) be the truth-value of the
n'th instance of Goldbach's conjecture (or some other "Brouwerian"
conjecture).  Let P be some random "boring" formula, such as, er,
Goldbach's conjecture, and Q be an "interesting" one, full of
disjunctions, existential quantifiers, and whatnot. Now define
R to be (all n : N) if f(n) then P else Q.  The boringness oracle
would now have to decide Goldbach's conjecture in order to tell
whether R was boring.

Of course,
> Perhaps, rather than thiking about adding a Prop to Agda, it would be
> worthwhile thinking about having a "thinning" phase in Agda's
> extractions, like RZ does. The idea is to chop off "boring" parts of
> types and realizers/proofs. 
might be possible (but I'm not sure I would want it).

What I'm picking up from this nice discussion is the difference
between a proof being computationally uninteresting, and intellectually
interesting.  I understand that Alex Wilkie has spent a lot of his
considerable intellectual energy in figuring out whether Wiles' proof
of Fermat's Last Theorem can be coded in Peano Arithmetic.  Perhaps
we should put him out of his misery and tell him it is just \x.*,
and can be written in a very small fragment of PA?

Hank