Mercurial > cpdt > repo
comparison src/Universes.v @ 343:be8c7aae20f4
Pass over Universes
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 17 Oct 2011 11:09:23 -0400 |
parents | d5787b70cf48 |
children | 7466ac31f162 |
comparison
equal
deleted
inserted
replaced
342:25d60fed2e96 | 343:be8c7aae20f4 |
---|---|
1 (* Copyright (c) 2009-2010, Adam Chlipala | 1 (* Copyright (c) 2009-2011, Adam Chlipala |
2 * | 2 * |
3 * This work is licensed under a | 3 * This work is licensed under a |
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |
5 * Unported License. | 5 * Unported License. |
6 * The license text is available at: | 6 * The license text is available at: |
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 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. | 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 %\index{set theory}%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 %\index{Gallina}%Gallina, which adds features to the more theoretical CIC%~\cite{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 *) |
25 | 25 |
26 (** Every object in Gallina has a type. *) | 26 (** %\index{type hierarchy}%Every object in Gallina has a type. *) |
27 | 27 |
28 Check 0. | 28 Check 0. |
29 (** %\vspace{-.15in}% [[ | 29 (** %\vspace{-.15in}% [[ |
30 0 | 30 0 |
31 : nat | 31 : nat |
48 Set | 48 Set |
49 : Type | 49 : Type |
50 | 50 |
51 ]] | 51 ]] |
52 | 52 |
53 The type [Set] may be considered as the set of all sets, a concept that set theory handles in terms of %\textit{%#<i>#classes#</i>#%}%. In Coq, this more general notion is [Type]. *) | 53 The type [Set] may be considered as the set of all sets, a concept that set theory handles in terms of %\index{class (in set theory)}\textit{%#<i>#classes#</i>#%}%. In Coq, this more general notion is [Type]. *) |
54 | 54 |
55 Check Type. | 55 Check Type. |
56 (** %\vspace{-.15in}% [[ | 56 (** %\vspace{-.15in}% [[ |
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 proposition. 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, via %\index{Girard's paradox}%Girard's paradox%~\cite{GirardsParadox}%. 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.%\index{Vernacular commands!Set Printing Universes}% *) |
65 | 65 |
66 Set Printing Universes. | 66 Set Printing Universes. |
67 | 67 |
68 Check nat. | 68 Check nat. |
69 (** %\vspace{-.15in}% [[ | 69 (** %\vspace{-.15in}% [[ |
92 | 92 |
93 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 [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]. | 93 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 [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]. |
94 | 94 |
95 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]. | 95 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]. |
96 | 96 |
97 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. | 97 In the second query's output, we see that the occurrence of [Type] that we check is assigned a fresh %\index{universe variable}\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. |
98 | 98 |
99 Another crucial concept in CIC is %\textit{%#<i>#predicativity#</i>#%}%. Consider these queries. *) | 99 Another crucial concept in CIC is %\index{predicativity}\textit{%#<i>#predicativity#</i>#%}%. Consider these queries. *) |
100 | 100 |
101 Check forall T : nat, fin T. | 101 Check forall T : nat, fin T. |
102 (** %\vspace{-.15in}% [[ | 102 (** %\vspace{-.15in}% [[ |
103 forall T : nat, fin T | 103 forall T : nat, fin T |
104 : Set | 104 : Set |
129 (** %\vspace{-.15in}% [[ | 129 (** %\vspace{-.15in}% [[ |
130 id 0 | 130 id 0 |
131 : nat | 131 : nat |
132 | 132 |
133 Check id Set. | 133 Check id Set. |
134 | 134 ]] |
135 | |
136 << | |
135 Error: Illegal application (Type Error): | 137 Error: Illegal application (Type Error): |
136 ... | 138 ... |
137 The 1st term has type "Type $ (Top.15)+1 ^" which should be coercible to "Set". | 139 The 1st term has type "Type (* (Top.15)+1 *)" which should be coercible to "Set". |
138 | 140 >> |
139 ]] | 141 |
140 | 142 The parameter [T] of [id] must be instantiated with a [Set]. The type [nat] is a [Set], but [Set] is not. We can try fixing the problem by generalizing our definition of [id]. *) |
141 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]. *) | |
142 | 143 |
143 Reset id. | 144 Reset id. |
144 Definition id (T : Type) (x : T) : T := x. | 145 Definition id (T : Type) (x : T) : T := x. |
145 Check id 0. | 146 Check id 0. |
146 (** %\vspace{-.15in}% [[ | 147 (** %\vspace{-.15in}% [[ |
162 : Type $ Top.19 ^ | 163 : Type $ Top.19 ^ |
163 ]] | 164 ]] |
164 *) | 165 *) |
165 | 166 |
166 (** So far so good. As we apply [id] to different [T] values, the inferred index for [T]'s [Type] occurrence automatically moves higher up the type hierarchy. | 167 (** So far so good. As we apply [id] to different [T] values, the inferred index for [T]'s [Type] occurrence automatically moves higher up the type hierarchy. |
167 | |
168 [[ | 168 [[ |
169 Check id id. | 169 Check id id. |
170 | 170 ]] |
171 | |
172 << | |
171 Error: Universe inconsistency (cannot enforce Top.16 < Top.16). | 173 Error: Universe inconsistency (cannot enforce Top.16 < Top.16). |
172 | 174 >> |
173 ]] | 175 |
174 | 176 %\index{universe inconsistency}%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. %\index{impredicativity}%Impredicativity is associated with popular paradoxes in set theory, involving inconsistent constructions like %``%#"#the set of all sets that do not contain themselves#"#%''% (%\index{Russell's paradox}%Russell's paradox). Similar paradoxes would result from uncontrolled impredicativity in Coq. *) |
175 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 would result from uncontrolled impredicativity in Coq. *) | |
176 | 177 |
177 | 178 |
178 (** ** Inductive Definitions *) | 179 (** ** Inductive Definitions *) |
179 | 180 |
180 (** 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]. | 181 (** 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]. |
182 [[ | 183 [[ |
183 Inductive exp : Set -> Set := | 184 Inductive exp : Set -> Set := |
184 | Const : forall T : Set, T -> exp T | 185 | Const : forall T : Set, T -> exp T |
185 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) | 186 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) |
186 | Eq : forall T, exp T -> exp T -> exp bool. | 187 | Eq : forall T, exp T -> exp T -> exp bool. |
187 | 188 ]] |
189 | |
190 << | |
188 Error: Large non-propositional inductive types must be in Type. | 191 Error: Large non-propositional inductive types must be in Type. |
189 | 192 >> |
190 ]] | 193 |
191 | 194 This definition is %\index{large inductive types}\textit{%#<i>#large#</i>#%}% in the sense that at least one of its constructors takes an argument whose type has type [Type]. Coq would be inconsistent if we allowed definitions like this one in their full generality. Instead, we must change [exp] to live in [Type]. We will go even further and move [exp]'s index to [Type] as well. *) |
192 This definition is %\textit{%#<i>#large#</i>#%}% in the sense that at least one of its constructors takes an argument whose type has type [Type]. Coq would be inconsistent if we allowed definitions like this one in their full generality. Instead, we must change [exp] to live in [Type]. We will go even further and move [exp]'s index to [Type] as well. *) | |
193 | 195 |
194 Inductive exp : Type -> Type := | 196 Inductive exp : Type -> Type := |
195 | Const : forall T, T -> exp T | 197 | Const : forall T, T -> exp T |
196 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) | 198 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) |
197 | Eq : forall T, exp T -> exp T -> exp bool. | 199 | Eq : forall T, exp T -> exp T -> exp bool. |
223 | 225 |
224 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall. | 226 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall. |
225 | 227 |
226 [[ | 228 [[ |
227 Check Const (Const O). | 229 Check Const (Const O). |
228 | 230 ]] |
231 | |
232 << | |
229 Error: Universe inconsistency (cannot enforce Top.42 < Top.42). | 233 Error: Universe inconsistency (cannot enforce Top.42 < Top.42). |
230 | 234 >> |
231 ]] | |
232 | 235 |
233 We are unable to instantiate the parameter [T] of [Const] with an [exp] type. To see why, it is helpful to print the annotated version of [exp]'s inductive definition. *) | 236 We are unable to instantiate the parameter [T] of [Const] with an [exp] type. To see why, it is helpful to print the annotated version of [exp]'s inductive definition. *) |
234 | 237 |
235 Print exp. | 238 Print exp. |
236 (** %\vspace{-.15in}% [[ | 239 (** %\vspace{-.15in}% [[ |
245 | 248 |
246 ]] | 249 ]] |
247 | 250 |
248 We see that the index type of [exp] has been assigned to universe level [Top.8]. In addition, each of the four occurrences of [Type] in the types of the constructors gets its own universe variable. Each of these variables appears explicitly in the type of [exp]. In particular, any type [exp T] lives at a universe level found by incrementing by one the maximum of the four argument variables. A consequence of this is that [exp] %\textit{%#<i>#must#</i>#%}% live at a higher universe level than any type which may be passed to one of its constructors. This consequence led to the universe inconsistency. | 251 We see that the index type of [exp] has been assigned to universe level [Top.8]. In addition, each of the four occurrences of [Type] in the types of the constructors gets its own universe variable. Each of these variables appears explicitly in the type of [exp]. In particular, any type [exp T] lives at a universe level found by incrementing by one the maximum of the four argument variables. A consequence of this is that [exp] %\textit{%#<i>#must#</i>#%}% live at a higher universe level than any type which may be passed to one of its constructors. This consequence led to the universe inconsistency. |
249 | 252 |
250 Strangely, the universe variable [Top.8] only appears in one place. Is there no restriction imposed on which types are valid arguments to [exp]? In fact, there is a restriction, but it only appears in a global set of universe constraints that are maintained %``%#"#off to the side,#"#%''% not appearing explicitly in types. We can print the current database. *) | 253 Strangely, the universe variable [Top.8] only appears in one place. Is there no restriction imposed on which types are valid arguments to [exp]? In fact, there is a restriction, but it only appears in a global set of universe constraints that are maintained %``%#"#off to the side,#"#%''% not appearing explicitly in types. We can print the current database.%\index{Vernacular commands!Print Universes}% *) |
251 | 254 |
252 Print Universes. | 255 Print Universes. |
253 (** %\vspace{-.15in}% [[ | 256 (** %\vspace{-.15in}% [[ |
254 Top.19 < Top.9 <= Top.8 | 257 Top.19 < Top.9 <= Top.8 |
255 Top.15 < Top.9 <= Top.8 <= Coq.Init.Datatypes.38 | 258 Top.15 < Top.9 <= Top.8 <= Coq.Init.Datatypes.38 |
256 Top.14 < Top.9 <= Top.8 <= Coq.Init.Datatypes.37 | 259 Top.14 < Top.9 <= Top.8 <= Coq.Init.Datatypes.37 |
257 Top.11 < Top.9 <= Top.8 | 260 Top.11 < Top.9 <= Top.8 |
258 | 261 |
259 ]] | 262 ]] |
260 | 263 |
261 [Print Universes] outputs many more constraints, but we have collected only those that mention [Top] variables. We see one constraint for each universe variable associated with a constructor argument from [exp]'s definition. [Top.19] is the type argument to [Eq]. The constraint for [Top.19] effectively says that [Top.19] must be less than [Top.8], the universe of [exp]'s indices; an intermediate variable [Top.9] appears as an artifact of the way the constraint was generated. | 264 The command outputs many more constraints, but we have collected only those that mention [Top] variables. We see one constraint for each universe variable associated with a constructor argument from [exp]'s definition. Universe variable [Top.19] is the type argument to [Eq]. The constraint for [Top.19] effectively says that [Top.19] must be less than [Top.8], the universe of [exp]'s indices; an intermediate variable [Top.9] appears as an artifact of the way the constraint was generated. |
262 | 265 |
263 The next constraint, for [Top.15], is more complicated. This is the universe of the second argument to the [Pair] constructor. Not only must [Top.15] be less than [Top.8], but it also comes out that [Top.8] must be less than [Coq.Init.Datatypes.38]. What is this new universe variable? It is from the definition of the [prod] inductive family, to which types of the form [A * B] are desugared. *) | 266 The next constraint, for [Top.15], is more complicated. This is the universe of the second argument to the [Pair] constructor. Not only must [Top.15] be less than [Top.8], but it also comes out that [Top.8] must be less than [Coq.Init.Datatypes.38]. What is this new universe variable? It is from the definition of the [prod] inductive family, to which types of the form [A * B] are desugared. *) |
264 | 267 |
265 Print prod. | 268 Print prod. |
266 (** %\vspace{-.15in}% [[ | 269 (** %\vspace{-.15in}% [[ |
283 | 286 |
284 Check (nat, (Type, Set)). | 287 Check (nat, (Type, Set)). |
285 (** %\vspace{-.15in}% [[ | 288 (** %\vspace{-.15in}% [[ |
286 (nat, (Type $ Top.44 ^ , Set)) | 289 (nat, (Type $ Top.44 ^ , Set)) |
287 : Set * (Type $ Top.45 ^ * Type $ Top.46 ^ ) | 290 : Set * (Type $ Top.45 ^ * Type $ Top.46 ^ ) |
288 | |
289 ]] | 291 ]] |
290 | 292 |
291 The same cannot be done with a counterpart to [prod] that does not use parameters. *) | 293 The same cannot be done with a counterpart to [prod] that does not use parameters. *) |
292 | 294 |
293 Inductive prod' : Type -> Type -> Type := | 295 Inductive prod' : Type -> Type -> Type := |
294 | pair' : forall A B : Type, A -> B -> prod' A B. | 296 | pair' : forall A B : Type, A -> B -> prod' A B. |
295 | |
296 (** [[ | 297 (** [[ |
297 Check (pair' nat (pair' Type Set)). | 298 Check (pair' nat (pair' Type Set)). |
298 | 299 ]] |
300 | |
301 << | |
299 Error: Universe inconsistency (cannot enforce Top.51 < Top.51). | 302 Error: Universe inconsistency (cannot enforce Top.51 < Top.51). |
300 | 303 >> |
301 ]] | |
302 | 304 |
303 The key benefit parameters bring us is the ability to avoid quantifying over types in the types of constructors. Such quantification induces less-than constraints, while parameters only introduce less-than-or-equal-to constraints. | 305 The key benefit parameters bring us is the ability to avoid quantifying over types in the types of constructors. Such quantification induces less-than constraints, while parameters only introduce less-than-or-equal-to constraints. |
304 | 306 |
305 Coq includes one more (potentially confusing) feature related to parameters. While Gallina does not support real universe polymorphism, there is a convenience facility that mimics universe polymorphism in some cases. We can illustrate what this means with a simple example. *) | 307 Coq includes one more (potentially confusing) feature related to parameters. While Gallina does not support real %\index{universe polymorphism}%universe polymorphism, there is a convenience facility that mimics universe polymorphism in some cases. We can illustrate what this means with a simple example. *) |
306 | 308 |
307 Inductive foo (A : Type) : Type := | 309 Inductive foo (A : Type) : Type := |
308 | Foo : A -> foo A. | 310 | Foo : A -> foo A. |
309 | 311 |
310 (* begin hide *) | 312 (* begin hide *) |
340 | 342 |
341 Check bar. | 343 Check bar. |
342 (** %\vspace{-.15in}% [[ | 344 (** %\vspace{-.15in}% [[ |
343 bar | 345 bar |
344 : Prop | 346 : Prop |
345 | |
346 ]] | 347 ]] |
347 | 348 |
348 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *) | 349 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *) |
349 | 350 |
350 | 351 |
363 | 364 |
364 Print ex. | 365 Print ex. |
365 (** %\vspace{-.15in}% [[ | 366 (** %\vspace{-.15in}% [[ |
366 Inductive ex (A : Type) (P : A -> Prop) : Prop := | 367 Inductive ex (A : Type) (P : A -> Prop) : Prop := |
367 ex_intro : forall x : A, P x -> ex P | 368 ex_intro : forall x : A, P x -> ex P |
368 | |
369 ]] | 369 ]] |
370 | 370 |
371 It is natural to want a function to extract the first components of data structures like these. Doing so is easy enough for [sig]. *) | 371 It is natural to want a function to extract the first components of data structures like these. Doing so is easy enough for [sig]. *) |
372 | 372 |
373 Definition projS A (P : A -> Prop) (x : sig P) : A := | 373 Definition projS A (P : A -> Prop) (x : sig P) : A := |
374 match x with | 374 match x with |
375 | exist v _ => v | 375 | exist v _ => v |
376 end. | 376 end. |
377 | 377 |
378 (** We run into trouble with a version that has been changed to work with [ex]. | 378 (** We run into trouble with a version that has been changed to work with [ex]. |
379 | |
380 [[ | 379 [[ |
381 Definition projE A (P : A -> Prop) (x : ex P) : A := | 380 Definition projE A (P : A -> Prop) (x : ex P) : A := |
382 match x with | 381 match x with |
383 | ex_intro v _ => v | 382 | ex_intro v _ => v |
384 end. | 383 end. |
385 | 384 ]] |
385 | |
386 << | |
386 Error: | 387 Error: |
387 Incorrect elimination of "x" in the inductive type "ex": | 388 Incorrect elimination of "x" in the inductive type "ex": |
388 the return type has sort "Type" while it should be "Prop". | 389 the return type has sort "Type" while it should be "Prop". |
389 Elimination of an inductive object of sort Prop | 390 Elimination of an inductive object of sort Prop |
390 is not allowed on a predicate in sort Type | 391 is not allowed on a predicate in sort Type |
391 because proofs can be eliminated only to build proofs. | 392 because proofs can be eliminated only to build proofs. |
392 | 393 >> |
393 ]] | 394 |
394 | 395 In formal Coq parlance, %\index{elimination}``%#"#elimination#"#%''% means %``%#"#pattern-matching.#"#%''% The typing rules of Gallina forbid us from pattern-matching on a discriminee whose type belongs to [Prop], whenever the result type of the [match] has a type besides [Prop]. This is a sort of %``%#"#information flow#"#%''% policy, where the type system ensures that the details of proofs can never have any effect on parts of a development that are not also marked as proofs. |
395 In formal Coq parlance, %``%#"#limination#"#%''% means %``%#"#pattern-matching.#"#%''% The typing rules of Gallina forbid us from pattern-matching on a discriminee whose type belongs to [Prop], whenever the result type of the [match] has a type besides [Prop]. This is a sort of %``%#"#information flow#"#%''% policy, where the type system ensures that the details of proofs can never have any effect on parts of a development that are not also marked as proofs. | |
396 | 396 |
397 This restriction matches informal practice. We think of programs and proofs as clearly separated, and, outside of constructive logic, the idea of computing with proofs is ill-formed. The distinction also has practical importance in Coq, where it affects the behavior of extraction. | 397 This restriction matches informal practice. We think of programs and proofs as clearly separated, and, outside of constructive logic, the idea of computing with proofs is ill-formed. The distinction also has practical importance in Coq, where it affects the behavior of extraction. |
398 | 398 |
399 Recall that extraction is Coq's facility for translating Coq developments into programs in general-purpose programming languages like OCaml. Extraction %\textit{%#<i>#erases#</i>#%}% proofs and leaves programs intact. A simple example with [sig] and [ex] demonstrates the distinction. *) | 399 Recall that %\index{program extraction}%extraction is Coq's facility for translating Coq developments into programs in general-purpose programming languages like OCaml. Extraction %\textit{%#<i>#erases#</i>#%}% proofs and leaves programs intact. A simple example with [sig] and [ex] demonstrates the distinction. *) |
400 | 400 |
401 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) := | 401 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) := |
402 match x with | 402 match x with |
403 | exist n pf => exist _ n (sym_eq pf) | 403 | exist n pf => exist _ n (sym_eq pf) |
404 end. | 404 end. |
424 let sym_ex = __ | 424 let sym_ex = __ |
425 >> | 425 >> |
426 | 426 |
427 In this example, the [ex] type itself is in [Prop], so whole [ex] packages are erased. Coq extracts every proposition as the (Coq-specific) type %\texttt{\_\_}%#<tt>__</tt>#, whose single constructor is %\texttt{\_\_}%#<tt>__</tt>#. Not only are proofs replaced by [__], but proof arguments to functions are also removed completely, as we see here. | 427 In this example, the [ex] type itself is in [Prop], so whole [ex] packages are erased. Coq extracts every proposition as the (Coq-specific) type %\texttt{\_\_}%#<tt>__</tt>#, whose single constructor is %\texttt{\_\_}%#<tt>__</tt>#. Not only are proofs replaced by [__], but proof arguments to functions are also removed completely, as we see here. |
428 | 428 |
429 Extraction is very helpful as an optimization over programs that contain proofs. In languages like Haskell, advanced features make it possible to program with proofs, as a way of convincing the type checker to accept particular definitions. Unfortunately, when proofs are encoded as values in GADTs, these proofs exist at runtime and consume resources. In contrast, with Coq, as long as you keep all of your proofs within [Prop], extraction is guaranteed to erase them. | 429 Extraction is very helpful as an optimization over programs that contain proofs. In languages like Haskell, advanced features make it possible to program with proofs, as a way of convincing the type checker to accept particular definitions. Unfortunately, when proofs are encoded as values in GADTs%~\cite{GADT}%, these proofs exist at runtime and consume resources. In contrast, with Coq, as long as all proofs are kept within [Prop], extraction is guaranteed to erase them. |
430 | 430 |
431 Many fans of the Curry-Howard correspondence support the idea of %\textit{%#<i>#extracting programs from proofs#</i>#%}%. In reality, few users of Coq and related tools do any such thing. Instead, extraction is better thought of as an optimization that reduces the runtime costs of expressive typing. | 431 Many fans of the %\index{Curry-Howard correspondence}%Curry-Howard correspondence support the idea of %\textit{%#<i>#extracting programs from proofs#</i>#%}%. In reality, few users of Coq and related tools do any such thing. Instead, extraction is better thought of as an optimization that reduces the runtime costs of expressive typing. |
432 | 432 |
433 %\medskip% | 433 %\medskip% |
434 | 434 |
435 We have seen two of the differences between proofs and programs: proofs are subject to an elimination restriction and are elided by extraction. The remaining difference is that [Prop] is %\textit{%#<i>#impredicative#</i>#%}%, as this example shows. *) | 435 We have seen two of the differences between proofs and programs: proofs are subject to an elimination restriction and are elided by extraction. The remaining difference is that [Prop] is %\index{impredicativity}\textit{%#<i>#impredicative#</i>#%}%, as this example shows. *) |
436 | 436 |
437 Check forall P Q : Prop, P \/ Q -> Q \/ P. | 437 Check forall P Q : Prop, P \/ Q -> Q \/ P. |
438 (** %\vspace{-.15in}% [[ | 438 (** %\vspace{-.15in}% [[ |
439 forall P Q : Prop, P \/ Q -> Q \/ P | 439 forall P Q : Prop, P \/ Q -> Q \/ P |
440 : Prop | 440 : Prop |
505 Base (Base 1) | 505 Base (Base 1) |
506 : eqPlus (Base 1) (Base 1) | 506 : eqPlus (Base 1) (Base 1) |
507 ]] | 507 ]] |
508 *) | 508 *) |
509 | 509 |
510 (** Stating equality facts about proofs may seem baroque, but we have already seen its utility in the chapter on reasoning about equality proofs. *) | |
511 | |
510 | 512 |
511 (** * Axioms *) | 513 (** * Axioms *) |
512 | 514 |
513 (** While the specific logic Gallina is hardcoded into Coq's implementation, it is possible to add certain logical rules in a controlled way. In other words, Coq may be used to reason about many different refinements of Gallina where strictly more theorems are provable. We achieve this by asserting %\textit{%#<i>#axioms#</i>#%}% without proof. | 515 (** While the specific logic Gallina is hardcoded into Coq's implementation, it is possible to add certain logical rules in a controlled way. In other words, Coq may be used to reason about many different refinements of Gallina where strictly more theorems are provable. We achieve this by asserting %\index{axioms}\textit{%#<i>#axioms#</i>#%}% without proof. |
514 | 516 |
515 We will motivate the idea by touring through some standard axioms, as enumerated in Coq's online FAQ. I will add additional commentary as appropriate. *) | 517 We will motivate the idea by touring through some standard axioms, as enumerated in Coq's online FAQ. I will add additional commentary as appropriate. *) |
516 | 518 |
517 (** ** The Basics *) | 519 (** ** The Basics *) |
518 | 520 |
519 (** One simple example of a useful axiom is the law of the excluded middle. *) | 521 (** One simple example of a useful axiom is the %\index{law of the excluded middle}%law of the excluded middle. *) |
520 | 522 |
521 Require Import Classical_Prop. | 523 Require Import Classical_Prop. |
522 Print classic. | 524 Print classic. |
523 (** %\vspace{-.15in}% [[ | 525 (** %\vspace{-.15in}% [[ |
524 *** [ classic : forall P : Prop, P \/ ~ P ] | 526 *** [ classic : forall P : Prop, P \/ ~ P ] |
525 | 527 ]] |
526 ]] | 528 |
527 | 529 In the implementation of module [Classical_Prop], this axiom was defined with the command%\index{Vernacular commands!Axiom}% *) |
528 In the implementation of module [Classical_Prop], this axiom was defined with the command *) | |
529 | 530 |
530 Axiom classic : forall P : Prop, P \/ ~ P. | 531 Axiom classic : forall P : Prop, P \/ ~ P. |
531 | 532 |
532 (** An [Axiom] may be declared with any type, in any of the universes. There is a synonym [Parameter] for [Axiom], and that synonym is often clearer for assertions not of type [Prop]. For instance, we can assert the existence of objects with certain properties. *) | 533 (** An [Axiom] may be declared with any type, in any of the universes. There is a synonym %\index{Vernacular commands!Parameter}%[Parameter] for [Axiom], and that synonym is often clearer for assertions not of type [Prop]. For instance, we can assert the existence of objects with certain properties. *) |
533 | 534 |
534 Parameter n : nat. | 535 Parameter n : nat. |
535 Axiom positive : n > 0. | 536 Axiom positive : n > 0. |
536 Reset n. | 537 Reset n. |
537 | 538 |
538 (** This kind of %``%#"#axiomatic presentation#"#%''% of a theory is very common outside of higher-order logic. However, in Coq, it is almost always preferable to stick to defining your objects, functions, and predicates via inductive definitions and functional programming. | 539 (** This kind of %``%#"#axiomatic presentation#"#%''% of a theory is very common outside of higher-order logic. However, in Coq, it is almost always preferable to stick to defining your objects, functions, and predicates via inductive definitions and functional programming. |
539 | 540 |
540 In general, there is a significant burden associated with any use of axioms. It is easy to assert a set of axioms that together is %\textit{%#<i>#inconsistent#</i>#%}%. That is, a set of axioms may imply [False], which allows any theorem to proved, which defeats the purpose of a proof assistant. For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *) | 541 In general, there is a significant burden associated with any use of axioms. It is easy to assert a set of axioms that together is %\index{inconsistent axioms}\textit{%#<i>#inconsistent#</i>#%}%. That is, a set of axioms may imply [False], which allows any theorem to proved, which defeats the purpose of a proof assistant. For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *) |
541 | 542 |
542 Axiom not_classic : ~ forall P : Prop, P \/ ~ P. | 543 Axiom not_classic : ~ forall P : Prop, P \/ ~ P. |
543 | 544 |
544 Theorem uhoh : False. | 545 Theorem uhoh : False. |
545 generalize classic not_classic; tauto. | 546 generalize classic not_classic; tauto. |
549 destruct uhoh. | 550 destruct uhoh. |
550 Qed. | 551 Qed. |
551 | 552 |
552 Reset not_classic. | 553 Reset not_classic. |
553 | 554 |
554 (** On the subject of the law of the excluded middle itself, this axiom is usually quite harmless, and many practical Coq developments assume it. It has been proved metatheoretically to be consistent with CIC. Here, %``%#"#proved metatheoretically#"#%''% means that someone proved on paper that excluded middle holds in a %\textit{%#<i>#model#</i>#%}% of CIC in set theory. All of the other axioms that we will survey in this section hold in the same model, so they are all consistent together. | 555 (** On the subject of the law of the excluded middle itself, this axiom is usually quite harmless, and many practical Coq developments assume it. It has been proved metatheoretically to be consistent with CIC. Here, %``%#"#proved metatheoretically#"#%''% means that someone proved on paper that excluded middle holds in a %\textit{%#<i>#model#</i>#%}% of CIC in set theory%~\cite{SetsInTypes}%. All of the other axioms that we will survey in this section hold in the same model, so they are all consistent together. |
555 | 556 |
556 Recall that Coq implements %\textit{%#<i>#constructive#</i>#%}% logic by default, where excluded middle is not provable. Proofs in constructive logic can be thought of as programs. A [forall] quantifier denotes a dependent function type, and a disjunction denotes a variant type. In such a setting, excluded middle could be interpreted as a decision procedure for arbitrary propositions, which computability theory tells us cannot exist. Thus, constructive logic with excluded middle can no longer be associated with our usual notion of programming. | 557 Recall that Coq implements %\index{constructive logic}\textit{%#<i>#constructive#</i>#%}% logic by default, where excluded middle is not provable. Proofs in constructive logic can be thought of as programs. A [forall] quantifier denotes a dependent function type, and a disjunction denotes a variant type. In such a setting, excluded middle could be interpreted as a decision procedure for arbitrary propositions, which computability theory tells us cannot exist. Thus, constructive logic with excluded middle can no longer be associated with our usual notion of programming. |
557 | 558 |
558 Given all this, why is it all right to assert excluded middle as an axiom? The intuitive justification is that the elimination restriction for [Prop] prevents us from treating proofs as programs. An excluded middle axiom that quantified over [Set] instead of [Prop] %\textit{%#<i>#would#</i>#%}% be problematic. If a development used that axiom, we would not be able to extract the code to OCaml (soundly) without implementing a genuine universal decision procedure. In contrast, values whose types belong to [Prop] are always erased by extraction, so we sidestep the axiom's algorithmic consequences. | 559 Given all this, why is it all right to assert excluded middle as an axiom? The intuitive justification is that the elimination restriction for [Prop] prevents us from treating proofs as programs. An excluded middle axiom that quantified over [Set] instead of [Prop] %\textit{%#<i>#would#</i>#%}% be problematic. If a development used that axiom, we would not be able to extract the code to OCaml (soundly) without implementing a genuine universal decision procedure. In contrast, values whose types belong to [Prop] are always erased by extraction, so we sidestep the axiom's algorithmic consequences. |
559 | 560 |
560 Because the proper use of axioms is so precarious, there are helpful commands for determining which axioms a theorem relies on. *) | 561 Because the proper use of axioms is so precarious, there are helpful commands for determining which axioms a theorem relies on.%\index{Vernacular commands!Print Assumptions}% *) |
561 | 562 |
562 Theorem t1 : forall P : Prop, P -> ~ ~ P. | 563 Theorem t1 : forall P : Prop, P -> ~ ~ P. |
563 tauto. | 564 tauto. |
564 Qed. | 565 Qed. |
565 | 566 |
566 Print Assumptions t1. | 567 Print Assumptions t1. |
567 (** %\vspace{-.15in}% [[ | 568 (** << |
568 Closed under the global context | 569 Closed under the global context |
569 ]] | 570 >> |
570 *) | 571 *) |
571 | 572 |
572 Theorem t2 : forall P : Prop, ~ ~ P -> P. | 573 Theorem t2 : forall P : Prop, ~ ~ P -> P. |
573 (** [[ | 574 (** [[ |
574 tauto. | 575 tauto. |
575 | 576 ]] |
577 << | |
576 Error: tauto failed. | 578 Error: tauto failed. |
577 | 579 >> |
578 ]] | |
579 *) | 580 *) |
580 | |
581 intro P; destruct (classic P); tauto. | 581 intro P; destruct (classic P); tauto. |
582 Qed. | 582 Qed. |
583 | 583 |
584 Print Assumptions t2. | 584 Print Assumptions t2. |
585 (** %\vspace{-.15in}% [[ | 585 (** %\vspace{-.15in}% [[ |
586 Axioms: | 586 Axioms: |
587 classic : forall P : Prop, P \/ ~ P | 587 classic : forall P : Prop, P \/ ~ P |
588 | |
589 ]] | 588 ]] |
590 | 589 |
591 It is possible to avoid this dependence in some specific cases, where excluded middle %\textit{%#<i>#is#</i>#%}% provable, for decidable families of propositions. *) | 590 It is possible to avoid this dependence in some specific cases, where excluded middle %\textit{%#<i>#is#</i>#%}% provable, for decidable families of propositions. *) |
592 | 591 |
593 Theorem nat_eq_dec : forall n m : nat, n = m \/ n <> m. | 592 Theorem nat_eq_dec : forall n m : nat, n = m \/ n <> m. |
597 Theorem t2' : forall n m : nat, ~ ~ (n = m) -> n = m. | 596 Theorem t2' : forall n m : nat, ~ ~ (n = m) -> n = m. |
598 intros n m; destruct (nat_eq_dec n m); tauto. | 597 intros n m; destruct (nat_eq_dec n m); tauto. |
599 Qed. | 598 Qed. |
600 | 599 |
601 Print Assumptions t2'. | 600 Print Assumptions t2'. |
602 (** %\vspace{-.15in}% [[ | 601 (** << |
603 Closed under the global context | 602 Closed under the global context |
604 ]] | 603 >> |
605 | 604 |
606 %\bigskip% | 605 %\bigskip% |
607 | 606 |
608 Mainstream mathematical practice assumes excluded middle, so it can be useful to have it available in Coq developments, though it is also nice to know that a theorem is proved in a simpler formal system than classical logic. There is a similar story for %\textit{%#<i>#proof irrelevance#</i>#%}%, which simplifies proof issues that would not even arise in mainstream math. *) | 607 Mainstream mathematical practice assumes excluded middle, so it can be useful to have it available in Coq developments, though it is also nice to know that a theorem is proved in a simpler formal system than classical logic. There is a similar story for %\index{proof irrelevance}\textit{%#<i>#proof irrelevance#</i>#%}%, which simplifies proof issues that would not even arise in mainstream math. *) |
609 | 608 |
610 Require Import ProofIrrelevance. | 609 Require Import ProofIrrelevance. |
611 Print proof_irrelevance. | 610 Print proof_irrelevance. |
612 (** %\vspace{-.15in}% [[ | 611 (** %\vspace{-.15in}% [[ |
613 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ] | 612 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ] |
614 | |
615 ]] | 613 ]] |
616 | 614 |
617 This axiom asserts that any two proofs of the same proposition are equal. If we replaced [p1 = p2] by [p1 <-> p2], then the statement would be provable. However, equality is a stronger notion than logical equivalence. Recall this example function from Chapter 6. *) | 615 This axiom asserts that any two proofs of the same proposition are equal. If we replaced [p1 = p2] by [p1 <-> p2], then the statement would be provable. However, equality is a stronger notion than logical equivalence. Recall this example function from Chapter 6. *) |
618 | 616 |
619 (* begin hide *) | 617 (* begin hide *) |
626 match n with | 624 match n with |
627 | O => fun pf : 0 > 0 => match zgtz pf with end | 625 | O => fun pf : 0 > 0 => match zgtz pf with end |
628 | S n' => fun _ => n' | 626 | S n' => fun _ => n' |
629 end. | 627 end. |
630 | 628 |
631 (** We might want to prove that different proofs of [n > 0] do not lead to different results from our richly-typed predecessor function. *) | 629 (** We might want to prove that different proofs of [n > 0] do not lead to different results from our richly typed predecessor function. *) |
632 | 630 |
633 Theorem pred_strong1_irrel : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2. | 631 Theorem pred_strong1_irrel : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2. |
634 destruct n; crush. | 632 destruct n; crush. |
635 Qed. | 633 Qed. |
636 | 634 |
650 Print eq_rect_eq. | 648 Print eq_rect_eq. |
651 (** %\vspace{-.15in}% [[ | 649 (** %\vspace{-.15in}% [[ |
652 *** [ eq_rect_eq : | 650 *** [ eq_rect_eq : |
653 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), | 651 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), |
654 x = eq_rect p Q x p h ] | 652 x = eq_rect p Q x p h ] |
655 | 653 ]] |
656 ]] | 654 |
657 | 655 This axiom says that it is permissible to simplify pattern matches over proofs of equalities like [e = e]. The axiom is logically equivalent to some simpler corollaries. In the theorem names, %``%#"#UIP#"#%''% stands for %\index{unicity of identity proofs}``%#"#unicity of identity proofs#"#%''%, where %``%#"#identity#"#%''% is a synonym for %``%#"#equality.#"#%''% *) |
658 This axiom says that it is permissible to simplify pattern matches over proofs of equalities like [e = e]. The axiom is logically equivalent to some simpler corollaries. *) | |
659 | 656 |
660 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = refl_equal x. | 657 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = refl_equal x. |
661 intros; replace pf with (eq_rect x (eq x) (refl_equal x) x pf); [ | 658 intros; replace pf with (eq_rect x (eq x) (refl_equal x) x pf); [ |
662 symmetry; apply eq_rect_eq | 659 symmetry; apply eq_rect_eq |
663 | exact (match pf as pf' return match pf' in _ = y return x = y with | 660 | exact (match pf as pf' return match pf' in _ = y return x = y with |
691 | 688 |
692 ]] | 689 ]] |
693 | 690 |
694 This axiom says that two functions are equal if they map equal inputs to equal outputs. Such facts are not provable in general in CIC, but it is consistent to assume that they are. | 691 This axiom says that two functions are equal if they map equal inputs to equal outputs. Such facts are not provable in general in CIC, but it is consistent to assume that they are. |
695 | 692 |
696 A simple corollary shows that the same property applies to predicates. In some cases, one might prefer to assert this corollary as the axiom, to restrict the consequences to proofs and not programs. *) | 693 A simple corollary shows that the same property applies to predicates. *) |
697 | 694 |
698 Corollary predicate_extensionality : forall (A : Type) (B : A -> Prop) (f g : forall x : A, B x), | 695 Corollary predicate_extensionality : forall (A : Type) (B : A -> Prop) (f g : forall x : A, B x), |
699 (forall x : A, f x = g x) -> f = g. | 696 (forall x : A, f x = g x) -> f = g. |
700 intros; apply functional_extensionality_dep; assumption. | 697 intros; apply functional_extensionality_dep; assumption. |
701 Qed. | 698 Qed. |
702 | 699 |
700 (** In some cases, one might prefer to assert this corollary as the axiom, to restrict the consequences to proofs and not programs. *) | |
701 | |
703 | 702 |
704 (** ** Axioms of Choice *) | 703 (** ** Axioms of Choice *) |
705 | 704 |
706 (** Some Coq axioms are also points of contention in mainstream math. The most prominent example is the axiom of choice. In fact, there are multiple versions that we might consider, and, considered in isolation, none of these versions means quite what it means in classical set theory. | 705 (** Some Coq axioms are also points of contention in mainstream math. The most prominent example is the %\index{axiom of choice}%axiom of choice. In fact, there are multiple versions that we might consider, and, considered in isolation, none of these versions means quite what it means in classical set theory. |
707 | 706 |
708 First, it is possible to implement a choice operator %\textit{%#<i>#without#</i>#%}% axioms in some potentially surprising cases. *) | 707 First, it is possible to implement a choice operator %\textit{%#<i>#without#</i>#%}% axioms in some potentially surprising cases. *) |
709 | 708 |
710 Require Import ConstructiveEpsilon. | 709 Require Import ConstructiveEpsilon. |
711 Check constructive_definite_description. | 710 Check constructive_definite_description. |
718 (exists! x : A, P x) -> {x : A | P x} | 717 (exists! x : A, P x) -> {x : A | P x} |
719 ]] | 718 ]] |
720 *) | 719 *) |
721 | 720 |
722 Print Assumptions constructive_definite_description. | 721 Print Assumptions constructive_definite_description. |
723 (** %\vspace{-.15in}% [[ | 722 (** << |
724 Closed under the global context | 723 Closed under the global context |
725 | 724 >> |
726 ]] | |
727 | 725 |
728 This function transforms a decidable predicate [P] into a function that produces an element satisfying [P] from a proof that such an element exists. The functions [f] and [g], in conjunction with an associated injectivity property, are used to express the idea that the set [A] is countable. Under these conditions, a simple brute force algorithm gets the job done: we just enumerate all elements of [A], stopping when we find one satisfying [P]. The existence proof, specified in terms of %\textit{%#<i>#unique#</i>#%}% existence [exists!], guarantees termination. The definition of this operator in Coq uses some interesting techniques, as seen in the implementation of the [ConstructiveEpsilon] module. | 726 This function transforms a decidable predicate [P] into a function that produces an element satisfying [P] from a proof that such an element exists. The functions [f] and [g], in conjunction with an associated injectivity property, are used to express the idea that the set [A] is countable. Under these conditions, a simple brute force algorithm gets the job done: we just enumerate all elements of [A], stopping when we find one satisfying [P]. The existence proof, specified in terms of %\textit{%#<i>#unique#</i>#%}% existence [exists!], guarantees termination. The definition of this operator in Coq uses some interesting techniques, as seen in the implementation of the [ConstructiveEpsilon] module. |
729 | 727 |
730 Countable choice is provable in set theory without appealing to the general axiom of choice. To support the more general principle in Coq, we must also add an axiom. Here is a functional version of the axiom of unique choice. *) | 728 Countable choice is provable in set theory without appealing to the general axiom of choice. To support the more general principle in Coq, we must also add an axiom. Here is a functional version of the axiom of unique choice. *) |
731 | 729 |
733 Check dependent_unique_choice. | 731 Check dependent_unique_choice. |
734 (** %\vspace{-.15in}% [[ | 732 (** %\vspace{-.15in}% [[ |
735 dependent_unique_choice | 733 dependent_unique_choice |
736 : forall (A : Type) (B : A -> Type) (R : forall x : A, B x -> Prop), | 734 : forall (A : Type) (B : A -> Type) (R : forall x : A, B x -> Prop), |
737 (forall x : A, exists! y : B x, R x y) -> | 735 (forall x : A, exists! y : B x, R x y) -> |
738 exists f : forall x : A, B x, forall x : A, R x (f x) | 736 exists f : forall x : A, B x, |
739 | 737 forall x : A, R x (f x) |
740 ]] | 738 ]] |
741 | 739 |
742 This axiom lets us convert a relational specification [R] into a function implementing that specification. We need only prove that [R] is truly a function. An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs. We also simplify the statement of the theorem by considering only non-dependent function types. *) | 740 This axiom lets us convert a relational specification [R] into a function implementing that specification. We need only prove that [R] is truly a function. An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs. We also simplify the statement of the theorem by considering only non-dependent function types. *) |
743 | 741 |
744 Require Import ClassicalChoice. | 742 Require Import ClassicalChoice. |
764 | 762 |
765 However, when we combine an axiom of choice with the law of the excluded middle, the idea of %``%#"#choice#"#%''% becomes more interesting. Excluded middle gives us a highly non-computational way of constructing proofs, but it does not change the computational nature of programs. Thus, the axiom of choice is still giving us a way of translating between two different sorts of %``%#"#programs,#"#%''% but the input programs (which are proofs) may be written in a rich language that goes beyond normal computability. This truly is more than repackaging a function with a different type. | 763 However, when we combine an axiom of choice with the law of the excluded middle, the idea of %``%#"#choice#"#%''% becomes more interesting. Excluded middle gives us a highly non-computational way of constructing proofs, but it does not change the computational nature of programs. Thus, the axiom of choice is still giving us a way of translating between two different sorts of %``%#"#programs,#"#%''% but the input programs (which are proofs) may be written in a rich language that goes beyond normal computability. This truly is more than repackaging a function with a different type. |
766 | 764 |
767 %\bigskip% | 765 %\bigskip% |
768 | 766 |
769 The Coq tools support a command-line flag %\texttt{%#<tt>#-impredicative-set#</tt>#%}%, which modifies Gallina in a more fundamental way by making [Set] impredicative. A term like [forall T : Set, T] has type [Set], and inductive definitions in [Set] may have constructors that quantify over arguments of any types. To maintain consistency, an elimination restriction must be imposed, similarly to the restriction for [Prop]. The restriction only applies to large inductive types, where some constructor quantifies over a type of type [Type]. In such cases, a value in this inductive type may only be pattern-matched over to yield a result type whose type is [Set] or [Prop]. This contrasts with [Prop], where the restriction applies even to non-large inductive types, and where the result type may only have type [Prop]. | 767 The Coq tools support a command-line flag %\index{impredicative Set}\texttt{%#<tt>#-impredicative-set#</tt>#%}%, which modifies Gallina in a more fundamental way by making [Set] impredicative. A term like [forall T : Set, T] has type [Set], and inductive definitions in [Set] may have constructors that quantify over arguments of any types. To maintain consistency, an elimination restriction must be imposed, similarly to the restriction for [Prop]. The restriction only applies to large inductive types, where some constructor quantifies over a type of type [Type]. In such cases, a value in this inductive type may only be pattern-matched over to yield a result type whose type is [Set] or [Prop]. This contrasts with [Prop], where the restriction applies even to non-large inductive types, and where the result type may only have type [Prop]. |
770 | 768 |
771 In old versions of Coq, [Set] was impredicative by default. Later versions make [Set] predicative to avoid inconsistency with some classical axioms. In particular, one should watch out when using impredicative [Set] with axioms of choice. In combination with excluded middle or predicate extensionality, this can lead to inconsistency. Impredicative [Set] can be useful for modeling inherently impredicative mathematical concepts, but almost all Coq developments get by fine without it. *) | 769 In old versions of Coq, [Set] was impredicative by default. Later versions make [Set] predicative to avoid inconsistency with some classical axioms. In particular, one should watch out when using impredicative [Set] with axioms of choice. In combination with excluded middle or predicate extensionality, this can lead to inconsistency. Impredicative [Set] can be useful for modeling inherently impredicative mathematical concepts, but almost all Coq developments get by fine without it. *) |
772 | 770 |
773 (** ** Axioms and Computation *) | 771 (** ** Axioms and Computation *) |
774 | 772 |
780 end. | 778 end. |
781 | 779 |
782 (** Computation over programs that use [cast] can proceed smoothly. *) | 780 (** Computation over programs that use [cast] can proceed smoothly. *) |
783 | 781 |
784 Eval compute in (cast (refl_equal (nat -> nat)) (fun n => S n)) 12. | 782 Eval compute in (cast (refl_equal (nat -> nat)) (fun n => S n)) 12. |
785 (** [[ | 783 (** %\vspace{-.15in}%[[ |
786 = 13 | 784 = 13 |
787 : nat | 785 : nat |
788 ]] | 786 ]] |
789 *) | 787 *) |
790 | 788 |
799 (** [[ | 797 (** [[ |
800 = match t3 in (_ = P) return P with | 798 = match t3 in (_ = P) return P with |
801 | refl_equal => fun n : nat => First | 799 | refl_equal => fun n : nat => First |
802 end 12 | 800 end 12 |
803 : fin (12 + 1) | 801 : fin (12 + 1) |
804 | |
805 ]] | 802 ]] |
806 | 803 |
807 Computation gets stuck in a pattern-match on the proof [t3]. The structure of [t3] is not known, so the match cannot proceed. It turns out a more basic problem leads to this particular situation. We ended the proof of [t3] with [Qed], so the definition of [t3] is not available to computation. That is easily fixed. *) | 804 Computation gets stuck in a pattern-match on the proof [t3]. The structure of [t3] is not known, so the match cannot proceed. It turns out a more basic problem leads to this particular situation. We ended the proof of [t3] with [Qed], so the definition of [t3] is not available to computation. That is easily fixed. *) |
808 | 805 |
809 Reset t3. | 806 Reset t3. |
818 = match | 815 = match |
819 match | 816 match |
820 match | 817 match |
821 functional_extensionality | 818 functional_extensionality |
822 .... | 819 .... |
823 | |
824 ]] | 820 ]] |
825 | 821 |
826 We elide most of the details. A very unwieldy tree of nested matches on equality proofs appears. This time evaluation really %\textit{%#<i>#is#</i>#%}% stuck on a use of an axiom. | 822 We elide most of the details. A very unwieldy tree of nested matches on equality proofs appears. This time evaluation really %\textit{%#<i>#is#</i>#%}% stuck on a use of an axiom. |
827 | 823 |
828 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *) | 824 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *) |
838 Eval compute in cast (t4 13) First. | 834 Eval compute in cast (t4 13) First. |
839 (** %\vspace{-.15in}% [[ | 835 (** %\vspace{-.15in}% [[ |
840 = First | 836 = First |
841 : fin (13 + 1) | 837 : fin (13 + 1) |
842 ]] | 838 ]] |
843 *) | 839 |
840 This simple computational reduction hides the use of a recursive function to produce a suitable [refl_equal] proof term. The recursion originates in our use of [induction] in [t4]'s proof. *) | |
841 |