Mercurial > cpdt > repo

comparison src/Universes.v @ 343:be8c7aae20f4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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