20.5 Add a ring structure

It can be done in the Coqtoplevel (No ML file to edit and to link with Coq). First, Ring can handle two kinds of structure: rings and semi-rings. Semi-rings are like rings without an opposite to addition. Their precise specification (in Gallina) can be found in the file

tactics/contrib/polynom/Ring_theory.v

The typical example of ring is Z, the typical example of semi-ring is nat.

The specification of a ring is divided in two parts: first the record of constants (Å, Ä, 1, 0, ) and then the theorems (associativity, commutativity, etc.).

Section Theory_of_semi_rings.

Variable A : Type.
Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : A.
(* There is also a "weakly decidable" equality on A. That means 
  that if (A_eq x y)=true then x=y but x=y can arise when 
  (A_eq x y)=false. On an abstract ring the function [x,y:A]false
  is a good choice. The proof of A_eq_prop is in this case easy. *)
Variable Aeq : A -> A -> bool.

Record Semi_Ring_Theory : Prop :=
{ SR_plus_sym  : (n,m:A)[| n + m == m + n |];
  SR_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];

  SR_mult_sym : (n,m:A)[| n*m == m*n |];
  SR_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
  SR_plus_zero_left :(n:A)[| 0 + n == n|];
  SR_mult_one_left : (n:A)[| 1*n == n |];
  SR_mult_zero_left : (n:A)[| 0*n == 0 |];
  SR_distr_left   : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
  SR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p;
  SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
}.

Section Theory_of_rings.

Variable A : Type.

Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : A.
Variable Aopp : A -> A.
Variable Aeq : A -> A -> bool.


Record Ring_Theory : Prop :=
{ Th_plus_sym  : (n,m:A)[| n + m == m + n |];
  Th_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
  Th_mult_sym : (n,m:A)[| n*m == m*n |];
  Th_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
  Th_plus_zero_left :(n:A)[| 0 + n == n|];
  Th_mult_one_left : (n:A)[| 1*n == n |];
  Th_opp_def : (n:A) [| n + (-n) == 0 |];
  Th_distr_left   : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
  Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
}.

To define a ring structure on A, you must provide an addition, a multiplication, an opposite function and two unities 0 and 1.

You must then prove all theorems that make (A,Aplus,Amult,Aone,Azero,Aeq) a ring structure, and pack them with the Build_Ring_Theory constructor.

Finally to register a ring the syntax is:

Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ...cn ].

where A is a term of type Set, Aplus is a term of type A->A->A, Amult is a term of type A->A->A, Aone is a term of type A, Azero is a term of type A, Ainv is a term of type A->A, Aeq is a term of type A->bool, T is a term of type (Ring_Theory A Aplus Amult Aone Azero Ainv Aeq). The arguments c1 ...cn, are the names of constructors which define closed terms: a subterm will be considered as a constant if it is either one of the terms c1 ...cn or the application of one of these terms to closed terms. For nat, the given constructors are S and O, and the closed terms are O, (S O), (S (S O)), ...

Variants:

Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ].
There are two differences with the Add Ring command: there is no inverse function and the term T must be of type (Semi_Ring_Theory A Aplus Amult Aone Azero Aeq).
Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T.
This command should be used for when the operations of rings are not computable; for example the real numbers of theories/REALS/. Here 0+1 is not beta-reduced to 1 but you still may want to rewrite it to 1 using the ring axioms. The argument Aeq is not used; a good choice for that function is [x:A]false.
Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T.

Error messages:

Not a valid (semi)ring theory.
That happens when the typing condition does not hold.

Currently, the hypothesis is made than no more than one ring structure may be declared for a given type in Set or Type. This allows automatic detection of the theory used to achieve the normalization. On popular demand, we can change that and allow several ring structures on the same set.

The table of theories of Ring is compatible with the Coq sectioning mechanism. If you declare a Ring inside a section, the declaration will be thrown away when closing the section. And when you load a compiled file, all the Add Ring commands of this file that are not inside a section will be loaded.

The typical example of ring is Z, and the typical example of semi-ring is nat. Another ring structure is defined on the booleans.
Warning: Only the ring of booleans is loaded by default with the Ring module. To load the ring structure for nat, load the module ArithRing, and for Z, load the module ZArithRing.