Mercurial > cpdt > repo

annotate src/Universes.v @ 287:be571572c088

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PC-inspired Universes tweaks
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 14:05:00 -0500
parents f15f7c4eebfe
children 7b38729be069
rev   line source
adam@287 1 (* Copyright (c) 2009-2010, 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@230 11 Require Import DepList Tactics.
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
adam@287 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
adam@287 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
adam@287 91 Occurrences of [Type] are annotated with some additional information, inside comments. These annotations have to do with the secret behind [Type]: it really stands for an infinite hierarchy of types. The type of [Set] is [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
adam@287 120 The behind-the-scenes manipulation of universe variables gives us predicativity. Consider this simple definition of a polymorphic identity function, where the first argument [T] will automatically be marked as implicit, since it can be inferred from the type of the second argument [x]. *)
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
adam@287 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 would 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
adam@287 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@231 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 parameters. 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@233 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@233 295
adamc@233 296 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. *)
adamc@233 297
adamc@233 298 Inductive foo (A : Type) : Type :=
adamc@233 299 | Foo : A -> foo A.
adamc@229 300
adamc@229 301 (* begin hide *)
adamc@229 302 Unset Printing Universes.
adamc@229 303 (* end hide *)
adamc@229 304
adamc@233 305 Check foo nat.
adamc@233 306 (** %\vspace{-.15in}% [[
adamc@233 307 foo nat
adamc@233 308 : Set
adamc@233 309 ]] *)
adamc@233 310
adamc@233 311 Check foo Set.
adamc@233 312 (** %\vspace{-.15in}% [[
adamc@233 313 foo Set
adamc@233 314 : Type
adamc@233 315 ]] *)
adamc@233 316
adamc@233 317 Check foo True.
adamc@233 318 (** %\vspace{-.15in}% [[
adamc@233 319 foo True
adamc@233 320 : Prop
adamc@233 321
adamc@233 322 ]]
adamc@233 323
adam@287 324 The basic pattern here is that Coq is willing to automatically build a %``%#"#copied-and-pasted#"#%''% version of an inductive definition, where some occurrences of [Type] have been replaced by [Set] or [Prop]. In each context, the type-checker tries to find the valid replacements that are lowest in the type hierarchy. Automatic cloning of definitions can be much more convenient than manual cloning. We have already taken advantage of the fact that we may re-use the same families of tuple and list types to form values in [Set] and [Type].
adamc@233 325
adamc@233 326 Imitation polymorphism can be confusing in some contexts. For instance, it is what is responsible for this weird behavior. *)
adamc@233 327
adamc@233 328 Inductive bar : Type := Bar : bar.
adamc@233 329
adamc@233 330 Check bar.
adamc@233 331 (** %\vspace{-.15in}% [[
adamc@233 332 bar
adamc@233 333 : Prop
adamc@233 334
adamc@233 335 ]]
adamc@233 336
adamc@233 337 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *)
adamc@233 338
adamc@229 339
adamc@229 340 (** * The [Prop] Universe *)
adamc@229 341
adam@287 342 (** 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 343
adamc@229 344 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 345
adamc@229 346 Print sig.
adamc@229 347 (** %\vspace{-.15in}% [[
adamc@229 348 Inductive sig (A : Type) (P : A -> Prop) : Type :=
adamc@229 349 exist : forall x : A, P x -> sig P
adamc@229 350 ]] *)
adamc@229 351
adamc@229 352 Print ex.
adamc@229 353 (** %\vspace{-.15in}% [[
adamc@229 354 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
adamc@229 355 ex_intro : forall x : A, P x -> ex P
adamc@229 356
adamc@229 357 ]]
adamc@229 358
adamc@229 359 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 360
adamc@229 361 Definition projS A (P : A -> Prop) (x : sig P) : A :=
adamc@229 362 match x with
adamc@229 363 | exist v _ => v
adamc@229 364 end.
adamc@229 365
adamc@229 366 (** We run into trouble with a version that has been changed to work with [ex].
adamc@229 367
adamc@229 368 [[
adamc@229 369 Definition projE A (P : A -> Prop) (x : ex P) : A :=
adamc@229 370 match x with
adamc@229 371 | ex_intro v _ => v
adamc@229 372 end.
adamc@229 373
adamc@229 374 Error:
adamc@229 375 Incorrect elimination of "x" in the inductive type "ex":
adamc@229 376 the return type has sort "Type" while it should be "Prop".
adamc@229 377 Elimination of an inductive object of sort Prop
adamc@229 378 is not allowed on a predicate in sort Type
adamc@229 379 because proofs can be eliminated only to build proofs.
adamc@229 380
adamc@229 381 ]]
adamc@229 382
adam@287 383 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.
adamc@229 384
adamc@229 385 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 386
adamc@229 387 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 388
adamc@229 389 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) :=
adamc@229 390 match x with
adamc@229 391 | exist n pf => exist _ n (sym_eq pf)
adamc@229 392 end.
adamc@229 393
adamc@229 394 Extraction sym_sig.
adamc@229 395 (** <<
adamc@229 396 (** val sym_sig : nat -> nat **)
adamc@229 397
adamc@229 398 let sym_sig x = x
adamc@229 399 >>
adamc@229 400
adamc@229 401 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 402
adamc@229 403 Definition sym_ex (x : ex (fun n => n = 0)) : ex (fun n => 0 = n) :=
adamc@229 404 match x with
adamc@229 405 | ex_intro n pf => ex_intro _ n (sym_eq pf)
adamc@229 406 end.
adamc@229 407
adamc@229 408 Extraction sym_ex.
adamc@229 409 (** <<
adamc@229 410 (** val sym_ex : __ **)
adamc@229 411
adamc@229 412 let sym_ex = __
adamc@229 413 >>
adamc@229 414
adam@287 415 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.
adamc@229 416
adamc@229 417 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 418
adamc@229 419 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 420
adamc@229 421 %\medskip%
adamc@229 422
adamc@229 423 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 424
adamc@229 425 Check forall P Q : Prop, P \/ Q -> Q \/ P.
adamc@229 426 (** %\vspace{-.15in}% [[
adamc@229 427 forall P Q : Prop, P \/ Q -> Q \/ P
adamc@229 428 : Prop
adamc@229 429
adamc@229 430 ]]
adamc@229 431
adamc@230 432 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.
adamc@230 433
adamc@230 434 Impredicativity also allows us to implement a version of our earlier [exp] type that does not suffer from the weakness that we found. *)
adamc@230 435
adamc@230 436 Inductive expP : Type -> Prop :=
adamc@230 437 | ConstP : forall T, T -> expP T
adamc@230 438 | PairP : forall T1 T2, expP T1 -> expP T2 -> expP (T1 * T2)
adamc@230 439 | EqP : forall T, expP T -> expP T -> expP bool.
adamc@230 440
adamc@230 441 Check ConstP 0.
adamc@230 442 (** %\vspace{-.15in}% [[
adamc@230 443 ConstP 0
adamc@230 444 : expP nat
adamc@230 445 ]] *)
adamc@230 446
adamc@230 447 Check PairP (ConstP 0) (ConstP tt).
adamc@230 448 (** %\vspace{-.15in}% [[
adamc@230 449 PairP (ConstP 0) (ConstP tt)
adamc@230 450 : expP (nat * unit)
adamc@230 451 ]] *)
adamc@230 452
adamc@230 453 Check EqP (ConstP Set) (ConstP Type).
adamc@230 454 (** %\vspace{-.15in}% [[
adamc@230 455 EqP (ConstP Set) (ConstP Type)
adamc@230 456 : expP bool
adamc@230 457 ]] *)
adamc@230 458
adamc@230 459 Check ConstP (ConstP O).
adamc@230 460 (** %\vspace{-.15in}% [[
adamc@230 461 ConstP (ConstP 0)
adamc@230 462 : expP (expP nat)
adamc@230 463
adamc@230 464 ]]
adamc@230 465
adam@287 466 In this case, our victory is really a shallow one. As we have marked [expP] as a family of proofs, we cannot deconstruct our expressions in the usual programmatic ways, which makes them almost useless for the usual purposes. Impredicative quantification is much more useful in defining inductive families that we really think of as judgments. For instance, this code defines a notion of equality that is strictly more permissive than the base equality [=]. *)
adamc@230 467
adamc@230 468 Inductive eqPlus : forall T, T -> T -> Prop :=
adamc@230 469 | Base : forall T (x : T), eqPlus x x
adamc@230 470 | Func : forall dom ran (f1 f2 : dom -> ran),
adamc@230 471 (forall x : dom, eqPlus (f1 x) (f2 x))
adamc@230 472 -> eqPlus f1 f2.
adamc@230 473
adamc@230 474 Check (Base 0).
adamc@230 475 (** %\vspace{-.15in}% [[
adamc@230 476 Base 0
adamc@230 477 : eqPlus 0 0
adamc@230 478 ]] *)
adamc@230 479
adamc@230 480 Check (Func (fun n => n) (fun n => 0 + n) (fun n => Base n)).
adamc@230 481 (** %\vspace{-.15in}% [[
adamc@230 482 Func (fun n : nat => n) (fun n : nat => 0 + n) (fun n : nat => Base n)
adamc@230 483 : eqPlus (fun n : nat => n) (fun n : nat => 0 + n)
adamc@230 484 ]] *)
adamc@230 485
adamc@230 486 Check (Base (Base 1)).
adamc@230 487 (** %\vspace{-.15in}% [[
adamc@230 488 Base (Base 1)
adamc@230 489 : eqPlus (Base 1) (Base 1)
adamc@230 490 ]] *)
adamc@230 491
adamc@230 492
adamc@230 493 (** * Axioms *)
adamc@230 494
adamc@230 495 (** 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.
adamc@230 496
adamc@230 497 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. *)
adamc@230 498
adamc@230 499 (** ** The Basics *)
adamc@230 500
adamc@231 501 (** One simple example of a useful axiom is the law of the excluded middle. *)
adamc@230 502
adamc@230 503 Require Import Classical_Prop.
adamc@230 504 Print classic.
adamc@230 505 (** %\vspace{-.15in}% [[
adamc@230 506 *** [ classic : forall P : Prop, P \/ ~ P ]
adamc@230 507
adamc@230 508 ]]
adamc@230 509
adamc@230 510 In the implementation of module [Classical_Prop], this axiom was defined with the command *)
adamc@230 511
adamc@230 512 Axiom classic : forall P : Prop, P \/ ~ P.
adamc@230 513
adamc@230 514 (** 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. *)
adamc@230 515
adamc@230 516 Parameter n : nat.
adamc@230 517 Axiom positive : n > 0.
adamc@230 518 Reset n.
adamc@230 519
adam@287 520 (** 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.
adamc@230 521
adamc@230 522 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]. *)
adamc@230 523
adam@287 524 Axiom not_classic : ~ forall P : Prop, P \/ ~ P.
adamc@230 525
adamc@230 526 Theorem uhoh : False.
adam@287 527 generalize classic not_classic; tauto.
adamc@230 528 Qed.
adamc@230 529
adamc@230 530 Theorem uhoh_again : 1 + 1 = 3.
adamc@230 531 destruct uhoh.
adamc@230 532 Qed.
adamc@230 533
adamc@230 534 Reset not_classic.
adamc@230 535
adam@287 536 (** 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.
adamc@230 537
adamc@230 538 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.
adamc@230 539
adamc@231 540 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.
adamc@230 541
adamc@230 542 Because the proper use of axioms is so precarious, there are helpful commands for determining which axioms a theorem relies on. *)
adamc@230 543
adamc@230 544 Theorem t1 : forall P : Prop, P -> ~ ~ P.
adamc@230 545 tauto.
adamc@230 546 Qed.
adamc@230 547
adamc@230 548 Print Assumptions t1.
adamc@230 549 (** %\vspace{-.15in}% [[
adamc@230 550 Closed under the global context
adamc@230 551 ]] *)
adamc@230 552
adamc@230 553 Theorem t2 : forall P : Prop, ~ ~ P -> P.
adamc@230 554 (** [[
adamc@230 555 tauto.
adamc@230 556
adamc@230 557 Error: tauto failed.
adamc@230 558
adamc@230 559 ]] *)
adamc@230 560
adamc@230 561 intro P; destruct (classic P); tauto.
adamc@230 562 Qed.
adamc@230 563
adamc@230 564 Print Assumptions t2.
adamc@230 565 (** %\vspace{-.15in}% [[
adamc@230 566 Axioms:
adamc@230 567 classic : forall P : Prop, P \/ ~ P
adamc@230 568
adamc@230 569 ]]
adamc@230 570
adamc@231 571 It is possible to avoid this dependence in some specific cases, where excluded middle %\textit{%#<i>#is#</i>#%}% provable, for decidable families of propositions. *)
adamc@230 572
adam@287 573 Theorem nat_eq_dec : forall n m : nat, n = m \/ n <> m.
adamc@230 574 induction n; destruct m; intuition; generalize (IHn m); intuition.
adamc@230 575 Qed.
adamc@230 576
adamc@230 577 Theorem t2' : forall n m : nat, ~ ~ (n = m) -> n = m.
adam@287 578 intros n m; destruct (nat_eq_dec n m); tauto.
adamc@230 579 Qed.
adamc@230 580
adamc@230 581 Print Assumptions t2'.
adamc@230 582 (** %\vspace{-.15in}% [[
adamc@230 583 Closed under the global context
adamc@230 584 ]]
adamc@230 585
adamc@230 586 %\bigskip%
adamc@230 587
adamc@230 588 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. *)
adamc@230 589
adamc@230 590 Require Import ProofIrrelevance.
adamc@230 591 Print proof_irrelevance.
adamc@230 592 (** %\vspace{-.15in}% [[
adamc@230 593 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ]
adamc@230 594
adamc@230 595 ]]
adamc@230 596
adamc@231 597 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. *)
adamc@230 598
adamc@230 599 (* begin hide *)
adamc@230 600 Lemma zgtz : 0 > 0 -> False.
adamc@230 601 crush.
adamc@230 602 Qed.
adamc@230 603 (* end hide *)
adamc@230 604
adamc@230 605 Definition pred_strong1 (n : nat) : n > 0 -> nat :=
adamc@230 606 match n with
adamc@230 607 | O => fun pf : 0 > 0 => match zgtz pf with end
adamc@230 608 | S n' => fun _ => n'
adamc@230 609 end.
adamc@230 610
adamc@230 611 (** We might want to prove that different proofs of [n > 0] do not lead to different results from our richly-typed predecessor function. *)
adamc@230 612
adamc@230 613 Theorem pred_strong1_irrel : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
adamc@230 614 destruct n; crush.
adamc@230 615 Qed.
adamc@230 616
adamc@230 617 (** The proof script is simple, but it involved peeking into the definition of [pred_strong1]. For more complicated function definitions, it can be considerably more work to prove that they do not discriminate on details of proof arguments. This can seem like a shame, since the [Prop] elimination restriction makes it impossible to write any function that does otherwise. Unfortunately, this fact is only true metatheoretically, unless we assert an axiom like [proof_irrelevance]. With that axiom, we can prove our theorem without consulting the definition of [pred_strong1]. *)
adamc@230 618
adamc@230 619 Theorem pred_strong1_irrel' : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
adamc@230 620 intros; f_equal; apply proof_irrelevance.
adamc@230 621 Qed.
adamc@230 622
adamc@230 623
adamc@230 624 (** %\bigskip%
adamc@230 625
adamc@230 626 In the chapter on equality, we already discussed some axioms that are related to proof irrelevance. In particular, Coq's standard library includes this axiom: *)
adamc@230 627
adamc@230 628 Require Import Eqdep.
adamc@230 629 Import Eq_rect_eq.
adamc@230 630 Print eq_rect_eq.
adamc@230 631 (** %\vspace{-.15in}% [[
adamc@230 632 *** [ eq_rect_eq :
adamc@230 633 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@230 634 x = eq_rect p Q x p h ]
adamc@230 635
adamc@230 636 ]]
adamc@230 637
adamc@230 638 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. *)
adamc@230 639
adamc@230 640 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = refl_equal x.
adamc@230 641 intros; replace pf with (eq_rect x (eq x) (refl_equal x) x pf); [
adamc@230 642 symmetry; apply eq_rect_eq
adamc@230 643 | exact (match pf as pf' return match pf' in _ = y return x = y with
adamc@230 644 | refl_equal => refl_equal x
adamc@230 645 end = pf' with
adamc@230 646 | refl_equal => refl_equal _
adamc@230 647 end) ].
adamc@230 648 Qed.
adamc@230 649
adamc@230 650 Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2.
adamc@230 651 intros; generalize pf1 pf2; subst; intros;
adamc@230 652 match goal with
adamc@230 653 | [ |- ?pf1 = ?pf2 ] => rewrite (UIP_refl pf1); rewrite (UIP_refl pf2); reflexivity
adamc@230 654 end.
adamc@230 655 Qed.
adamc@230 656
adamc@231 657 (** These corollaries are special cases of proof irrelevance. In developments that only need proof irrelevance for equality, there is no need to assert full irrelevance.
adamc@230 658
adamc@230 659 Another facet of proof irrelevance is that, like excluded middle, it is often provable for specific propositions. For instance, [UIP] is provable whenever the type [A] has a decidable equality operation. The module [Eqdep_dec] of the standard library contains a proof. A similar phenomenon applies to other notable cases, including less-than proofs. Thus, it is often possible to use proof irrelevance without asserting axioms.
adamc@230 660
adamc@230 661 %\bigskip%
adamc@230 662
adamc@230 663 There are two more basic axioms that are often assumed, to avoid complications that do not arise in set theory. *)
adamc@230 664
adamc@230 665 Require Import FunctionalExtensionality.
adamc@230 666 Print functional_extensionality_dep.
adamc@230 667 (** %\vspace{-.15in}% [[
adamc@230 668 *** [ functional_extensionality_dep :
adamc@230 669 forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
adamc@230 670 (forall x : A, f x = g x) -> f = g ]
adamc@230 671
adamc@230 672 ]]
adamc@230 673
adamc@230 674 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.
adamc@230 675
adamc@230 676 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. *)
adamc@230 677
adamc@230 678 Corollary predicate_extensionality : forall (A : Type) (B : A -> Prop) (f g : forall x : A, B x),
adamc@230 679 (forall x : A, f x = g x) -> f = g.
adamc@230 680 intros; apply functional_extensionality_dep; assumption.
adamc@230 681 Qed.
adamc@230 682
adamc@230 683
adamc@230 684 (** ** Axioms of Choice *)
adamc@230 685
adamc@230 686 (** 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.
adamc@230 687
adamc@230 688 First, it is possible to implement a choice operator %\textit{%#<i>#without#</i>#%}% axioms in some potentially surprising cases. *)
adamc@230 689
adamc@230 690 Require Import ConstructiveEpsilon.
adamc@230 691 Check constructive_definite_description.
adamc@230 692 (** %\vspace{-.15in}% [[
adamc@230 693 constructive_definite_description
adamc@230 694 : forall (A : Set) (f : A -> nat) (g : nat -> A),
adamc@230 695 (forall x : A, g (f x) = x) ->
adamc@230 696 forall P : A -> Prop,
adamc@230 697 (forall x : A, {P x} + {~ P x}) ->
adamc@230 698 (exists! x : A, P x) -> {x : A | P x}
adamc@230 699 ]] *)
adamc@230 700
adamc@230 701 Print Assumptions constructive_definite_description.
adamc@230 702 (** %\vspace{-.15in}% [[
adamc@230 703 Closed under the global context
adamc@230 704
adamc@230 705 ]]
adamc@230 706
adamc@231 707 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.
adamc@230 708
adamc@230 709 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. *)
adamc@230 710
adamc@230 711 Require Import ClassicalUniqueChoice.
adamc@230 712 Check dependent_unique_choice.
adamc@230 713 (** %\vspace{-.15in}% [[
adamc@230 714 dependent_unique_choice
adamc@230 715 : forall (A : Type) (B : A -> Type) (R : forall x : A, B x -> Prop),
adamc@230 716 (forall x : A, exists! y : B x, R x y) ->
adamc@230 717 exists f : forall x : A, B x, forall x : A, R x (f x)
adamc@230 718
adamc@230 719 ]]
adamc@230 720
adamc@230 721 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. *)
adamc@230 722
adamc@230 723 Require Import ClassicalChoice.
adamc@230 724 Check choice.
adamc@230 725 (** %\vspace{-.15in}% [[
adamc@230 726 choice
adamc@230 727 : forall (A B : Type) (R : A -> B -> Prop),
adamc@230 728 (forall x : A, exists y : B, R x y) ->
adamc@230 729 exists f : A -> B, forall x : A, R x (f x)
adamc@230 730
adamc@230 731 ]]
adamc@230 732
adamc@230 733 This principle is proved as a theorem, based on the unique choice axiom and an additional axiom of relational choice from the [RelationalChoice] module.
adamc@230 734
adamc@230 735 In set theory, the axiom of choice is a fundamental philosophical commitment one makes about the universe of sets. In Coq, the choice axioms say something weaker. For instance, consider the simple restatement of the [choice] axiom where we replace existential quantification by its Curry-Howard analogue, subset types. *)
adamc@230 736
adamc@230 737 Definition choice_Set (A B : Type) (R : A -> B -> Prop) (H : forall x : A, {y : B | R x y})
adamc@230 738 : {f : A -> B | forall x : A, R x (f x)} :=
adamc@230 739 exist (fun f => forall x : A, R x (f x))
adamc@230 740 (fun x => proj1_sig (H x)) (fun x => proj2_sig (H x)).
adamc@230 741
adam@287 742 (** Via the Curry-Howard correspondence, this %``%#"#axiom#"#%''% can be taken to have the same meaning as the original. It is implemented trivially as a transformation not much deeper than uncurrying. Thus, we see that the utility of the axioms that we mentioned earlier comes in their usage to build programs from proofs. Normal set theory has no explicit proofs, so the meaning of the usual axiom of choice is subtlely different. In Gallina, the axioms implement a controlled relaxation of the restrictions on information flow from proofs to programs.
adamc@230 743
adam@287 744 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.
adamc@230 745
adamc@230 746 %\bigskip%
adamc@230 747
adamc@230 748 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].
adamc@230 749
adamc@230 750 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. *)
adamc@230 751
adamc@230 752 (** ** Axioms and Computation *)
adamc@230 753
adamc@230 754 (** One additional axiom-related wrinkle arises from an aspect of Gallina that is very different from set theory: a notion of %\textit{%#<i>#computational equivalence#</i>#%}% is central to the definition of the formal system. Axioms tend not to play well with computation. Consider this example. We start by implementing a function that uses a type equality proof to perform a safe type-cast. *)
adamc@230 755
adamc@230 756 Definition cast (x y : Set) (pf : x = y) (v : x) : y :=
adamc@230 757 match pf with
adamc@230 758 | refl_equal => v
adamc@230 759 end.
adamc@230 760
adamc@230 761 (** Computation over programs that use [cast] can proceed smoothly. *)
adamc@230 762
adamc@230 763 Eval compute in (cast (refl_equal (nat -> nat)) (fun n => S n)) 12.
adamc@230 764 (** [[
adamc@230 765 = 13
adamc@230 766 : nat
adamc@230 767 ]] *)
adamc@230 768
adamc@230 769 (** Things do not go as smoothly when we use [cast] with proofs that rely on axioms. *)
adamc@230 770
adamc@230 771 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
adamc@230 772 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
adamc@230 773 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
adamc@230 774 Qed.
adamc@230 775
adamc@230 776 Eval compute in (cast t3 (fun _ => First)) 12.
adamc@230 777 (** [[
adamc@230 778 = match t3 in (_ = P) return P with
adamc@230 779 | refl_equal => fun n : nat => First
adamc@230 780 end 12
adamc@230 781 : fin (12 + 1)
adamc@230 782
adamc@230 783 ]]
adamc@230 784
adamc@230 785 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. *)
adamc@230 786
adamc@230 787 Reset t3.
adamc@230 788
adamc@230 789 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
adamc@230 790 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
adamc@230 791 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
adamc@230 792 Defined.
adamc@230 793
adamc@230 794 Eval compute in (cast t3 (fun _ => First)) 12.
adamc@230 795 (** [[
adamc@230 796 = match
adamc@230 797 match
adamc@230 798 match
adamc@230 799 functional_extensionality
adamc@230 800 ....
adamc@230 801
adamc@230 802 ]]
adamc@230 803
adamc@230 804 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.
adamc@230 805
adamc@230 806 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *)
adamc@230 807
adamc@230 808 Lemma plus1 : forall n, S n = n + 1.
adamc@230 809 induction n; simpl; intuition.
adamc@230 810 Defined.
adamc@230 811
adamc@230 812 Theorem t4 : forall n, fin (S n) = fin (n + 1).
adamc@230 813 intro; f_equal; apply plus1.
adamc@230 814 Defined.
adamc@230 815
adamc@230 816 Eval compute in cast (t4 13) First.
adamc@230 817 (** %\vspace{-.15in}% [[
adamc@230 818 = First
adamc@230 819 : fin (13 + 1)
adamc@230 820 ]] *)