The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 7 Aug 2006, Conor McBride wrote:

> The argument Fabrice cites from Wikipedia is valid when == is taken to be the 
> conventional alpha-beta-eta equality of the lambda-calculus. If you pick a 
> fresh variable x, and confirm f x == g x, that's the same deal as checking 
> \x.f x == \x.g x. Russell's worry about bindings isn't a problem in this 
> free-to-bound direction: if you're equal wrt the same fresh free variable, 
> then it's trivial to pick alpha-equivalent lambda-abstractions, as done 
> above. It's the other way where you have the trouble: if \x.f x == \y. g y, 
> then you don't necessarily get f x == g y.

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.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''