The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Adam Chlipala wrote:
> Wan Hai wrote:
>> I want to prove that:
>>
>> forall m1 m2 n, fc n (fun x=>m1*m2*x) = fc n (fun x=>m2*m1*x)
>>
>> It is obviously right. [...]
>>
>> Is there another way to prove this not using the extensionality axiom?
>>   
> 
> It turns out that (as far as I know), in base CIC without axioms, the
> proposition is not even right, let alone "obviously right." :-)
> 

Right. (fun x=>m1*m2*x) = (fun x=>m2*m1*x) is not provable in Coq, but
it doesn't mean that you cannot prove the lemma about fc.
Indeed, it is very easy to prove that fc is "extensional" (i.e. returns
the same nat if applied to extensionaly equal functions):

Lemma fc_ext : forall n f g, (forall n, f n = g n) -> fc n f = fc n g.
induction n; simpl; intros; auto.
Qed.
Then, take (f:=fun x=>m1*m2*x) and (g:=fun x=>m2*m1*x) and the premisse
is provable.

As a rule of thumb, having functional extensionality (or not having it)
changes equalities on functions, but not equalities on first order
inductive types (like nat).

Bruno Barras.