The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Dear Pablo,

This "simple equality" says that any pair of programs producing the
same output on any input has the same source code. In particular, taking
A=B=(list nat),f =quicksort and g=mergesort, you claim that both mergesort
and quicksort are the same program. That's not true, but you can add it as an
axiom without compromising Coq's consistency.

Best wishes,
Eduardo.

Le mar, 16 mai 2000, Pablo Argon a écrit :
> Hi all,
>       I wonder how to prove this simple equality :
> 
> Theorem ff_is_gg : (A,B:Set;ff,gg:A->B)
>   ((x:A)(ff x)=(gg x))<->([x:A](ff x))=([x:A](gg x)).
> 
> Thank you in advance, Pablo
-- 
----------------------------------------------------------
Eduardo Gimenez                Tel :   (33) 1 30 97 25 13 
Trusted Logic SA                Std :   (33) 1 30 97 25 00 
5, rue du Bailliage               Fax :   (33) 1 30 97 25 19 
78000 Versailles               Web : www.trusted-logic.fr 
----------------------------------------------------------