The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.org>]

Hello,


Le 18 oct. 2010 à 23:02, Vladimir Voevodsky a écrit :

> Hi, I have the following two questions:
> 
> Q.1 Is it  impossible to prove in Coq that any two functions from empty 
> type to empty type are equal ?
> 
> Q.2 Is it possible to preserve extraction after adding the functional 
> extensionality axiom ((forall x:X, f x = g x) -> f =g)?

I do not have fundamental information to add to what has been said, 
especially on 1. To make things more concrete
for question 2 :

The axiom will indeed not break to properties of the extracted programs. 
There is however some subtlety hidden here,
since there are computational elimination schemes for equality proofs :

eq_rect
     : forall (A : Type) (x : A) (P : A -> Type),
       P x -> forall y : A, x = y -> P y

But the extraction is "clever" enough to give a computational translation of 
this scheme :

Coq < Extraction eq_rect.
(** val eq_rect : 'a1 -> 'a2 -> 'a1 -> 'a2 **)

let eq_rect x f y =
  f

So the fact that an equality proof comes from an axiom like extentionality 
will not appear in the extracted
program


I hope I have not obscured things :)

Best,


Benjamin