The Coq mailing list

[Sylvie.Boldo AT inria.fr]

Hi,

Thanks for the replies ! I missed the reference to ring[H] in the manual.
Unfortunately, it solves the simplified example, but not the real one 
:°-(

Less simplified example:
--
Require Import Reals.
Variable f:R->R.
Hypothesis H: forall (a b:R), (f a*f b=f (a*b))%R.

Theorem toto: forall (a b c:R), (f(a)*(f(a)-b)+b*f(a)=f(a*a))%R.
--

I would have to use ring [H a a] but it is highly unpractical.
In fact, I was using "repeat rewrite <- H" so in practise, I would need to 
use [H a b, H b -a, H b a, H c a....] with "big" a,b & c...

> Yes it is a small incompatibility with the previous ring_simplify
> but we thought that the benefit of having more readable outputs was
> worth it. Anyway having or not a power function is a flag in the
> primitive  ring tactic. It is just activated when applied to R.
> If you happen to have too much problem, we could turn in down.
Well, it IS more readable, no doubt about it. I see 2 possible answers 
that would solve my problem:
 * having a flag to turn it down if wanted
 * using a different pow such that a^2=a*a, knowing that this pow will 
be used in a^b with b >=2 (this is the real case as ring_simplify will use 
pow only when it is at least a square.


> Having full associative commutative rewriting in Coq would
> of course be nicer, I hope it will come with coq8.2 :-)
I fully agree :-)

Sylvie Boldo


--
Sylvie Boldo, projet ProVal, INRIA Futurs