Project topics and materials
Get Complete Project Material File(s) Now! »
Excluded middle and proof irrelevance
In the constructive type theory implemented by the Coq system, the excluded middle principle does not hold in general for any statement expressed in the Prop sort. It corresponds to the fact that a proposition might be provable, that its negation might be provable or that neither are provable. An advantage of Boolean statement is that they enjoy excluded middle (a Boolean is either true of false).
Interaction between bool and other types
Propositions that can be reflected to Booleans are exactly the decidable proposi-tions. Hence, Boolean reflection is a great tool to ease case analysis, since a case on a Boolean-reflected proposition creates two subgoals according to the possible truth values of this Boolean. The SSReflect library provides more elaborated constructs, especially to take advantage of both the Boolean and the predicate it reflects. We give examples of this in Section 1.3.
In Coq, two proofs of the same statement have no reason to be equal. Indeed, equality is intentional, which means it distinguishes two programs that compute the same value (i.e. that are extensionally equal), but that are not written in the same way. A traditional example would be that although the bubble sort and the quick sort both sort lists, they are not equal. However, all the proofs of equality of two given Booleans are the same.
Lemma bool_irrelevance (x y : bool) (E E’ : x = y) : E = E’.
In the SSReflect library, this is presented as a consequence of a more general fact: proofs of equality are all equal on types on which equality is decidable.
Theorem eq_irrelevance (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2.
This property is called proof irrelevance, [52] we only showed it applies to proof of equalities in an eqType, i.e. a type on which equality is decidable. The structure of eqType is described in Section 2.2. This implies there is exactly zero or one proof of such equality statements: either the two elements are equal, and there is exactly one proof of equality, or they are not, and there is no proof of equality.
In particular, this implies a strong property on the Σ-type sT := {x : T | P x} of elements of a type T that satisfy a Boolean property P: two elements of sT are equal if and only if their first projection (i.e. the projection projT1 : sT -> T) are equal. This is not true in general where two elements of the Σ-type originating from the same element in the type T can be different because their proof of membership are. We call subtypes the Σ-types for which this property holds.
Interaction between bool and other types
Discrete types
The most used Boolean operator in the library is the equality operator on types with decidable equality (also called discrete types) eqType. Indeed, it reflects Coq intentional equality to a Boolean predicate eq_op, which is denoted using the nota-tion (_ == _). Chapter 2 explains how eqType is defined and integrated in a larger context.
One of the most simple datatypes on which such a decidable operator can be defined is bool. But equality is also decidable on nat, the type of Coq natural numbers. This leads to the definition of the eqn equality operator on nat.
Fixpoint eqn m n {struct m} :=
match m, n with
| 0, 0 => true
| m’.+1, n’.+1 => eqn m’ n’
| _, _ => false
15
1 Booleans in Coq logic
end.
This operator reflects the intentional equality in the sense the lemma eqnP is prov-able:
Lemma eqnP : forall x y : nat, reflect (x = y) (eqn x y).
Inductive families
There are multiple specific inductive types that play a role similar to reflect, in which they associate the provability of a proposition or a list of propositions, with another datatype. One of the most used is the leq_xor_gtn inductive family.
Inductive leq_xor_gtn m n : bool -> bool -> Set :=
| LeqNotGtn of m <= n : leq_xor_gtn m n true false
| GtnNotLeq of n < m : leq_xor_gtn m n false true.
And it is used through its only instantiation:
Lemma leqP m n : leq_xor_gtn m n (m <= n) (n < m).
When we make a case analysis on a proof of (leqP m n), it generates two sub-goals, one for each constructor. We explain how this works in Section 4.2, as we reuse this concept and extend it.
Container datatypes
The SSReflect library also provides support for the theory of container data-types. Those are types equipped with Boolean characteristic functions, and modeled by the structure of predType. Any inhabitant of a type equipped with a struc-ture of (predType T) should be associated with a total Boolean unary operator of type (T -> bool). This Boolean operator benefits from a generic (_ \in _) infix notation: it is a membership test. For instance, if T is a type with decid-able equality, the type (seq T) of finite sequences of elements in T has a structure of (predType T), whose membership operator is the usual membership test for se-quences. For any sequence (s : seq T), the Boolean expression (x \in s) tests whether x belongs to the elements of the sequence s. A predType structure however does not imply the effectiveness of the comparison between its elements: the sub-set relation between (a : T) and (b : T), denoted by {subset a <= b}, is not a Boolean test, even if T is an instance of predType, as there is a priori no effective way to test this inclusion.
For a further introduction to small scale reflection and to the support provided by the SSReflect tactic language and libraries, one may refer to [44].
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
