The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi

> 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 :-(

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.

> Theorem toto: forall (b:R), (a*a*a-b+b=a)%R.
> intros.
> ring_simplify.
> unfold pow.
> (* here rewrite H fails *)
> ---

In this particular example you can make use of the capability of
ring to do some restricted form of rewriting modulo assoc/comm with

ring_simplify [H]

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

--
Laurent