The Coq mailing list

[Conor McBride <ctm AT Cs.Nott.AC.UK>]

Hi Russell

roconnor AT theorem.ca
 wrote:
> On Mon, 7 Aug 2006, 
> roconnor AT theorem.ca
>  wrote:
>
> > I didn't realize the lambda-calculus was so bizzare.
> >
> > In Coq, I can prove (forall x:list nat, bubblesort x = quicksort x).  
> > From this I can get (bubblesort x = quicksort x) inside the context 
> > [x:list nat]. So now don't we have f x = g x for a fresh varaible x?  
> > The only constraint on x is its type, so x is as free as it is ever 
> > going to get.
>
> Oh wait, I'm talking about = for Leibniz equality, and you are talking 
> about == for alpha-beta-eta equality.  The difference being that 
> Leibniz equality is more or less alpha-beta-delta-iota equality?

Yes, we're talking about different equalities.

In a non-empty context, Leibniz (or some other propositional) equality 
is more than alpha-beta-delta-iota equality. Typically, you'll find that 
under the hypothesis x:nat, you'll have x+0 and 0+x being Leibniz equal 
(proof by induction), but not alpha-beta-delta-iota equal. There's an 
inevitable gap between the expressions that the machine can see are 
equal by computation alone and the expressions which you can prove are 
equal by offering sophisticated (especially inductive) forms of evidence.

As it happens, for the propositional equality in Coq, this gap vanishes 
/in the empty context/. This is not necessarily a good thing.

All the best

Conor


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.