Mercurial > cpdt > repo

comparison src/Universes.v @ 228:0be1a42b3035

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof-reading pass through first bit of Universes
author Adam Chlipala <adamc@hcoop.net>
date Fri, 20 Nov 2009 10:18:35 -0500
parents d8c54a25c81f
children 2bb1642f597c
comparison
equal deleted inserted replaced
227:d8c54a25c81f 228:0be1a42b3035
14 (* end hide *) 14 (* end hide *)
15 15
16 16
17 (** %\chapter{Universes and Axioms}% *) 17 (** %\chapter{Universes and Axioms}% *)
18 18
19 (** Many traditional theorems can be proved in Coq without special knowledge of CIC, the logic behind the prover. A development just seems to be using a particular ASCII notation for standard formulas based on set theory. Nonetheless, as we saw in Chapter 4, CIC differs from set theory in making it possible to define the usual logical connectives as derived notions. The foundation of it all is a dependently-typed functional programming language, based on dependent function types and inductive type families. By using the facilities of this language directly, we can accomplish some things much more easily than in mainstream math. 19 (** Many traditional theorems can be proved in Coq without special knowledge of CIC, the logic behind the prover. A development just seems to be using a particular ASCII notation for standard formulas based on set theory. Nonetheless, as we saw in Chapter 4, CIC differs from set theory in starting from fewer orthogonal primitives. It is possible to define the usual logical connectives as derived notions. The foundation of it all is a dependently-typed functional programming language, based on dependent function types and inductive type families. By using the facilities of this language directly, we can accomplish some things much more easily than in mainstream math.
20 20
21 Gallina, which adds features to the more theoretical CIC, is the logic implemented in Coq. It has a relatively simple foundation that can be defined rigorously in a page or two of formal proof rules. Still, there are some important subtleties that have practical ramifications. This chapter focuses on those subtleties, avoiding formal metatheory in favor of example code. *) 21 Gallina, which adds features to the more theoretical CIC, is the logic implemented in Coq. It has a relatively simple foundation that can be defined rigorously in a page or two of formal proof rules. Still, there are some important subtleties that have practical ramifications. This chapter focuses on those subtleties, avoiding formal metatheory in favor of example code. *)
22 22
23 23
24 (** * The [Type] Hierarchy *) 24 (** * The [Type] Hierarchy *)
57 Type 57 Type
58 : Type 58 : Type
59 59
60 ]] 60 ]]
61 61
62 Strangely enough, [Type] appears to be its own type. It is known that polymorphic languages with this property are inconsistent. That is, using such a language to encode proofs is unwise, because it is possible to "prove" any theorem. What is really going on here? 62 Strangely enough, [Type] appears to be its own type. It is known that polymorphic languages with this property are inconsistent. That is, using such a language to encode proofs is unwise, because it is possible to "prove" any proposition. What is really going on here?
63 63
64 Let us repeat some of our queries after toggling a flag related to Coq's printing behavior. *) 64 Let us repeat some of our queries after toggling a flag related to Coq's printing behavior. *)
65 65
66 Set Printing Universes. 66 Set Printing Universes.
67 67
86 Type $ Top.3 ^ 86 Type $ Top.3 ^
87 : Type $ (Top.3)+1 ^ 87 : Type $ (Top.3)+1 ^
88 88
89 ]] 89 ]]
90 90
91 Occurrences of [Type] are annotated with some additional information, inside comments. These annotations have to do with the secret behind [Type]: it really stands for an infinite hierarchy of types. The type of [Set] is [Type0], the type of [Type0] is [Type1], the type of [Type1] is [Type2], and so on. This is how we avoid the "[Type : Type]" paradox. As a convenience, the universe hierarchy drives Coq's one variety of subtyping. Any term whose type is [Type] at level [i] is automatically also described by [Type] at level [j] when [j > i]. 91 Occurrences of [Type] are annotated with some additional information, inside comments. These annotations have to do with the secret behind [Type]: it Sreally stands for an infinite hierarchy of types. The type of [Set] is [Type(0)], the type of [Type(0)] is [Type(1)], the type of [Type(1)] is [Type(2)], and so on. This is how we avoid the "[Type : Type]" paradox. As a convenience, the universe hierarchy drives Coq's one variety of subtyping. Any term whose type is [Type] at level [i] is automatically also described by [Type] at level [j] when [j > i].
92 92
93 In the outputs of our first [Check] query, we see that the type level of [Set]'s type is [(0)+1]. Here [0] stands for the level of [Set], and we increment it to arrive at the level that %\textit{%#<i>#classifies#</i>#%}% [Set]. 93 In the outputs of our first [Check] query, we see that the type level of [Set]'s type is [(0)+1]. Here [0] stands for the level of [Set], and we increment it to arrive at the level that %\textit{%#<i>#classifies#</i>#%}% [Set].
94 94
95 In the second query's output, we see that the occurrence of [Type] that we check is assigned a fresh %\textit{%#<i>#universe variable#</i>#%}% [Top.3]. The output type increments [Top.3] to move up a level in the universe hierarchy. As we write code that uses definitions whose types mention universe variables, unification may refine the values of those variables. Luckily, the user rarely has to worry about the details. 95 In the second query's output, we see that the occurrence of [Type] that we check is assigned a fresh %\textit{%#<i>#universe variable#</i>#%}% [Top.3]. The output type increments [Top.3] to move up a level in the universe hierarchy. As we write code that uses definitions whose types mention universe variables, unification may refine the values of those variables. Luckily, the user rarely has to worry about the details.
96 96
128 128
129 Check id Set. 129 Check id Set.
130 130
131 Error: Illegal application (Type Error): 131 Error: Illegal application (Type Error):
132 ... 132 ...
133 The 1st term has type "Type (* (Top.15)+1 *)" which should be coercible to "Set". 133 The 1st term has type "Type $ (Top.15)+1 ^" which should be coercible to "Set".
134 134
135 ]] 135 ]]
136 136
137 The parameter [T] of [id] must be instantiated with a [Set]. [nat] is a [Set], but [Set] is not. We can try fixing the problem by generalizing our definition of [id]. *) 137 The parameter [T] of [id] must be instantiated with a [Set]. [nat] is a [Set], but [Set] is not. We can try fixing the problem by generalizing our definition of [id]. *)
138 138
163 163
164 Error: Universe inconsistency (cannot enforce Top.16 < Top.16). 164 Error: Universe inconsistency (cannot enforce Top.16 < Top.16).
165 165
166 ]] 166 ]]
167 167
168 This error message reminds us that the universe variable for [T] still exists, even though it is usually hidden. To apply [id] to itself, that variable would need to be less than itself in the type hierarchy. Universe inconsistency error messages announce cases like this one where a term could only type-check by violating an implied constraint over universe variables. Such errors demonstrate that [Type] is %\textit{%#<i>#predicative#</i>#%}%, where this word has a CIC meaning closely related to its usual mathematical meaning. A predicative system enforces the constraint that, for any object of quantified type, none of those quantifiers may never be instantiated with the object itself. Impredicativity is associated with popular paradoxes in set theory, involving inconsistent constructions like "the set of all sets that do not contain themselves." Similar paradoxes result from uncontrolled impredicativity in Coq. *) 168 This error message reminds us that the universe variable for [T] still exists, even though it is usually hidden. To apply [id] to itself, that variable would need to be less than itself in the type hierarchy. Universe inconsistency error messages announce cases like this one where a term could only type-check by violating an implied constraint over universe variables. Such errors demonstrate that [Type] is %\textit{%#<i>#predicative#</i>#%}%, where this word has a CIC meaning closely related to its usual mathematical meaning. A predicative system enforces the constraint that, for any object of quantified type, none of those quantifiers may ever be instantiated with the object itself. Impredicativity is associated with popular paradoxes in set theory, involving inconsistent constructions like "the set of all sets that do not contain themselves." Similar paradoxes result from uncontrolled impredicativity in Coq. *)
169 169
170 170
171 (** ** Inductive Definitions *) 171 (** ** Inductive Definitions *)
172 172
173 (** Predicativity restrictions also apply to inductive definitions. As an example, let us consider a type of expression trees that allows injection of any native Coq value. The idea is that an [exp T] stands for a reflected expression of type [T]. 173 (** Predicativity restrictions also apply to inductive definitions. As an example, let us consider a type of expression trees that allows injection of any native Coq value. The idea is that an [exp T] stands for a reflected expression of type [T].
187 Inductive exp : Type -> Type := 187 Inductive exp : Type -> Type :=
188 | Const : forall T, T -> exp T 188 | Const : forall T, T -> exp T
189 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) 189 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
190 | Eq : forall T, exp T -> exp T -> exp bool. 190 | Eq : forall T, exp T -> exp T -> exp bool.
191 191
192 (** This definition is accepted. We can build some sample expressions. *) 192 (** Note that before we had to include an annotation [: Set] for the variable [T] in [Const]'s type, but we need no annotation now. When the type of a variable is not known, and when that variable is used in a context where only types are allowed, Coq infers that the variable is of type [Type]. That is the right behavior here, but it was wrong for the [Set] version of [exp].
193
194 Our new definition is accepted. We can build some sample expressions. *)
193 195
194 Check Const 0. 196 Check Const 0.
195 (** %\vspace{-.15in}% [[ 197 (** %\vspace{-.15in}% [[
196 Const 0 198 Const 0
197 : exp nat 199 : exp nat
203 : exp (nat * unit) 205 : exp (nat * unit)
204 ]] *) 206 ]] *)
205 207
206 Check Eq (Const Set) (Const Type). 208 Check Eq (Const Set) (Const Type).
207 (** %\vspace{-.15in}% [[ 209 (** %\vspace{-.15in}% [[
208 Eq (Const Set) (Const Type (* Top.59 *)) 210 Eq (Const Set) (Const Type $ Top.59 ^ )
209 : exp bool 211 : exp bool
210 212
211 ]] 213 ]]
212 214
213 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall. 215 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall.