19.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 filetactics/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, Q) and then the theorems (associativity, commutativity, etc.).
Record Semi_Ring_Constants [A:Set] : Set :=
{ SRplus : A -> A -> A;
SRmult : A -> A -> A;
SRone : A;
SRzero : A;
SReq : A -> A -> bool
}.
Record Semi_Ring_Theory [A:Set; C:(Semi_Ring_Theory A)] : 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;
}.
Record Ring_Constants [A:Set] : Set :=
{ Rplus : A -> A -> A;
Rmult : A -> A -> A;
Ropp: A -> A;
Rone : A;
Rzero : A;
Req : A -> A -> bool
}.
Record Ring_Theory [A:Set; C:(Ring_Constants A)] : 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 |];
}.
To define a ring structure on A, you must provide an addition, a multiplication, an opposite function and two unities 0 and 1. You pack them with the
Build_Ring_Constants constructor.You must then prove all theorems that make (A,C) a ring structure, and pack them with the
Build_Ring_Theory constructor.Finally to register a ring you must type :
Add Ring a c t [ c1 ...cn ].
where a is a term of type Set, c is a term of type (Ring_Constants a), t is a term of type (Ring_Theory a c). c1 ...cn, are the names of constructors who 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 construtors are S and O, and the closed terms are O, (S O), (S (S O)), ...
Warning: a, c and t must be transparent constants (see section 5.2.5). You must save them with the command Defined rahter than Save.
Variants:
-
Add Semi Ring a c t [ c1 ...cn ].
Here c must be a term of type (Semi_Ring_Constants a), and t a term of type (Semi_Ring_Theory a c).
Error messages:
- Not a valid (semi)ring theory. That happens when the condition on a, c and t does not hold.
You can have a look at the scripts NatRing.v, ZRing.v and Bool_Ring.v to see examples of such definitions.
After the Add Ring command, you can use polynom for the declared ring or semi-ring in the way presented in the previous answer.
Currently the hypothesis is made than no more than one ring structure may be declared for a given type in Set. 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. Anyway the source code of Ring was written for didactic purposes, it is or should be clear and well documented, then you can easily hack it do to whatever you want.
The table of theories of Ring is compatible with the Coq sectionning mechanism. If you declare a Ring inside a section, the declaration will be thrown away when closing the section. And when you require a compiled file, all the Add Ring commands of this file that are not inside a section will be loaded.