The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

> > By the way, I would be curious to known whether there exists an
> > unprovable (without extensionality) equality between two nat's...
>
> Certainly. Let's have an example where the
> functions aren't applied. Try
>
> forall (f : (Nat -> Nat) -> Nat),
>  f (fun x => x + 0) = f (fun x => 0 + x)

Well put! This counterexample in some way also suggests the way out.  
We should only quantify over functions which respect extensional  
equality:

forall f : (Nat -> Nat) -> Nat , (forall g h : Nat -> Nat . forall  
i:Nat , g i = h i -> f g = f h) ->
        f (fun x => x + 0) = f (fun x => 0 + x)

and this is easy to prove. However, whenever you instantiate the  
quantification you are now obliged to show that the function you  
instantiate with preserves extensional equality. Luckily, this will  
always hold if you consistently follow this scheme...

If there is something you can always prove, you may want to build it  
into your theory. This is the motivation behind OTT, I'd say.

Cheers,
Thorsten

> All the best
>
> Conor
>
> PS In the last few days, I've managed to
> construct the extensional universe from
> "Observational Equality, Now!" (Altenkirch,
> McBride, Swierstra, 2007) in Coq. By
> reflecting on this universe, one can build
> an equality which is extensional and
> substitutive, whilst retaining canonicity
> for datatypes. Hopefully, extensionality
> will soon stop being such a painful source
> of trouble.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


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.