The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi Adam, Vladimir, and all,

On 18 Oct 2010, at 22:25, Adam Chlipala wrote:

> Vladimir Voevodsky wrote:
> > Q.1 Is it  impossible to prove in Coq that any two functions from  
> > empty type to empty type are equal ?
>
> I would assume this requires an extensionality axiom like below, but  
> I'll wait for a more informed person to answer this part. :)

That's the case.

If there were an axiom-free proof that all 0 -> 0 functions are
propositionally equal, we would have a proof in the empty context
that

  id = magic 0

where magic X : 0 -> X eliminates its argument.

That proof can only be refl, but id is not convertible with magic 0,
so there ain't no such proof.

> > Q.2 Is it possible to preserve extraction after adding the  
> > functional extensionality axiom ((forall x:X, f x = g x) ->  f =g)?
>
> I think this poses no problems, because this axiom would live in the  
> [Prop] universe (because of the use of [=]), and extraction erases  
> everything in that universe, anyway.

Right again. Extensionality *axioms* mess up the computational
properties of open terms, but they pose no threat to extraction.
I'll try to find a suitable reference for that, but don't be
shy if you know one!

It might be possible to fix this particular issue, for 0 -> 0,
by adding the eta-rule for functions and identifying all
elements of the empty type definitionally. (In Epigram 2, all
elements of 0 -> 0, where 0 is the set of proofs of False,
are definitionally equal.)

Note, however, that you don't get far past 0 -> 0 by trying
to make the definitional equality more extensional. If you
identify all elements of 0 -> 2 definitionally, then
(fn x => true) = (fn x => false) and definitional equality
collapses under a false hypothesis, normalisation fails, etc.

Hoping this helps

Conor