The Coq mailing list

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

Sylvie.Boldo AT inria.fr
 wrote:

  Hello Sylvie,
    This is not really an answer to your questions but it will solve 
your problem :
       The ring(_simplify) tactics are able to compute a normal form 
modulo rewriting, the rewriting equality should be of the
         following form :   n*M = P,   where n is a number, M a 
monomial and P a polynomial.
       So you can prove your goal as follow:
            intros; ring_simplify [H].
        >> a = a
            trivial.
        >> Proof completed.

       Or simply :
           intros; ring [H]. 
       >> Proof completed.

You can give more than one hypothesis : ring [H1, H2, H3].

  Hope this help.
      Benjamin

   

> Hello,
>
> I have just begun using coq V8.1 and the new ring tactics. I am 
> currently fighting with the normal form given by the tactic 
> ring_simplify. More precisely, I have discovered that it now uses the 
> notation "^" when the same term is multiplied by itself. That is nicer 
> to look at, but very difficult to use afterwards. When unfolded, a^2 
> becomes a*(a*1), therefore rewriting on a*a is impossible :-(
>
> Simplified example:
> ---
> Require Import Reals.
> Variable a:R.
> Hypothesis H: (a*a=1)%R.
>
> Theorem toto: forall (b:R), (a*a*a-b+b=a)%R.
> intros.
> ring_simplify.
> unfold pow.
>  (* here rewrite H fails *)
> ---
>
> This is not impossible to solve (with nicely chosen replace), but it 
> is a real pain for complex a and b.
>
> Would it be possible that the chosen pow (the one I get when I use 
> ring_simplify), when unfolded, would give the expected answer ?
> In fact, I would like a^2 to be a*a...
>
> Regards,
>
> Sylvie Boldo