Mercurial > cpdt > repo

annotate src/Universes.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents be571572c088
children d5787b70cf48
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
adam@302 72 ]]
adam@302 73 *)
adamc@227 74
adamc@227 75 (** printing $ %({}*% #(<a/>*# *)
adamc@227 76 (** printing ^ %*{})% #*<a/>)# *)
adamc@227 77
adamc@227 78 Check Set.
adamc@227 79 (** %\vspace{-.15in}% [[
adamc@227 80 Set
adamc@227 81 : Type $ (0)+1 ^
adamc@227 82
adam@302 83 ]]
adam@302 84 *)
adamc@227 85
adamc@227 86 Check Type.
adamc@227 87 (** %\vspace{-.15in}% [[
adamc@227 88 Type $ Top.3 ^
adamc@227 89 : Type $ (Top.3)+1 ^
adamc@227 90
adamc@227 91 ]]
adamc@227 92
adam@287 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].
adamc@227 94
adamc@227 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].
adamc@227 96
adamc@227 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.
adamc@227 98
adamc@227 99 Another crucial concept in CIC is %\textit{%#<i>#predicativity#</i>#%}%. Consider these queries. *)
adamc@227 100
adamc@227 101 Check forall T : nat, fin T.
adamc@227 102 (** %\vspace{-.15in}% [[
adamc@227 103 forall T : nat, fin T
adamc@227 104 : Set
adam@302 105 ]]
adam@302 106 *)
adamc@227 107
adamc@227 108 Check forall T : Set, T.
adamc@227 109 (** %\vspace{-.15in}% [[
adamc@227 110 forall T : Set, T
adamc@227 111 : Type $ max(0, (0)+1) ^
adam@302 112 ]]
adam@302 113 *)
adamc@227 114
adamc@227 115 Check forall T : Type, T.
adamc@227 116 (** %\vspace{-.15in}% [[
adamc@227 117 forall T : Type $ Top.9 ^ , T
adamc@227 118 : Type $ max(Top.9, (Top.9)+1) ^
adamc@227 119
adamc@227 120 ]]
adamc@227 121
adamc@227 122 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 123
adam@287 124 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 125
adamc@227 126 Definition id (T : Set) (x : T) : T := x.
adamc@227 127
adamc@227 128 Check id 0.
adamc@227 129 (** %\vspace{-.15in}% [[
adamc@227 130 id 0
adamc@227 131 : nat
adamc@227 132
adamc@227 133 Check id Set.
adamc@227 134
adamc@227 135 Error: Illegal application (Type Error):
adamc@227 136 ...
adamc@228 137 The 1st term has type "Type $ (Top.15)+1 ^" which should be coercible to "Set".
adamc@227 138
adamc@227 139 ]]
adamc@227 140
adamc@227 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]. *)
adamc@227 142
adamc@227 143 Reset id.
adamc@227 144 Definition id (T : Type) (x : T) : T := x.
adamc@227 145 Check id 0.
adamc@227 146 (** %\vspace{-.15in}% [[
adamc@227 147 id 0
adamc@227 148 : nat
adam@302 149 ]]
adam@302 150 *)
adamc@227 151
adamc@227 152 Check id Set.
adamc@227 153 (** %\vspace{-.15in}% [[
adamc@227 154 id Set
adamc@227 155 : Type $ Top.17 ^
adam@302 156 ]]
adam@302 157 *)
adamc@227 158
adamc@227 159 Check id Type.
adamc@227 160 (** %\vspace{-.15in}% [[
adamc@227 161 id Type $ Top.18 ^
adamc@227 162 : Type $ Top.19 ^
adam@302 163 ]]
adam@302 164 *)
adamc@227 165
adamc@227 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.
adamc@227 167
adamc@227 168 [[
adamc@227 169 Check id id.
adamc@227 170
adamc@227 171 Error: Universe inconsistency (cannot enforce Top.16 < Top.16).
adamc@227 172
adamc@227 173 ]]
adamc@227 174
adam@287 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. *)
adamc@227 176
adamc@227 177
adamc@227 178 (** ** Inductive Definitions *)
adamc@227 179
adamc@227 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].
adamc@227 181
adamc@227 182 [[
adamc@227 183 Inductive exp : Set -> Set :=
adamc@227 184 | Const : forall T : Set, T -> exp T
adamc@227 185 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 186 | Eq : forall T, exp T -> exp T -> exp bool.
adamc@227 187
adamc@227 188 Error: Large non-propositional inductive types must be in Type.
adamc@227 189
adamc@227 190 ]]
adamc@227 191
adamc@227 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. *)
adamc@227 193
adamc@227 194 Inductive exp : Type -> Type :=
adamc@227 195 | Const : forall T, T -> exp T
adamc@227 196 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 197 | Eq : forall T, exp T -> exp T -> exp bool.
adamc@227 198
adamc@228 199 (** 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 200
adamc@228 201 Our new definition is accepted. We can build some sample expressions. *)
adamc@227 202
adamc@227 203 Check Const 0.
adamc@227 204 (** %\vspace{-.15in}% [[
adamc@227 205 Const 0
adamc@227 206 : exp nat
adam@302 207 ]]
adam@302 208 *)
adamc@227 209
adamc@227 210 Check Pair (Const 0) (Const tt).
adamc@227 211 (** %\vspace{-.15in}% [[
adamc@227 212 Pair (Const 0) (Const tt)
adamc@227 213 : exp (nat * unit)
adam@302 214 ]]
adam@302 215 *)
adamc@227 216
adamc@227 217 Check Eq (Const Set) (Const Type).
adamc@227 218 (** %\vspace{-.15in}% [[
adamc@228 219 Eq (Const Set) (Const Type $ Top.59 ^ )
adamc@227 220 : exp bool
adamc@227 221
adamc@227 222 ]]
adamc@227 223
adamc@227 224 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall.
adamc@227 225
adamc@227 226 [[
adamc@227 227 Check Const (Const O).
adamc@227 228
adamc@227 229 Error: Universe inconsistency (cannot enforce Top.42 < Top.42).
adamc@227 230
adamc@227 231 ]]
adamc@227 232
adamc@227 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. *)
adamc@227 234
adamc@227 235 Print exp.
adamc@227 236 (** %\vspace{-.15in}% [[
adamc@227 237 Inductive exp
adamc@227 238 : Type $ Top.8 ^ ->
adamc@227 239 Type
adamc@227 240 $ max(0, (Top.11)+1, (Top.14)+1, (Top.15)+1, (Top.19)+1) ^ :=
adamc@227 241 Const : forall T : Type $ Top.11 ^ , T -> exp T
adamc@227 242 | Pair : forall (T1 : Type $ Top.14 ^ ) (T2 : Type $ Top.15 ^ ),
adamc@227 243 exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 244 | Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool
adamc@227 245
adamc@227 246 ]]
adamc@227 247
adamc@227 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.
adamc@227 249
adam@287 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. *)
adamc@227 251
adamc@227 252 Print Universes.
adamc@227 253 (** %\vspace{-.15in}% [[
adamc@227 254 Top.19 < Top.9 <= Top.8
adamc@227 255 Top.15 < Top.9 <= Top.8 <= Coq.Init.Datatypes.38
adamc@227 256 Top.14 < Top.9 <= Top.8 <= Coq.Init.Datatypes.37
adamc@227 257 Top.11 < Top.9 <= Top.8
adamc@227 258
adamc@227 259 ]]
adamc@227 260
adamc@227 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.
adamc@227 262
adamc@227 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. *)
adamc@227 264
adamc@227 265 Print prod.
adamc@227 266 (** %\vspace{-.15in}% [[
adamc@227 267 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ )
adamc@227 268 (B : Type $ Coq.Init.Datatypes.38 ^ )
adamc@227 269 : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ :=
adamc@227 270 pair : A -> B -> A * B
adamc@227 271
adamc@227 272 ]]
adamc@227 273
adamc@227 274 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 275
adamc@227 276 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 277
adamc@227 278 %\medskip%
adamc@227 279
adamc@227 280 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 281
adamc@231 282 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 283
adamc@227 284 Check (nat, (Type, Set)).
adamc@227 285 (** %\vspace{-.15in}% [[
adamc@227 286 (nat, (Type $ Top.44 ^ , Set))
adamc@227 287 : Set * (Type $ Top.45 ^ * Type $ Top.46 ^ )
adamc@227 288
adamc@227 289 ]]
adamc@227 290
adamc@227 291 The same cannot be done with a counterpart to [prod] that does not use parameters. *)
adamc@227 292
adamc@227 293 Inductive prod' : Type -> Type -> Type :=
adamc@227 294 | pair' : forall A B : Type, A -> B -> prod' A B.
adamc@227 295
adamc@227 296 (** [[
adamc@227 297 Check (pair' nat (pair' Type Set)).
adamc@227 298
adamc@227 299 Error: Universe inconsistency (cannot enforce Top.51 < Top.51).
adamc@227 300
adamc@227 301 ]]
adamc@227 302
adamc@233 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.
adamc@233 304
adamc@233 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. *)
adamc@233 306
adamc@233 307 Inductive foo (A : Type) : Type :=
adamc@233 308 | Foo : A -> foo A.
adamc@229 309
adamc@229 310 (* begin hide *)
adamc@229 311 Unset Printing Universes.
adamc@229 312 (* end hide *)
adamc@229 313
adamc@233 314 Check foo nat.
adamc@233 315 (** %\vspace{-.15in}% [[
adamc@233 316 foo nat
adamc@233 317 : Set
adam@302 318 ]]
adam@302 319 *)
adamc@233 320
adamc@233 321 Check foo Set.
adamc@233 322 (** %\vspace{-.15in}% [[
adamc@233 323 foo Set
adamc@233 324 : Type
adam@302 325 ]]
adam@302 326 *)
adamc@233 327
adamc@233 328 Check foo True.
adamc@233 329 (** %\vspace{-.15in}% [[
adamc@233 330 foo True
adamc@233 331 : Prop
adamc@233 332
adamc@233 333 ]]
adamc@233 334
adam@287 335 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 336
adamc@233 337 Imitation polymorphism can be confusing in some contexts. For instance, it is what is responsible for this weird behavior. *)
adamc@233 338
adamc@233 339 Inductive bar : Type := Bar : bar.
adamc@233 340
adamc@233 341 Check bar.
adamc@233 342 (** %\vspace{-.15in}% [[
adamc@233 343 bar
adamc@233 344 : Prop
adamc@233 345
adamc@233 346 ]]
adamc@233 347
adamc@233 348 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *)
adamc@233 349
adamc@229 350
adamc@229 351 (** * The [Prop] Universe *)
adamc@229 352
adam@287 353 (** 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 354
adamc@229 355 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 356
adamc@229 357 Print sig.
adamc@229 358 (** %\vspace{-.15in}% [[
adamc@229 359 Inductive sig (A : Type) (P : A -> Prop) : Type :=
adamc@229 360 exist : forall x : A, P x -> sig P
adam@302 361 ]]
adam@302 362 *)
adamc@229 363
adamc@229 364 Print ex.
adamc@229 365 (** %\vspace{-.15in}% [[
adamc@229 366 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
adamc@229 367 ex_intro : forall x : A, P x -> ex P
adamc@229 368
adamc@229 369 ]]
adamc@229 370
adamc@229 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]. *)
adamc@229 372
adamc@229 373 Definition projS A (P : A -> Prop) (x : sig P) : A :=
adamc@229 374 match x with
adamc@229 375 | exist v _ => v
adamc@229 376 end.
adamc@229 377
adamc@229 378 (** We run into trouble with a version that has been changed to work with [ex].
adamc@229 379
adamc@229 380 [[
adamc@229 381 Definition projE A (P : A -> Prop) (x : ex P) : A :=
adamc@229 382 match x with
adamc@229 383 | ex_intro v _ => v
adamc@229 384 end.
adamc@229 385
adamc@229 386 Error:
adamc@229 387 Incorrect elimination of "x" in the inductive type "ex":
adamc@229 388 the return type has sort "Type" while it should be "Prop".
adamc@229 389 Elimination of an inductive object of sort Prop
adamc@229 390 is not allowed on a predicate in sort Type
adamc@229 391 because proofs can be eliminated only to build proofs.
adamc@229 392
adamc@229 393 ]]
adamc@229 394
adam@287 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.
adamc@229 396
adamc@229 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.
adamc@229 398
adamc@229 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. *)
adamc@229 400
adamc@229 401 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) :=
adamc@229 402 match x with
adamc@229 403 | exist n pf => exist _ n (sym_eq pf)
adamc@229 404 end.
adamc@229 405
adamc@229 406 Extraction sym_sig.
adamc@229 407 (** <<
adamc@229 408 (** val sym_sig : nat -> nat **)
adamc@229 409
adamc@229 410 let sym_sig x = x
adamc@229 411 >>
adamc@229 412
adamc@229 413 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 414
adamc@229 415 Definition sym_ex (x : ex (fun n => n = 0)) : ex (fun n => 0 = n) :=
adamc@229 416 match x with
adamc@229 417 | ex_intro n pf => ex_intro _ n (sym_eq pf)
adamc@229 418 end.
adamc@229 419
adamc@229 420 Extraction sym_ex.
adamc@229 421 (** <<
adamc@229 422 (** val sym_ex : __ **)
adamc@229 423
adamc@229 424 let sym_ex = __
adamc@229 425 >>
adamc@229 426
adam@302 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.
adamc@229 428
adamc@229 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.
adamc@229 430
adamc@229 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.
adamc@229 432
adamc@229 433 %\medskip%
adamc@229 434
adamc@229 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. *)
adamc@229 436
adamc@229 437 Check forall P Q : Prop, P \/ Q -> Q \/ P.
adamc@229 438 (** %\vspace{-.15in}% [[
adamc@229 439 forall P Q : Prop, P \/ Q -> Q \/ P
adamc@229 440 : Prop
adamc@229 441
adamc@229 442 ]]
adamc@229 443
adamc@230 444 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 445
adamc@230 446 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 447
adamc@230 448 Inductive expP : Type -> Prop :=
adamc@230 449 | ConstP : forall T, T -> expP T
adamc@230 450 | PairP : forall T1 T2, expP T1 -> expP T2 -> expP (T1 * T2)
adamc@230 451 | EqP : forall T, expP T -> expP T -> expP bool.
adamc@230 452
adamc@230 453 Check ConstP 0.
adamc@230 454 (** %\vspace{-.15in}% [[
adamc@230 455 ConstP 0
adamc@230 456 : expP nat
adam@302 457 ]]
adam@302 458 *)
adamc@230 459
adamc@230 460 Check PairP (ConstP 0) (ConstP tt).
adamc@230 461 (** %\vspace{-.15in}% [[
adamc@230 462 PairP (ConstP 0) (ConstP tt)
adamc@230 463 : expP (nat * unit)
adam@302 464 ]]
adam@302 465 *)
adamc@230 466
adamc@230 467 Check EqP (ConstP Set) (ConstP Type).
adamc@230 468 (** %\vspace{-.15in}% [[
adamc@230 469 EqP (ConstP Set) (ConstP Type)
adamc@230 470 : expP bool
adam@302 471 ]]
adam@302 472 *)
adamc@230 473
adamc@230 474 Check ConstP (ConstP O).
adamc@230 475 (** %\vspace{-.15in}% [[
adamc@230 476 ConstP (ConstP 0)
adamc@230 477 : expP (expP nat)
adamc@230 478
adamc@230 479 ]]
adamc@230 480
adam@287 481 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 482
adamc@230 483 Inductive eqPlus : forall T, T -> T -> Prop :=
adamc@230 484 | Base : forall T (x : T), eqPlus x x
adamc@230 485 | Func : forall dom ran (f1 f2 : dom -> ran),
adamc@230 486 (forall x : dom, eqPlus (f1 x) (f2 x))
adamc@230 487 -> eqPlus f1 f2.
adamc@230 488
adamc@230 489 Check (Base 0).
adamc@230 490 (** %\vspace{-.15in}% [[
adamc@230 491 Base 0
adamc@230 492 : eqPlus 0 0
adam@302 493 ]]
adam@302 494 *)
adamc@230 495
adamc@230 496 Check (Func (fun n => n) (fun n => 0 + n) (fun n => Base n)).
adamc@230 497 (** %\vspace{-.15in}% [[
adamc@230 498 Func (fun n : nat => n) (fun n : nat => 0 + n) (fun n : nat => Base n)
adamc@230 499 : eqPlus (fun n : nat => n) (fun n : nat => 0 + n)
adam@302 500 ]]
adam@302 501 *)
adamc@230 502
adamc@230 503 Check (Base (Base 1)).
adamc@230 504 (** %\vspace{-.15in}% [[
adamc@230 505 Base (Base 1)
adamc@230 506 : eqPlus (Base 1) (Base 1)
adam@302 507 ]]
adam@302 508 *)
adamc@230 509
adamc@230 510
adamc@230 511 (** * Axioms *)
adamc@230 512
adamc@230 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.
adamc@230 514
adamc@230 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. *)
adamc@230 516
adamc@230 517 (** ** The Basics *)
adamc@230 518
adamc@231 519 (** One simple example of a useful axiom is the law of the excluded middle. *)
adamc@230 520
adamc@230 521 Require Import Classical_Prop.
adamc@230 522 Print classic.
adamc@230 523 (** %\vspace{-.15in}% [[
adamc@230 524 *** [ classic : forall P : Prop, P \/ ~ P ]
adamc@230 525
adamc@230 526 ]]
adamc@230 527
adamc@230 528 In the implementation of module [Classical_Prop], this axiom was defined with the command *)
adamc@230 529
adamc@230 530 Axiom classic : forall P : Prop, P \/ ~ P.
adamc@230 531
adamc@230 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. *)
adamc@230 533
adamc@230 534 Parameter n : nat.
adamc@230 535 Axiom positive : n > 0.
adamc@230 536 Reset n.
adamc@230 537
adam@287 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.
adamc@230 539
adamc@230 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]. *)
adamc@230 541
adam@287 542 Axiom not_classic : ~ forall P : Prop, P \/ ~ P.
adamc@230 543
adamc@230 544 Theorem uhoh : False.
adam@287 545 generalize classic not_classic; tauto.
adamc@230 546 Qed.
adamc@230 547
adamc@230 548 Theorem uhoh_again : 1 + 1 = 3.
adamc@230 549 destruct uhoh.
adamc@230 550 Qed.
adamc@230 551
adamc@230 552 Reset not_classic.
adamc@230 553
adam@287 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.
adamc@230 555
adamc@230 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.
adamc@230 557
adamc@231 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.
adamc@230 559
adamc@230 560 Because the proper use of axioms is so precarious, there are helpful commands for determining which axioms a theorem relies on. *)
adamc@230 561
adamc@230 562 Theorem t1 : forall P : Prop, P -> ~ ~ P.
adamc@230 563 tauto.
adamc@230 564 Qed.
adamc@230 565
adamc@230 566 Print Assumptions t1.
adamc@230 567 (** %\vspace{-.15in}% [[
adamc@230 568 Closed under the global context
adam@302 569 ]]
adam@302 570 *)
adamc@230 571
adamc@230 572 Theorem t2 : forall P : Prop, ~ ~ P -> P.
adamc@230 573 (** [[
adamc@230 574 tauto.
adamc@230 575
adamc@230 576 Error: tauto failed.
adamc@230 577
adam@302 578 ]]
adam@302 579 *)
adamc@230 580
adamc@230 581 intro P; destruct (classic P); tauto.
adamc@230 582 Qed.
adamc@230 583
adamc@230 584 Print Assumptions t2.
adamc@230 585 (** %\vspace{-.15in}% [[
adamc@230 586 Axioms:
adamc@230 587 classic : forall P : Prop, P \/ ~ P
adamc@230 588
adamc@230 589 ]]
adamc@230 590
adamc@231 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. *)
adamc@230 592
adam@287 593 Theorem nat_eq_dec : forall n m : nat, n = m \/ n <> m.
adamc@230 594 induction n; destruct m; intuition; generalize (IHn m); intuition.
adamc@230 595 Qed.
adamc@230 596
adamc@230 597 Theorem t2' : forall n m : nat, ~ ~ (n = m) -> n = m.
adam@287 598 intros n m; destruct (nat_eq_dec n m); tauto.
adamc@230 599 Qed.
adamc@230 600
adamc@230 601 Print Assumptions t2'.
adamc@230 602 (** %\vspace{-.15in}% [[
adamc@230 603 Closed under the global context
adamc@230 604 ]]
adamc@230 605
adamc@230 606 %\bigskip%
adamc@230 607
adamc@230 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. *)
adamc@230 609
adamc@230 610 Require Import ProofIrrelevance.
adamc@230 611 Print proof_irrelevance.
adamc@230 612 (** %\vspace{-.15in}% [[
adamc@230 613 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ]
adamc@230 614
adamc@230 615 ]]
adamc@230 616
adamc@231 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. *)
adamc@230 618
adamc@230 619 (* begin hide *)
adamc@230 620 Lemma zgtz : 0 > 0 -> False.
adamc@230 621 crush.
adamc@230 622 Qed.
adamc@230 623 (* end hide *)
adamc@230 624
adamc@230 625 Definition pred_strong1 (n : nat) : n > 0 -> nat :=
adamc@230 626 match n with
adamc@230 627 | O => fun pf : 0 > 0 => match zgtz pf with end
adamc@230 628 | S n' => fun _ => n'
adamc@230 629 end.
adamc@230 630
adamc@230 631 (** 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 632
adamc@230 633 Theorem pred_strong1_irrel : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
adamc@230 634 destruct n; crush.
adamc@230 635 Qed.
adamc@230 636
adamc@230 637 (** 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 638
adamc@230 639 Theorem pred_strong1_irrel' : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
adamc@230 640 intros; f_equal; apply proof_irrelevance.
adamc@230 641 Qed.
adamc@230 642
adamc@230 643
adamc@230 644 (** %\bigskip%
adamc@230 645
adamc@230 646 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 647
adamc@230 648 Require Import Eqdep.
adamc@230 649 Import Eq_rect_eq.
adamc@230 650 Print eq_rect_eq.
adamc@230 651 (** %\vspace{-.15in}% [[
adamc@230 652 *** [ eq_rect_eq :
adamc@230 653 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@230 654 x = eq_rect p Q x p h ]
adamc@230 655
adamc@230 656 ]]
adamc@230 657
adamc@230 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. *)
adamc@230 659
adamc@230 660 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = refl_equal x.
adamc@230 661 intros; replace pf with (eq_rect x (eq x) (refl_equal x) x pf); [
adamc@230 662 symmetry; apply eq_rect_eq
adamc@230 663 | exact (match pf as pf' return match pf' in _ = y return x = y with
adamc@230 664 | refl_equal => refl_equal x
adamc@230 665 end = pf' with
adamc@230 666 | refl_equal => refl_equal _
adamc@230 667 end) ].
adamc@230 668 Qed.
adamc@230 669
adamc@230 670 Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2.
adamc@230 671 intros; generalize pf1 pf2; subst; intros;
adamc@230 672 match goal with
adamc@230 673 | [ |- ?pf1 = ?pf2 ] => rewrite (UIP_refl pf1); rewrite (UIP_refl pf2); reflexivity
adamc@230 674 end.
adamc@230 675 Qed.
adamc@230 676
adamc@231 677 (** 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 678
adamc@230 679 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 680
adamc@230 681 %\bigskip%
adamc@230 682
adamc@230 683 There are two more basic axioms that are often assumed, to avoid complications that do not arise in set theory. *)
adamc@230 684
adamc@230 685 Require Import FunctionalExtensionality.
adamc@230 686 Print functional_extensionality_dep.
adamc@230 687 (** %\vspace{-.15in}% [[
adamc@230 688 *** [ functional_extensionality_dep :
adamc@230 689 forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
adamc@230 690 (forall x : A, f x = g x) -> f = g ]
adamc@230 691
adamc@230 692 ]]
adamc@230 693
adamc@230 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.
adamc@230 695
adamc@230 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. *)
adamc@230 697
adamc@230 698 Corollary predicate_extensionality : forall (A : Type) (B : A -> Prop) (f g : forall x : A, B x),
adamc@230 699 (forall x : A, f x = g x) -> f = g.
adamc@230 700 intros; apply functional_extensionality_dep; assumption.
adamc@230 701 Qed.
adamc@230 702
adamc@230 703
adamc@230 704 (** ** Axioms of Choice *)
adamc@230 705
adamc@230 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.
adamc@230 707
adamc@230 708 First, it is possible to implement a choice operator %\textit{%#<i>#without#</i>#%}% axioms in some potentially surprising cases. *)
adamc@230 709
adamc@230 710 Require Import ConstructiveEpsilon.
adamc@230 711 Check constructive_definite_description.
adamc@230 712 (** %\vspace{-.15in}% [[
adamc@230 713 constructive_definite_description
adamc@230 714 : forall (A : Set) (f : A -> nat) (g : nat -> A),
adamc@230 715 (forall x : A, g (f x) = x) ->
adamc@230 716 forall P : A -> Prop,
adamc@230 717 (forall x : A, {P x} + {~ P x}) ->
adamc@230 718 (exists! x : A, P x) -> {x : A | P x}
adam@302 719 ]]
adam@302 720 *)
adamc@230 721
adamc@230 722 Print Assumptions constructive_definite_description.
adamc@230 723 (** %\vspace{-.15in}% [[
adamc@230 724 Closed under the global context
adamc@230 725
adamc@230 726 ]]
adamc@230 727
adamc@231 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.
adamc@230 729
adamc@230 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. *)
adamc@230 731
adamc@230 732 Require Import ClassicalUniqueChoice.
adamc@230 733 Check dependent_unique_choice.
adamc@230 734 (** %\vspace{-.15in}% [[
adamc@230 735 dependent_unique_choice
adamc@230 736 : forall (A : Type) (B : A -> Type) (R : forall x : A, B x -> Prop),
adamc@230 737 (forall x : A, exists! y : B x, R x y) ->
adamc@230 738 exists f : forall x : A, B x, forall x : A, R x (f x)
adamc@230 739
adamc@230 740 ]]
adamc@230 741
adamc@230 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. *)
adamc@230 743
adamc@230 744 Require Import ClassicalChoice.
adamc@230 745 Check choice.
adamc@230 746 (** %\vspace{-.15in}% [[
adamc@230 747 choice
adamc@230 748 : forall (A B : Type) (R : A -> B -> Prop),
adamc@230 749 (forall x : A, exists y : B, R x y) ->
adamc@230 750 exists f : A -> B, forall x : A, R x (f x)
adamc@230 751
adamc@230 752 ]]
adamc@230 753
adamc@230 754 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 755
adamc@230 756 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 757
adamc@230 758 Definition choice_Set (A B : Type) (R : A -> B -> Prop) (H : forall x : A, {y : B | R x y})
adamc@230 759 : {f : A -> B | forall x : A, R x (f x)} :=
adamc@230 760 exist (fun f => forall x : A, R x (f x))
adamc@230 761 (fun x => proj1_sig (H x)) (fun x => proj2_sig (H x)).
adamc@230 762
adam@287 763 (** 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 764
adam@287 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.
adamc@230 766
adamc@230 767 %\bigskip%
adamc@230 768
adamc@230 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].
adamc@230 770
adamc@230 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. *)
adamc@230 772
adamc@230 773 (** ** Axioms and Computation *)
adamc@230 774
adamc@230 775 (** 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 776
adamc@230 777 Definition cast (x y : Set) (pf : x = y) (v : x) : y :=
adamc@230 778 match pf with
adamc@230 779 | refl_equal => v
adamc@230 780 end.
adamc@230 781
adamc@230 782 (** Computation over programs that use [cast] can proceed smoothly. *)
adamc@230 783
adamc@230 784 Eval compute in (cast (refl_equal (nat -> nat)) (fun n => S n)) 12.
adamc@230 785 (** [[
adamc@230 786 = 13
adamc@230 787 : nat
adam@302 788 ]]
adam@302 789 *)
adamc@230 790
adamc@230 791 (** Things do not go as smoothly when we use [cast] with proofs that rely on axioms. *)
adamc@230 792
adamc@230 793 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
adamc@230 794 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
adamc@230 795 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
adamc@230 796 Qed.
adamc@230 797
adamc@230 798 Eval compute in (cast t3 (fun _ => First)) 12.
adamc@230 799 (** [[
adamc@230 800 = match t3 in (_ = P) return P with
adamc@230 801 | refl_equal => fun n : nat => First
adamc@230 802 end 12
adamc@230 803 : fin (12 + 1)
adamc@230 804
adamc@230 805 ]]
adamc@230 806
adamc@230 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. *)
adamc@230 808
adamc@230 809 Reset t3.
adamc@230 810
adamc@230 811 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
adamc@230 812 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
adamc@230 813 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
adamc@230 814 Defined.
adamc@230 815
adamc@230 816 Eval compute in (cast t3 (fun _ => First)) 12.
adamc@230 817 (** [[
adamc@230 818 = match
adamc@230 819 match
adamc@230 820 match
adamc@230 821 functional_extensionality
adamc@230 822 ....
adamc@230 823
adamc@230 824 ]]
adamc@230 825
adamc@230 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.
adamc@230 827
adamc@230 828 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *)
adamc@230 829
adamc@230 830 Lemma plus1 : forall n, S n = n + 1.
adamc@230 831 induction n; simpl; intuition.
adamc@230 832 Defined.
adamc@230 833
adamc@230 834 Theorem t4 : forall n, fin (S n) = fin (n + 1).
adamc@230 835 intro; f_equal; apply plus1.
adamc@230 836 Defined.
adamc@230 837
adamc@230 838 Eval compute in cast (t4 13) First.
adamc@230 839 (** %\vspace{-.15in}% [[
adamc@230 840 = First
adamc@230 841 : fin (13 + 1)
adam@302 842 ]]
adam@302 843 *)