Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] two related questions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] two related questions


chronological Thread 
  • From: Conor McBride <conor AT strictlypositive.org>
  • To: Adam Chlipala <adam AT chlipala.net>
  • Cc: Vladimir Voevodsky <vladimir AT ias.edu>, Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] two related questions
  • Date: Mon, 18 Oct 2010 23:30:11 +0100

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




Archive powered by MhonArc 2.6.16.

Top of Page