The Coq mailing list

["Wan Hai" <wan.whyhigh AT gmail.com>]

Hi, Florian

Yes, you are right.

The question I asked is an abstract version of what I want to prove.
In my first try, the "rewrite" step did not work, so I used the
extensionality axiom to do so. At that time, I thought rewriting
inside a function, such as rewrite m1*m2 to m2*m1 in (fun n=>m1*m2*n),
is not allowed in Coq. Now I know it works.

Maybe the solution Bruno Barras gave is more general.

Thanks a lot!

On Mon, Jun 2, 2008 at 3:11 PM, Florian Hatat 
<florian.hatat AT ens-lyon.fr>
 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.
>
> 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.
>
> By the way, I would be curious to known whether there exists an
> unprovable (without extensionality) equality between two nat's...
>
> --
> Florian,
> http://openweb.eu.org/
> http://www.linux-france.org/
>
>
>



-- 
Best regards,
Hai Wan