The Coq mailing list

[Sylvie.Boldo AT inria.fr]

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


--
Sylvie Boldo, projet ProVal, INRIA Futurs