Mercurial > cpdt > repo

annotate src/Universes.v @ 229:2bb1642f597c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prop section
author Adam Chlipala <adamc@hcoop.net>
date Fri, 20 Nov 2009 11:02:26 -0500
parents 0be1a42b3035
children 9dbcd6bad488
rev   line source
adamc@227 1 (* Copyright (c) 2009, Adam Chlipala
adamc@227 2 *
adamc@227 3 * This work is licensed under a
adamc@227 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@227 5 * Unported License.
adamc@227 6 * The license text is available at:
adamc@227 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@227 8 *)
adamc@227 9
adamc@227 10 (* begin hide *)
adamc@227 11 Require Import DepList.
adamc@227 12
adamc@227 13 Set Implicit Arguments.
adamc@227 14 (* end hide *)
adamc@227 15
adamc@227 16
adamc@227 17 (** %\chapter{Universes and Axioms}% *)
adamc@227 18
adamc@228 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.
adamc@227 20
adamc@227 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. *)
adamc@227 22
adamc@227 23
adamc@227 24 (** * The [Type] Hierarchy *)
adamc@227 25
adamc@227 26 (** Every object in Gallina has a type. *)
adamc@227 27
adamc@227 28 Check 0.
adamc@227 29 (** %\vspace{-.15in}% [[
adamc@227 30 0
adamc@227 31 : nat
adamc@227 32
adamc@227 33 ]]
adamc@227 34
adamc@227 35 It is natural enough that zero be considered as a natural number. *)
adamc@227 36
adamc@227 37 Check nat.
adamc@227 38 (** %\vspace{-.15in}% [[
adamc@227 39 nat
adamc@227 40 : Set
adamc@227 41
adamc@227 42 ]]
adamc@227 43
adamc@227 44 From a set theory perspective, it is unsurprising to consider the natural numbers as a "set." *)
adamc@227 45
adamc@227 46 Check Set.
adamc@227 47 (** %\vspace{-.15in}% [[
adamc@227 48 Set
adamc@227 49 : Type
adamc@227 50
adamc@227 51 ]]
adamc@227 52
adamc@227 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]. *)
adamc@227 54
adamc@227 55 Check Type.
adamc@227 56 (** %\vspace{-.15in}% [[
adamc@227 57 Type
adamc@227 58 : Type
adamc@227 59
adamc@227 60 ]]
adamc@227 61
adamc@228 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?
adamc@227 63
adamc@227 64 Let us repeat some of our queries after toggling a flag related to Coq's printing behavior. *)
adamc@227 65
adamc@227 66 Set Printing Universes.
adamc@227 67
adamc@227 68 Check nat.
adamc@227 69 (** %\vspace{-.15in}% [[
adamc@227 70 nat
adamc@227 71 : Set
adamc@227 72 ]] *)
adamc@227 73
adamc@227 74 (** printing $ %({}*% #(<a/>*# *)
adamc@227 75 (** printing ^ %*{})% #*<a/>)# *)
adamc@227 76
adamc@227 77 Check Set.
adamc@227 78 (** %\vspace{-.15in}% [[
adamc@227 79 Set
adamc@227 80 : Type $ (0)+1 ^
adamc@227 81
adamc@227 82 ]] *)
adamc@227 83
adamc@227 84 Check Type.
adamc@227 85 (** %\vspace{-.15in}% [[
adamc@227 86 Type $ Top.3 ^
adamc@227 87 : Type $ (Top.3)+1 ^
adamc@227 88
adamc@227 89 ]]
adamc@227 90
adamc@228 91 Occurrences of [Type] are annotated with some additional information, inside comments. These annotations have to do with the secret behind [Type]: it Sreally stands for an infinite hierarchy of types. The type of [Set] is [Type(0)], the type of [Type(0)] is [Type(1)], the type of [Type(1)] is [Type(2)], and so on. This is how we avoid the "[Type : Type]" paradox. As a convenience, the universe hierarchy drives Coq's one variety of subtyping. Any term whose type is [Type] at level [i] is automatically also described by [Type] at level [j] when [j > i].
adamc@227 92
adamc@227 93 In the outputs of our first [Check] query, we see that the type level of [Set]'s type is [(0)+1]. Here [0] stands for the level of [Set], and we increment it to arrive at the level that %\textit{%#<i>#classifies#</i>#%}% [Set].
adamc@227 94
adamc@227 95 In the second query's output, we see that the occurrence of [Type] that we check is assigned a fresh %\textit{%#<i>#universe variable#</i>#%}% [Top.3]. The output type increments [Top.3] to move up a level in the universe hierarchy. As we write code that uses definitions whose types mention universe variables, unification may refine the values of those variables. Luckily, the user rarely has to worry about the details.
adamc@227 96
adamc@227 97 Another crucial concept in CIC is %\textit{%#<i>#predicativity#</i>#%}%. Consider these queries. *)
adamc@227 98
adamc@227 99 Check forall T : nat, fin T.
adamc@227 100 (** %\vspace{-.15in}% [[
adamc@227 101 forall T : nat, fin T
adamc@227 102 : Set
adamc@227 103 ]] *)
adamc@227 104
adamc@227 105 Check forall T : Set, T.
adamc@227 106 (** %\vspace{-.15in}% [[
adamc@227 107 forall T : Set, T
adamc@227 108 : Type $ max(0, (0)+1) ^
adamc@227 109 ]] *)
adamc@227 110
adamc@227 111 Check forall T : Type, T.
adamc@227 112 (** %\vspace{-.15in}% [[
adamc@227 113 forall T : Type $ Top.9 ^ , T
adamc@227 114 : Type $ max(Top.9, (Top.9)+1) ^
adamc@227 115
adamc@227 116 ]]
adamc@227 117
adamc@227 118 These outputs demonstrate the rule for determining which universe a [forall] type lives in. In particular, for a type [forall x : T1, T2], we take the maximum of the universes of [T1] and [T2]. In the first example query, both [T1] ([nat]) and [T2] ([fin T]) are in [Set], so the [forall] type is in [Set], too. In the second query, [T1] is [Set], which is at level [(0)+1]; and [T2] is [T], which is at level [0]. Thus, the [forall] exists at the maximum of these two levels. The third example illustrates the same outcome, where we replace [Set] with an occurrence of [Type] that is assigned universe variable [Top.9]. This universe variable appears in the places where [0] appeared in the previous query.
adamc@227 119
adamc@227 120 The behind-the-scenes manipulation of universe variables gives us predicativity. Consider this simple definition of a polymorphic identity function. *)
adamc@227 121
adamc@227 122 Definition id (T : Set) (x : T) : T := x.
adamc@227 123
adamc@227 124 Check id 0.
adamc@227 125 (** %\vspace{-.15in}% [[
adamc@227 126 id 0
adamc@227 127 : nat
adamc@227 128
adamc@227 129 Check id Set.
adamc@227 130
adamc@227 131 Error: Illegal application (Type Error):
adamc@227 132 ...
adamc@228 133 The 1st term has type "Type $ (Top.15)+1 ^" which should be coercible to "Set".
adamc@227 134
adamc@227 135 ]]
adamc@227 136
adamc@227 137 The parameter [T] of [id] must be instantiated with a [Set]. [nat] is a [Set], but [Set] is not. We can try fixing the problem by generalizing our definition of [id]. *)
adamc@227 138
adamc@227 139 Reset id.
adamc@227 140 Definition id (T : Type) (x : T) : T := x.
adamc@227 141 Check id 0.
adamc@227 142 (** %\vspace{-.15in}% [[
adamc@227 143 id 0
adamc@227 144 : nat
adamc@227 145 ]] *)
adamc@227 146
adamc@227 147 Check id Set.
adamc@227 148 (** %\vspace{-.15in}% [[
adamc@227 149 id Set
adamc@227 150 : Type $ Top.17 ^
adamc@227 151 ]] *)
adamc@227 152
adamc@227 153 Check id Type.
adamc@227 154 (** %\vspace{-.15in}% [[
adamc@227 155 id Type $ Top.18 ^
adamc@227 156 : Type $ Top.19 ^
adamc@227 157 ]] *)
adamc@227 158
adamc@227 159 (** 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.
adamc@227 160
adamc@227 161 [[
adamc@227 162 Check id id.
adamc@227 163
adamc@227 164 Error: Universe inconsistency (cannot enforce Top.16 < Top.16).
adamc@227 165
adamc@227 166 ]]
adamc@227 167
adamc@228 168 This error message reminds us that the universe variable for [T] still exists, even though it is usually hidden. To apply [id] to itself, that variable would need to be less than itself in the type hierarchy. Universe inconsistency error messages announce cases like this one where a term could only type-check by violating an implied constraint over universe variables. Such errors demonstrate that [Type] is %\textit{%#<i>#predicative#</i>#%}%, where this word has a CIC meaning closely related to its usual mathematical meaning. A predicative system enforces the constraint that, for any object of quantified type, none of those quantifiers may ever be instantiated with the object itself. Impredicativity is associated with popular paradoxes in set theory, involving inconsistent constructions like "the set of all sets that do not contain themselves." Similar paradoxes result from uncontrolled impredicativity in Coq. *)
adamc@227 169
adamc@227 170
adamc@227 171 (** ** Inductive Definitions *)
adamc@227 172
adamc@227 173 (** Predicativity restrictions also apply to inductive definitions. As an example, let us consider a type of expression trees that allows injection of any native Coq value. The idea is that an [exp T] stands for a reflected expression of type [T].
adamc@227 174
adamc@227 175 [[
adamc@227 176 Inductive exp : Set -> Set :=
adamc@227 177 | Const : forall T : Set, T -> exp T
adamc@227 178 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 179 | Eq : forall T, exp T -> exp T -> exp bool.
adamc@227 180
adamc@227 181 Error: Large non-propositional inductive types must be in Type.
adamc@227 182
adamc@227 183 ]]
adamc@227 184
adamc@227 185 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. *)
adamc@227 186
adamc@227 187 Inductive exp : Type -> Type :=
adamc@227 188 | Const : forall T, T -> exp T
adamc@227 189 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 190 | Eq : forall T, exp T -> exp T -> exp bool.
adamc@227 191
adamc@228 192 (** Note that before we had to include an annotation [: Set] for the variable [T] in [Const]'s type, but we need no annotation now. When the type of a variable is not known, and when that variable is used in a context where only types are allowed, Coq infers that the variable is of type [Type]. That is the right behavior here, but it was wrong for the [Set] version of [exp].
adamc@228 193
adamc@228 194 Our new definition is accepted. We can build some sample expressions. *)
adamc@227 195
adamc@227 196 Check Const 0.
adamc@227 197 (** %\vspace{-.15in}% [[
adamc@227 198 Const 0
adamc@227 199 : exp nat
adamc@227 200 ]] *)
adamc@227 201
adamc@227 202 Check Pair (Const 0) (Const tt).
adamc@227 203 (** %\vspace{-.15in}% [[
adamc@227 204 Pair (Const 0) (Const tt)
adamc@227 205 : exp (nat * unit)
adamc@227 206 ]] *)
adamc@227 207
adamc@227 208 Check Eq (Const Set) (Const Type).
adamc@227 209 (** %\vspace{-.15in}% [[
adamc@228 210 Eq (Const Set) (Const Type $ Top.59 ^ )
adamc@227 211 : exp bool
adamc@227 212
adamc@227 213 ]]
adamc@227 214
adamc@227 215 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall.
adamc@227 216
adamc@227 217 [[
adamc@227 218 Check Const (Const O).
adamc@227 219
adamc@227 220 Error: Universe inconsistency (cannot enforce Top.42 < Top.42).
adamc@227 221
adamc@227 222 ]]
adamc@227 223
adamc@227 224 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. *)
adamc@227 225
adamc@227 226 Print exp.
adamc@227 227 (** %\vspace{-.15in}% [[
adamc@227 228 Inductive exp
adamc@227 229 : Type $ Top.8 ^ ->
adamc@227 230 Type
adamc@227 231 $ max(0, (Top.11)+1, (Top.14)+1, (Top.15)+1, (Top.19)+1) ^ :=
adamc@227 232 Const : forall T : Type $ Top.11 ^ , T -> exp T
adamc@227 233 | Pair : forall (T1 : Type $ Top.14 ^ ) (T2 : Type $ Top.15 ^ ),
adamc@227 234 exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 235 | Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool
adamc@227 236
adamc@227 237 ]]
adamc@227 238
adamc@227 239 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.
adamc@227 240
adamc@227 241 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. *)
adamc@227 242
adamc@227 243 Print Universes.
adamc@227 244 (** %\vspace{-.15in}% [[
adamc@227 245 Top.19 < Top.9 <= Top.8
adamc@227 246 Top.15 < Top.9 <= Top.8 <= Coq.Init.Datatypes.38
adamc@227 247 Top.14 < Top.9 <= Top.8 <= Coq.Init.Datatypes.37
adamc@227 248 Top.11 < Top.9 <= Top.8
adamc@227 249
adamc@227 250 ]]
adamc@227 251
adamc@227 252 [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.
adamc@227 253
adamc@227 254 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. *)
adamc@227 255
adamc@227 256 Print prod.
adamc@227 257 (** %\vspace{-.15in}% [[
adamc@227 258 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ )
adamc@227 259 (B : Type $ Coq.Init.Datatypes.38 ^ )
adamc@227 260 : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ :=
adamc@227 261 pair : A -> B -> A * B
adamc@227 262
adamc@227 263 ]]
adamc@227 264
adamc@227 265 We see that the constraint is enforcing that indices to [exp] must not live in a higher universe level than [B]-indices to [prod]. The next constraint above establishes a symmetric condition for [A].
adamc@227 266
adamc@227 267 Thus it is apparent that Coq maintains a tortuous set of universe variable inequalities behind the scenes. It may look like some functions are polymorphic in the universe levels of their arguments, but what is really happening is imperative updating of a system of constraints, such that all uses of a function are consistent with a global set of universe levels. When the constraint system may not be evolved soundly, we get a universe inconsistency error.
adamc@227 268
adamc@227 269 %\medskip%
adamc@227 270
adamc@227 271 Something interesting is revealed in the annotated definition of [prod]. A type [prod A B] lives at a universe that is the maximum of the universes of [A] and [B]. From our earlier experiments, we might expect that [prod]'s universe would in fact need to be %\textit{%#<i>#one higher#</i>#%}% than the maximum. The critical difference is that, in the definition of [prod], [A] and [B] are defined as %\textit{%#<i>#parameters#</i>#%}%; that is, they appear named to the left of the main colon, rather than appearing (possibly unnamed) to the right.
adamc@227 272
adamc@227 273 Parameters are not as flexible as normal inductive type arguments. The range types of all of the constructors of a parameterized type must share the same indices. Nonetheless, when it is possible to define a polymorphic type in this way, we gain the ability to use the new type family in more ways, without triggering universe inconsistencies. For instance, nested pairs of types are perfectly legal. *)
adamc@227 274
adamc@227 275 Check (nat, (Type, Set)).
adamc@227 276 (** %\vspace{-.15in}% [[
adamc@227 277 (nat, (Type $ Top.44 ^ , Set))
adamc@227 278 : Set * (Type $ Top.45 ^ * Type $ Top.46 ^ )
adamc@227 279
adamc@227 280 ]]
adamc@227 281
adamc@227 282 The same cannot be done with a counterpart to [prod] that does not use parameters. *)
adamc@227 283
adamc@227 284 Inductive prod' : Type -> Type -> Type :=
adamc@227 285 | pair' : forall A B : Type, A -> B -> prod' A B.
adamc@227 286
adamc@227 287 (** [[
adamc@227 288 Check (pair' nat (pair' Type Set)).
adamc@227 289
adamc@227 290 Error: Universe inconsistency (cannot enforce Top.51 < Top.51).
adamc@227 291
adamc@227 292 ]]
adamc@227 293
adamc@227 294 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. *)
adamc@229 295
adamc@229 296 (* begin hide *)
adamc@229 297 Unset Printing Universes.
adamc@229 298 (* end hide *)
adamc@229 299
adamc@229 300
adamc@229 301 (** * The [Prop] Universe *)
adamc@229 302
adamc@229 303 (** In Chapter 4, we saw parallel versions of useful datatypes for "programs" and "proofs." The convention was that programs live in [Set], and proofs live in [Prop]. We gave little explanation for why it is useful to maintain this distinction. There is certainly documentation value from separating programs from proofs; in practice, different concerns apply to building the two types of objects. It turns out, however, that these concerns motivate formal differences between the two universes in Coq.
adamc@229 304
adamc@229 305 Recall the types [sig] and [ex], which are the program and proof versions of existential quantification. Their definitions differ only in one place, where [sig] uses [Type] and [ex] uses [Prop]. *)
adamc@229 306
adamc@229 307 Print sig.
adamc@229 308 (** %\vspace{-.15in}% [[
adamc@229 309 Inductive sig (A : Type) (P : A -> Prop) : Type :=
adamc@229 310 exist : forall x : A, P x -> sig P
adamc@229 311 ]] *)
adamc@229 312
adamc@229 313 Print ex.
adamc@229 314 (** %\vspace{-.15in}% [[
adamc@229 315 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
adamc@229 316 ex_intro : forall x : A, P x -> ex P
adamc@229 317
adamc@229 318 ]]
adamc@229 319
adamc@229 320 It is natural to want a function to extract the first components of data structures like these. Doing so is easy enough for [sig]. *)
adamc@229 321
adamc@229 322 Definition projS A (P : A -> Prop) (x : sig P) : A :=
adamc@229 323 match x with
adamc@229 324 | exist v _ => v
adamc@229 325 end.
adamc@229 326
adamc@229 327 (** We run into trouble with a version that has been changed to work with [ex].
adamc@229 328
adamc@229 329 [[
adamc@229 330 Definition projE A (P : A -> Prop) (x : ex P) : A :=
adamc@229 331 match x with
adamc@229 332 | ex_intro v _ => v
adamc@229 333 end.
adamc@229 334
adamc@229 335 Error:
adamc@229 336 Incorrect elimination of "x" in the inductive type "ex":
adamc@229 337 the return type has sort "Type" while it should be "Prop".
adamc@229 338 Elimination of an inductive object of sort Prop
adamc@229 339 is not allowed on a predicate in sort Type
adamc@229 340 because proofs can be eliminated only to build proofs.
adamc@229 341
adamc@229 342 ]]
adamc@229 343
adamc@229 344 In formal Coq parlance, "elimination" means "pattern-matching." The typing rules of Gallina forbid us from pattern-matching on a discriminee whose types 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.
adamc@229 345
adamc@229 346 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.
adamc@229 347
adamc@229 348 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. *)
adamc@229 349
adamc@229 350 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) :=
adamc@229 351 match x with
adamc@229 352 | exist n pf => exist _ n (sym_eq pf)
adamc@229 353 end.
adamc@229 354
adamc@229 355 Extraction sym_sig.
adamc@229 356 (** <<
adamc@229 357 (** val sym_sig : nat -> nat **)
adamc@229 358
adamc@229 359 let sym_sig x = x
adamc@229 360 >>
adamc@229 361
adamc@229 362 Since extraction erases proofs, the second components of [sig] values are elided, making [sig] a simple identity type family. The [sym_sig] operation is thus an identity function. *)
adamc@229 363
adamc@229 364 Definition sym_ex (x : ex (fun n => n = 0)) : ex (fun n => 0 = n) :=
adamc@229 365 match x with
adamc@229 366 | ex_intro n pf => ex_intro _ n (sym_eq pf)
adamc@229 367 end.
adamc@229 368
adamc@229 369 Extraction sym_ex.
adamc@229 370 (** <<
adamc@229 371 (** val sym_ex : __ **)
adamc@229 372
adamc@229 373 let sym_ex = __
adamc@229 374 >>
adamc@229 375
adamc@229 376 In this example, the [ex] type itself is in [Prop], so whole [ex] packages are erased. Coq extracts every proposition as the 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.
adamc@229 377
adamc@229 378 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.
adamc@229 379
adamc@229 380 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.
adamc@229 381
adamc@229 382 %\medskip%
adamc@229 383
adamc@229 384 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. *)
adamc@229 385
adamc@229 386 Check forall P Q : Prop, P \/ Q -> Q \/ P.
adamc@229 387 (** %\vspace{-.15in}% [[
adamc@229 388 forall P Q : Prop, P \/ Q -> Q \/ P
adamc@229 389 : Prop
adamc@229 390
adamc@229 391 ]]
adamc@229 392
adamc@229 393 We see that it is possible to define a [Prop] that quantifies over other [Prop]s. This is fortunate, as we start wanting that ability even for such basic purposes as stating propositional tautologies. In the next section of this chapter, we will see some reasons why unrestricted impredicativity is undesirable. The impredicativity of [Prop] interacts crucially with the elimination restriction to avoid those pitfalls. *)