Algebraic Hierarchy

Get Complete Project Material File(s) Now! »

When doing mathematics, the objects we handle may share some structure, for example we can recognize many examples of groups, rings and fields in the literature. In fact, there is a huge number of diﬀerent structures which one can identify and which all have their own theory. When formalizing mathematics, it is very important to implement the sharing of mathematical structure, because we do not want to keep repeating the same proofs all over the developments. In programming languages, sharing is often achieved by abstraction: we derive all we need from basic facts, and then we specialize to our situation. Moreover, several mathematical structures may share more or less properties, which means the code has to be modular. For example, rings inherit all the properties of commutative groups, so rings should share some theory with commutative groups, which we do not want to duplicate. The purpose of an algebraic hierarchy is to organize mathematical structures and their theories in order to maximize sharing.
In this Chapter, we describe the constitution of the SSReflect algebraic hier-archy, essentially as it was made and described in [36]. A huge part of our work (cf Chapter 4) is based on this hierarchy, and reuses the same methodology to achieve the task of building an extension of this hierarchy.
We introduce a lot of important vocabulary in this chapter. In Section 2.1 we explain what we mean by axiom. Section 2.2 explains the diﬀerent structures the SSReflect library contains and what choices of operators, relations and axioms have been made. Section 2.3 gives a short insight on how the structure information is retrieved when needed.

On the meaning of axiom

One very important thing is to clarify first the use of the word axiom. In model theory and logic (as in [54, 30]), the axioms are the formulas from which we derive a theory using the rules of the logic (we describe this more formally in Section 10.1). In Coq, the word axiom can refer to the vernacular command Axiom, which is used to add an axiom to Coq itself. However, we use the word axiom to describe a property of an interface. Unlike for Coq axioms, we can and we must provide a proof of the axiom when we define a structure. For example, in Section 1.3 we provide a proof eqnP of the axiom eqP of the interface for discrete types, which is described
Remark
When used inside a module type, the key word Axiom takes a diﬀerent meaning and becomes a statement that has to be satisfied to implement the module, which is relatively close to our use.
In our work, we never make use of Coq axioms. Hence, from now on, the word “axiom” always refers to properties of structures.

Choice of interfaces

In SSReflect various algebraic structures are represented by records, i.e. elements of record types. In Coq record types are implemented using an inductive type with one constructor. The arguments of this constructor are named the fields of the record and the projections are the functions that returns the fields of a record. Their type is hence: “record type” → “type of the field”.
In the specific case where the record type characterizes an algebraic structure, we call this record type an interface, and the elements of an interface the corresponding structures. This diﬀers a little bit from Coq terminology where the vernacular command Structure is a synonym for Record: we use it only for records that have an algebraic meaning.
In the SSReflect library, structures have two fields: the carrier, whose type is Type and the class of the structure. The class is a record which must contain both the instantiation of the signature and proofs of the axioms of a class. The signature is the name and type of the operators and relations, and the axioms are formulas that explain the properties of the operators and characterizes the relations between them. The inheritance of interfaces is implemented by dividing the class in two parts: the first part is the class from the super-interface, while the second part, called mixin, is a record that contains the new operators and relations and the proofs of the new axioms. A complete description of the packaging of algebraic structure is given in [37, 36].
We give an example with the four first layers of the algebraic hierarchy in Fig-ure 2.1. The Figure 2.2 zooms out and gives a snapshot of the principal structures we use from the algebraic hierarchy. We then regroup in Figure 2.3 the signature that each new mixin adds to the previous ones, together with some useful definitions.
All the instances of these structures are discrete, i.e. based on a type with decidable equality. The operator for the equality decision procedure is denoted by (_ == _), and satisfies the following property:
Lemma eqP : forall (T : eqType) (x y : T), reflect (x = y) (x == y).
This axiom asserts that given two terms of type T, the equality decision procedure outputs true if and only if the two terms are equal (for the – so called – Leibniz equality, also known as propositional equality).
They are also equipped with a choice operator xchoose of type:
Definition xchoose : forall (T : choiceType) (P : T -> bool), (exists x, P x) -> T.
which satisfies the two following properties:
Lemma xchooseP : forall (T : choiceType) (P : T -> bool)
(xP : exists x, P x), P (xchoose T P xP).
Lemma eq_xchoose : forall (T : choiceType) (P Q : T -> bool)
(xP : exists x, P x) (xQ : exists x, Q x),
(forall x, P x = Q x) -> xchoose T P xP = xchoose T Q xQ.
These properties respectively ensure the correctness and uniqueness of the chosen element with respect to the predicate P.
For instance, in Coq, any countable type can be provably equipped with such a structure. This means we can take T to be the type Q of rational numbers.
The choice structure is fundamental to formalize both the comparison of Cauchy reals in Section 5 and the construction of the eﬀective quotient type in Section 7. However it is not crucial for quantifier elimination (Part III).
The zmodType structure of commutative groups comes with a number of nota-tions related to the additive notation of a commutative law, including those for iterated additions. The term x *+ n denotes (x + … + x) with n occurrences of x. Non constant iterations benefit from an infrastructure devoted to iterated operators (see [8]) and from a LATEX-style notation allowing various flavors of in-dexing: (\sum_(i <- r) F i) sums the values of F by iterating on the list r, while (\sum_(i \in A) F i) sums the values of F belonging to a finite set A, or (\sum_(n < i <= m | P i) F i) the values of F in the range ]n, m] which moreover satisfy the Boolean predicate P, etc. . . This infrastructure also provides a corpus of lemmas to manipulate these sums and split them, reindex them, etc.
The ringType structure of nonzero rings inherits from the one of commutat-ive group (and of its notations). In addition, it introduces notations for the mul-tiplicative law, including those for iterated products. The term x ^+ n denotes (x * … * x) the exponentiation of x by the natural number n. Again, we benefit here from the infrastructure for iterated operators: (\prod_(i <- r) F i) is the product of the values taken by the function F on the list r, etc. The infrastructure provides the theory of distributivity of an iterated product over an iterated sum. Finally, a ring structure defines a notation for the canonical embedding of natural numbers in any ring: n%:R denotes (1 + … + 1).
The ringType structure has variants respectively for commutative rings, rings with units (i.e. where it is decidable for an element to be invertible), commutative rings with units and integral domains. A field is a commutative ring with units in which every nonzero element is a unit.
Finally, scaling operations are available in module structures: a left module provides a left scaling operation denoted by (_ *: _) and a left algebra struc-ture defines an embedding of its ring of scalars into its carrier: (fun k => k *: 1). The algType (resp. unitAlgType) structure of algebra equips rings (reps. rings with units) with scaling that associates both left and right.
The decFieldType structure equips fields with a decidable first-order equational theory by requiring a satisfiability decision operator for first-order formulas on the language of rings.
The closedFieldType structure equips algebraically closed fields. It inherits from the decFieldType structure: a structure of algebraically closed field has to be built on a decidable field. This may disturb at first glance since the first-order theory of algebraically closed field enjoys quantifier elimination and is hence decidable.
This design choice in fact allows the user to specify explicitly the preferred decision procedure, which might not be quantifier elimination, for example in the case of finite fields.

READ Generalised Bogoliubov approximation

Structure inference

In SSReflect

When we consider elements of an algebraic structure, we implicitly refer to the elements of the carrier of the structure. For example, given a ring (R : ringType), taking an element (x : R) is in fact taking (x : Ring.sort R), where Ring.sort is the projection from the record to the carrier and is inserted implicitly by the coercion mechanism.
So for example, writing forall x y : R, x * y = y * x is typable and the result is expanded to the following form, when removing notations and showing implicit arguments.
forall x y : Ring.sort R, @mul R x y = @mul R y x because the multiplication operator has the following signature:
Definition mul : forall R : ringType, R -> R -> R
So far, there is no need for structure inference. Problems come when one does not use directly the appropriate structure. For example integers, as defined in Sec-tion 4.4.1, have a ring structure. We should be able to write forall x y : int, x * y = y * x, but int has type Type, not ringType (the ring structure of int was named int_Ring). Coq provide a mechanism to help the unification to find a solution. It is called canonical structure [77]. Indeed, the Coq system has to type:
forall x y : int, @mul ?ringType x y = @mul ?ringType y x
In this term, ?ringType is a meta-variable which is inserted automatically (through the implicit arguments and notation mechanism) and which has to be resolved by the unification algorithm of Coq.
Since x and y should have type (Ring.sort ?ringType) but have type int, this triggers a unification problem of the form:
Ring.sort ?ringType ≡ int
The structure int_Ring is the solution to this problem. By registering this canon-ical solution using the Canonical vernacular command, the unification algorithm will look for an entry corresponding to the pair (Ring.sort, int) in the canonical structure table and will find the entry int_Ring.
The command to print the canonical structure table in Coq is Print Canonical Projections and outputs results in the form:
key <- projection ( canonical structure )
So for our example with int being canonically a ringType, this gives:
int <- Ring.sort ( int_Ring )
The same problem occurs with inheritance. For example, addition has the follow-ing signature:
Definition add : forall Z : zmodType, Z -> Z -> Z
If we want to write (forall x y : R, x + y = y + x) where R still has type ringType, the system should reject the statement, because it should not be typ-able. When we remove the notations and put question marks in places where the system should be able to fill in the information through type inference, we get
forall x y : Ring.sort R, @add ?zmodType x y = @add ?zmodType y x.
Here, the unification algorithm encounters the unification problem:
Zmodule.sort ?zmodType ≡ Ring.sort R
But each zmodType has been declared has canonically a ringType, using the canon-ical structure Ring.zmodType. So the pair (Zmodule.sort, Ring.sort) was added to the canonical structure table and corresponds to the line
Ring.sort <- Zmodule.sort ( Ring.zmodType )
when using the command Print Canonical Projections.
The search for the appropriate structure is done at the core of the unification algorithm, which makes it very fast.

Comparison with other libraries tools and systems

The math classes development by van der Weegen, Spitters and Krebbers [81, 87] also builds a hierarchy of interfaces. There are two fundamental diﬀerences between it and the SSReflect one. The first diﬀerence is that it is defined in category theory and does not give much importance to the decidability of predicates such as equality or comparison, and it does require a choice operator, as the SSReflect algebraic hierarchy does.
The other diﬀerence is that the inference mechanism is based on type classes [80] rather than canonical structures [77]. In Coq, type classes where designed to solve the same kind of problems as canonical structures. Structure definition and inference using type classes is more flexible than with canonical structures in that they allow for multiple possible instances and backtracking. They use proof automation instead of being hard-wired into the unification algorithm, as described in [80], which is probably what makes it less eﬃcient in practice.
In Matita [1], unification hints [2] is also a mechanism to manually help the uni-fication to find solutions in case of failure, but in a more fine-grained way than canonical structures. They are even more flexible than type classes, in the way they let the user list the problems and their solution by hand. Combined with a good meta-language, they could be used to encode both type classes and canonical structures.

Table of contents :

I Infrastructure
1 Booleans in Coq logic
1.1 Reflection
1.2 Excluded middle and proof irrelevance
1.3 Interaction between bool and other types
2 Algebraic Hierarchy
2.1 On the meaning of axiom
2.2 Choice of interfaces
2.3 Structure inference
3 Polynomials
3.1 Polynomial arithmetic
3.2 Resultant
II Construction of numbers
4 Numeric rings
4.1 Extending the hierarchy
4.1.1 The Numeric Hierarchy
4.1.2 Discussion on the interfaces and their names
4.2 Signs, case analysis based on comparisons for reals
4.3 Intervals
4.4 Structure of integers and rational numbers
4.4.1 Integers
4.4.2 Rational numbers
5 Cauchy reals, algebraics
5.1 Cauchy reals
5.1.1 Cauchy sequences
5.1.2 Equality on Cauchy reals
5.1.3 Arithmetic operations and bounding
5.1.4 Reasoning with big enough values
5.1.5 Comparison with other implementations of reals
5.2 Algebraic reals
5.2.1 Decidability of comparison
5.2.2 Arithmetic operations
6 Quotient types in Coq
6.1 Quotients in mathematics
6.2 An interface for quotients
6.3 Quotient by an equivalence relation
6.3.1 Quotient of a choice structure
6.3.2 Quotient of type with an explicit encoding to a choice structure
6.4 Related work on quotient types
7 Construction of the real closure as a type
7.1 Algebraic numbers have an explicit encoding to a choice type
7.1.1 Decoding to algebraic Cauchy reals
7.1.2 Encoding of algebraic Cauchy reals
7.2 A quotient type for algebraic numbers
7.2.1 Construction of the quotient type
7.2.2 Real algebraic numbers form a real closed field
8 Discussion on the algebraic closure
8.1 Equivalent definitions for real closed fields
8.2 Direct construction and other methods
III Theory of real and algebraically closed fields
9 Elementary polynomial analysis
9.1 Direct consequences of the intermediate value theorem
9.2 Root isolation
9.3 Root neighborhoods
9.4 About existential formulas
10 Syntax, semantics and decidability
10.1 First-order logic, the usual presentation
10.2 Formalizing first-order logic in Coq
10.3 Quantifier elimination by projection
10.4 Decidability
11 Solving polynomial systems of equations (in one variable)
11.1 Reduction of the system
11.1.1 For discrete algebraically closed fields
11.1.2 For discrete real closed fields
11.2 Root counting using Tarski queries
11.3 Cauchy index
11.4 Algebraic formula characterizing the existence of a root
12 Programming and certifying the quantifier elimination
12.1 An example
12.2 Algorithm transformation and projection
12.3 Direct transformation
12.4 Continuation passing style transformation
IV Conclusion and perspectives
Lists of Figures
Bibliography
Index