The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

AUGER Cédric wrote:
> I have never used tactic ring, but why using such a name while (nat, 0, +,
> *) is not a ring?
>
>   
The general setting for ring to work is to have a combination of 
operations and
constants that constitute a ring.  The way ring works is to view all 
operations as
polynomial expression and to perform symbolic computation to recognize that
two syntactically different polynomial expressions are actually the same.

When the operations you have at hand do not constitute a ring, you can 
still work
with a semi-ring structure (the same as a ring, but with the opposite 
function)
using the same approach.  For this reason, the same tactic,
named "ring" will work both for rings (like the Z, Zplus, Zopp, Zmult, 
0%Z, 1%Z) and
for semi-rings (but here there is only nat, plus, mult 0%nat, 1%nat).

Plain users can actually configure the ring tactic so that it will be 
able to manipulate
formulas in their favorite type, using their favorite operations acting 
as addition,
multiplication, opposite, and constants used as 0 and 1 and comparing 
expressions
with respect to an arbitrary equivalence relation (not just equality).   
Please look at
the documentation for the commands "Add Ring" and "Add SemiRing" in the
Coq manual.

In an earlier version of Coq, expressions that contain 0%nat, 1%nat, 
plus, mult,
and S could not be handled by the ring tactic (because obviously S is 
not one of the
ring operations) so we had proposed a hack to transform all occurrences 
of (S e) into
(1 + e) prior to calling the regular ring tactic (this hack is described 
in the CoqArt,
tactic S_to_plus_simpl).  The tactic ring_nat was a combination of 
S_to_plus_simpl
and ring. When ring was re-designed, this hack became unnecessary and
ring_nat was not preserved.

Yves