The Coq mailing list

[Pablo Argon <pargon AT cadence.com>]

Eduardo Gimenez wrote:
> 
> 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.

> 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)).
> >

Dear Eduardo and Coq users, 
                I understand your remark and agree that the 
"simple equality" I meant cannot be the Coq's eq relation, is
an  <<intentional equality>>.

In fact, what I was looking for is a kind of "Proof Irrelevance
principle",
allowing me to prove, for example;

Lemma PfIrrelevance :
    (A:Set)(P:Prop)(f:P->A)(q1,q2:P) (f q1) = (f q2).

In my understanding, even if q1 and q2 are different proofs of a given
property, in what sense the value of f may depend on this, in order to 
make the equality (f q1) = (f q2) not provable ?

In practice, when dealing with dependent types we need to prove
something in the taste of:

Lemma HowtoRewriteHere :
(A:Set)(B:A->Prop)
  (a,a':A)(a=a')->(t,t':(sig A B))
    (b:(B a))(t=(exist A B a b))->
      (b':(B a')) (t'=(exist A B a' b'))-> t=t'.

in order to rewrite and go further.

Perhaps I'm missing something deep here...

Cheers,
        Pablo