[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Martin Escardo]

On 07/01/14 10:01, Frédéric Blanqui wrote:
> Nowadays, one can automatically certify in proof assistants like Coq or
> Isabelle/HOL quite complex termination proofs (see the website of the
> termination competition http://termcomp.uibk.ac.at/termcomp/home.seam).
> So, it would be a pity not to take advantage of this for making the life
> of proof assistants users easier, and allow them to define functions (or
> enrich the equivalence on types) in ways that can hardly (or cannot) be
> translated into eliminators. This is for instance the case of function
> definitions based on general rewriting theory. This of course may raise
> problems for making sure that such definitions are consistent, but it is
> another (interesting) problem.

The problem is that if you accept general recursive terminating
definitions, you are in fact realizing new axioms that are not
available in MLTT.

For example, once I and Paulo Oliva defined Bar Recursion in Agda (by
disabling non-termination checking in a short module) to realize the
Double Negation Shift (DNS), and used this to prove a form of the
Infinite Pigeonhole Principle, so that canonicity for ground types is
retained.

However, the DNS is certainly *not* provable in MLTT (in any of its
flavours).

Similarly, you can realize other principles by having general
recursion, such as the uniform continuity (UC) of all functions
(N->Bool)->N.

And so on.

Even assuming that this wouldn't violate consistency, you have a
problem: while UC may be consistent with Univalence (UA), it certainly
negates excluded middle, and the HoTT people want HoTT to be
compatible with excluded middle (EM), and with choice too (AC), which
it is, but not if you add something like UC.

I am not saying that your termination checker will be able to check
the termination of UC. But it may check the termination of a realizer
of an axiom that contradicts EM or AC, or even UA.

Also, even if you forget about HoTT, it is not clear what new axioms
you are adding when you allow general recursion, and the supply of new
axioms you get will (necessarily) depend on the particularities of
your termination checker (as there is no general termination checker),
and so we won't be sure precisely what axioms we are adding to
MLTT in this way.

That's why, as Thorsten says, it would be very good to have as a
meta-theorem that any termination-checked Agda program can be
in principle translated to eliminators (even if we decide not to do
that in practice).

M.