The Coq mailing list

[Conor McBride <ctm AT cs.nott.ac.uk>]

roconnor AT theorem.ca
 wrote:
> Can anyone provide me with a reference that shows that
>
> forall (T U : Set) (f g : T -> U),
> (forall x : T, f x = g x) -> (fun y : T => f y) = (fun y : T => g y)
>
> is not provable in Coq?

Not off hand, but it's a simple corollary of strong normalization and the
property that every normal form in the empty context is canonical.

Just take
  + defined by recursion on its first argument
  f = fun x : Nat => x + 0
  g = fun x : Nat => x

There's an inductive proof that these functions return equal values for all x:
plug this into the above and normalize. You must get a canonical proof
constructed by reflexivity, which only proves intensionally equal things
equal. But (fun y : Nat => y + 0) and (fun y : Nat => y) are not intensionally
equal. Oops.

Now, you mightn't mind losing the property that every equality proof in the
empty context is refl, but the tricky bit is dropping that property for
equality without losing it also for ordinary datatypes.

Working on it. A major clue can be found in Thorsten Altenkirch's LICS '99
paper...

Conor

--
http://www.cs.nott.ac.uk/~ctm

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.