The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT sophia.inria.fr>]

Hi Russell,

 thanks for your question, which is an occasion of writing down a few 
guideposts for using "newring."

> What's the relationship between setoid ring, and Benjamin and Assia's 
> newring tactic 
> <http://www-sop.inria.fr/marelle/Assia.Mahboubi/rech-eng.html>?
They are the same : newring was the (rather ugly) name of the first 
prototype, setoid ring is the name of the tactic in the new 
implementation of this work by Bruno Barras, which is available in the 
last beta release.

At the time being, two different implementations of the ring tactic are 
available in Coq8.1beta.
The first one, the "old" ring tactic is the one documented in the 
Reference manual.
The way the "new" one is implemented is described in the article you 
mentionned, but you will not find any information about the current 
syntax in the paper.
How to play with this new version of the tactic, in Coq8.1beta :

1)You should first begin with :
--
Require Import Pol.
Require Import Setoid.
Require Import Ring_tac.
Require Import ZRing_th.
--
2)Define a record gathering the ring constants and the equality relation 
which equips the ring structure you are interested in , using :
--
Definition Aring : ring_theory A0 A1 Aplus Amul Asub Aopp Aeq.
--
Above, the carrier A of the ring is implicit, A0 is the neutral for 
addition, A1, the neutral for multiplication, Aplus ,the additive 
law,... and Aeq is the equality relation which may be either a 
previously declared setoid equality or the Leibnitz equality (@eq A) .
To complete this definition Coq will ask you to provide proofs for the 
axiom of a commutative ring structure.

3) In the case Aeq is a setoid equality, you should declare the ring 
operations as morphisms before step 4).

4) Now you can declare the ring structure.
There are two situations :
4a) You are working with an *abstract* ring structure (in the sense 
defined in the Reference Manual), like it is the case for the real 
numbers of the standard library. In this case, the operations declared 
above have no computational content, they are just symbols.
The ring structure is declared by the command :
--
Add New Ring AR : Aring Abstract.
--
Above, AR is any name you may  choose for this ring structure.
In this case, the coefficients used in the syntaxification will be the 
default choice, Z (the one of ZArith).

4b) You are working with a *computational* ring structure. For example 
you may think of the rational numbers of the QArith standard library.
In this case, the constants and operations declared  for the ring 
structure will be used in the syntaxification process to build the 
coefficients of the polynomials.
Hence you need to provide two extra arguments when declaring the ring  
structure : a proof concerning  the decidable equality, which is needed 
for the decision process, and a tactic providing the description of the 
constants.
The first argument is of type

Aeq_ok: forall x y:A, Aeqb x y -> Aeq x y
where Aeqb : A -> A -> bool is the boolean equality  you would like to 
use for the decision.

The second argument is a tactic Acst, taking any term and returning the 
term itself in the case it is a ring constant you would like to lift in 
the syntaxified world and a flag NotConstant otherwise. For example if 
the ring is Z, you would probably like to lift any closed term of type Z 
which is build only with the constructors of the type Z and the type 
positive.

You can have a look at the file 
coq-8.1beta/contrib/setoid_ring/ZRing_th.v, where such a structure is 
defined for the ring of binary integers Z (and also for the semi-rings N 
and nat). It should give hints on the way such a tactic may be defined.

The ring structure is declared by the command :
--
Add New Ring AR : Aring Computational Aeq_ok Constant Acst.
--

5) Once the ring structure is declared, whatever version 
(computational/abstract, leibniz/setoid) of a ring you may be working 
with, and no matter how many ring structures you may have declared, the 
tactic is called by the "setoid ring" command.

Example :
---
Goal forall x y u v:A, Aeq (x + y + u + v) (u + v + y + x).
intros.
setoid ring.
Qed.
---
This is the current state of the syntax.
Of course, all comments on this are more than welcome.
Hope this helps,

Assia