The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

In that case you can redeclare the Field tactic on reals (and so the 
Ring tactic) :
Actually the Field tactic for reals is defined as follow (in 
contrib/setoid_ring/RealField.v) :
    Add Field RField : Rfield  (completeness Zeq_bool_complete, 
power_tac R_power_theory [Rpow_tac]).
                                                                                                           
^ here is your problem.


Just earase it.

Require Import Reals.
Add Field RField : Rfield  (completeness Zeq_bool_complete).

Variable a:R.
Hypothesis H: (a*a=1)%R.

Theorem toto: forall (b:R), (a*a*a-b+b=a)%R.
intros.
ring_simplify.
>>>    a*a*a = a.

   Benjamin
Sylvie.Boldo AT inria.fr
 wrote:

> 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