The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi

On 2 Jun 2008, at 14:11, Florian Hatat wrote:

> Hi,
>
> Wan Hai a écrit :
> > forall m1 m2 n, fc n (fun x=>m1*m2*x) = fc n (fun x=>m2*m1*x)
> > (...)
> > Is there another way to prove this not using the extensionality axiom
> In this particular case (since you can rewrite using the equality
> m1*m2*x = m2*m1*x, see the mult_comm lemma in Mult), you do not  
> need the
> extensionality axiom.

Which way does * associate? If to the left,
then the two functions are provably equal.
If to the right, then they are extensionally
but not provably equal.

> Theorem th1 : forall m1 m2 n, fc n (fun x=>m1*m2*x) = fc n (fun  
> x=>m2*m1*x).
> Proof.
> intros m1 m2 n.
> rewrite (mult_comm m1 m2).
> reflexivity.
> Qed.

I suspect that the above proof relies on left
association. Even so, where extensionally equal
functions are used only by applying them,
one can expect to construct an inductive
argument like Bruno's.

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

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.