Mercurial > cpdt > repo

annotate src/Universes.v @ 344:7466ac31f162

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New section on avoiding axioms
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Oct 2011 14:56:46 -0400
parents be8c7aae20f4
children 518c8994a715
rev   line source
adam@343 1 (* Copyright (c) 2009-2011, 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 *)
adam@314 11 Require Import DepList CpdtTactics.
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
adam@343 19 (** Many traditional theorems can be proved in Coq without special knowledge of CIC, the logic behind the prover. A development just seems to be using a particular ASCII notation for standard formulas based on %\index{set theory}%set theory. Nonetheless, as we saw in Chapter 4, CIC differs from set theory in starting from fewer orthogonal primitives. It is possible to define the usual logical connectives as derived notions. The foundation of it all is a dependently typed functional programming language, based on dependent function types and inductive type families. By using the facilities of this language directly, we can accomplish some things much more easily than in mainstream math.
adamc@227 20
adam@343 21 %\index{Gallina}%Gallina, which adds features to the more theoretical CIC%~\cite{CIC}%, is the logic implemented in Coq. It has a relatively simple foundation that can be defined rigorously in a page or two of formal proof rules. Still, there are some important subtleties that have practical ramifications. This chapter focuses on those subtleties, avoiding formal metatheory in favor of example code. *)
adamc@227 22
adamc@227 23
adamc@227 24 (** * The [Type] Hierarchy *)
adamc@227 25
adam@343 26 (** %\index{type hierarchy}%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
adam@343 53 The type [Set] may be considered as the set of all sets, a concept that set theory handles in terms of %\index{class (in set theory)}\textit{%#<i>#classes#</i>#%}%. In Coq, this more general notion is [Type]. *)
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@343 62 Strangely enough, [Type] appears to be its own type. It is known that polymorphic languages with this property are inconsistent, via %\index{Girard's paradox}%Girard's paradox%~\cite{GirardsParadox}%. That is, using such a language to encode proofs is unwise, because it is possible to %``%#"#prove#"#%''% any proposition. What is really going on here?
adamc@227 63
adam@343 64 Let us repeat some of our queries after toggling a flag related to Coq's printing behavior.%\index{Vernacular commands!Set Printing Universes}% *)
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
adam@343 97 In the second query's output, we see that the occurrence of [Type] that we check is assigned a fresh %\index{universe variable}\textit{%#<i>#universe variable#</i>#%}% [Top.3]. The output type increments [Top.3] to move up a level in the universe hierarchy. As we write code that uses definitions whose types mention universe variables, unification may refine the values of those variables. Luckily, the user rarely has to worry about the details.
adamc@227 98
adam@343 99 Another crucial concept in CIC is %\index{predicativity}\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.
adam@343 134 ]]
adamc@227 135
adam@343 136 <<
adamc@227 137 Error: Illegal application (Type Error):
adamc@227 138 ...
adam@343 139 The 1st term has type "Type (* (Top.15)+1 *)" which should be coercible to "Set".
adam@343 140 >>
adamc@227 141
adam@343 142 The parameter [T] of [id] must be instantiated with a [Set]. The type [nat] is a [Set], but [Set] is not. We can try fixing the problem by generalizing our definition of [id]. *)
adamc@227 143
adamc@227 144 Reset id.
adamc@227 145 Definition id (T : Type) (x : T) : T := x.
adamc@227 146 Check id 0.
adamc@227 147 (** %\vspace{-.15in}% [[
adamc@227 148 id 0
adamc@227 149 : nat
adam@302 150 ]]
adam@302 151 *)
adamc@227 152
adamc@227 153 Check id Set.
adamc@227 154 (** %\vspace{-.15in}% [[
adamc@227 155 id Set
adamc@227 156 : Type $ Top.17 ^
adam@302 157 ]]
adam@302 158 *)
adamc@227 159
adamc@227 160 Check id Type.
adamc@227 161 (** %\vspace{-.15in}% [[
adamc@227 162 id Type $ Top.18 ^
adamc@227 163 : Type $ Top.19 ^
adam@302 164 ]]
adam@302 165 *)
adamc@227 166
adamc@227 167 (** So far so good. As we apply [id] to different [T] values, the inferred index for [T]'s [Type] occurrence automatically moves higher up the type hierarchy.
adamc@227 168 [[
adamc@227 169 Check id id.
adam@343 170 ]]
adamc@227 171
adam@343 172 <<
adamc@227 173 Error: Universe inconsistency (cannot enforce Top.16 < Top.16).
adam@343 174 >>
adamc@227 175
adam@343 176 %\index{universe inconsistency}%This error message reminds us that the universe variable for [T] still exists, even though it is usually hidden. To apply [id] to itself, that variable would need to be less than itself in the type hierarchy. Universe inconsistency error messages announce cases like this one where a term could only type-check by violating an implied constraint over universe variables. Such errors demonstrate that [Type] is %\textit{%#<i>#predicative#</i>#%}%, where this word has a CIC meaning closely related to its usual mathematical meaning. A predicative system enforces the constraint that, for any object of quantified type, none of those quantifiers may ever be instantiated with the object itself. %\index{impredicativity}%Impredicativity is associated with popular paradoxes in set theory, involving inconsistent constructions like %``%#"#the set of all sets that do not contain themselves#"#%''% (%\index{Russell's paradox}%Russell's paradox). Similar paradoxes would result from uncontrolled impredicativity in Coq. *)
adamc@227 177
adamc@227 178
adamc@227 179 (** ** Inductive Definitions *)
adamc@227 180
adamc@227 181 (** Predicativity restrictions also apply to inductive definitions. As an example, let us consider a type of expression trees that allows injection of any native Coq value. The idea is that an [exp T] stands for a reflected expression of type [T].
adamc@227 182
adamc@227 183 [[
adamc@227 184 Inductive exp : Set -> Set :=
adamc@227 185 | Const : forall T : Set, T -> exp T
adamc@227 186 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 187 | Eq : forall T, exp T -> exp T -> exp bool.
adam@343 188 ]]
adamc@227 189
adam@343 190 <<
adamc@227 191 Error: Large non-propositional inductive types must be in Type.
adam@343 192 >>
adamc@227 193
adam@343 194 This definition is %\index{large inductive types}\textit{%#<i>#large#</i>#%}% in the sense that at least one of its constructors takes an argument whose type has type [Type]. Coq would be inconsistent if we allowed definitions like this one in their full generality. Instead, we must change [exp] to live in [Type]. We will go even further and move [exp]'s index to [Type] as well. *)
adamc@227 195
adamc@227 196 Inductive exp : Type -> Type :=
adamc@227 197 | Const : forall T, T -> exp T
adamc@227 198 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 199 | Eq : forall T, exp T -> exp T -> exp bool.
adamc@227 200
adamc@228 201 (** 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 202
adamc@228 203 Our new definition is accepted. We can build some sample expressions. *)
adamc@227 204
adamc@227 205 Check Const 0.
adamc@227 206 (** %\vspace{-.15in}% [[
adamc@227 207 Const 0
adamc@227 208 : exp nat
adam@302 209 ]]
adam@302 210 *)
adamc@227 211
adamc@227 212 Check Pair (Const 0) (Const tt).
adamc@227 213 (** %\vspace{-.15in}% [[
adamc@227 214 Pair (Const 0) (Const tt)
adamc@227 215 : exp (nat * unit)
adam@302 216 ]]
adam@302 217 *)
adamc@227 218
adamc@227 219 Check Eq (Const Set) (Const Type).
adamc@227 220 (** %\vspace{-.15in}% [[
adamc@228 221 Eq (Const Set) (Const Type $ Top.59 ^ )
adamc@227 222 : exp bool
adamc@227 223
adamc@227 224 ]]
adamc@227 225
adamc@227 226 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall.
adamc@227 227
adamc@227 228 [[
adamc@227 229 Check Const (Const O).
adam@343 230 ]]
adamc@227 231
adam@343 232 <<
adamc@227 233 Error: Universe inconsistency (cannot enforce Top.42 < Top.42).
adam@343 234 >>
adamc@227 235
adamc@227 236 We are unable to instantiate the parameter [T] of [Const] with an [exp] type. To see why, it is helpful to print the annotated version of [exp]'s inductive definition. *)
adamc@227 237
adamc@227 238 Print exp.
adamc@227 239 (** %\vspace{-.15in}% [[
adamc@227 240 Inductive exp
adamc@227 241 : Type $ Top.8 ^ ->
adamc@227 242 Type
adamc@227 243 $ max(0, (Top.11)+1, (Top.14)+1, (Top.15)+1, (Top.19)+1) ^ :=
adamc@227 244 Const : forall T : Type $ Top.11 ^ , T -> exp T
adamc@227 245 | Pair : forall (T1 : Type $ Top.14 ^ ) (T2 : Type $ Top.15 ^ ),
adamc@227 246 exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 247 | Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool
adamc@227 248
adamc@227 249 ]]
adamc@227 250
adamc@227 251 We see that the index type of [exp] has been assigned to universe level [Top.8]. In addition, each of the four occurrences of [Type] in the types of the constructors gets its own universe variable. Each of these variables appears explicitly in the type of [exp]. In particular, any type [exp T] lives at a universe level found by incrementing by one the maximum of the four argument variables. A consequence of this is that [exp] %\textit{%#<i>#must#</i>#%}% live at a higher universe level than any type which may be passed to one of its constructors. This consequence led to the universe inconsistency.
adamc@227 252
adam@343 253 Strangely, the universe variable [Top.8] only appears in one place. Is there no restriction imposed on which types are valid arguments to [exp]? In fact, there is a restriction, but it only appears in a global set of universe constraints that are maintained %``%#"#off to the side,#"#%''% not appearing explicitly in types. We can print the current database.%\index{Vernacular commands!Print Universes}% *)
adamc@227 254
adamc@227 255 Print Universes.
adamc@227 256 (** %\vspace{-.15in}% [[
adamc@227 257 Top.19 < Top.9 <= Top.8
adamc@227 258 Top.15 < Top.9 <= Top.8 <= Coq.Init.Datatypes.38
adamc@227 259 Top.14 < Top.9 <= Top.8 <= Coq.Init.Datatypes.37
adamc@227 260 Top.11 < Top.9 <= Top.8
adamc@227 261
adamc@227 262 ]]
adamc@227 263
adam@343 264 The command outputs many more constraints, but we have collected only those that mention [Top] variables. We see one constraint for each universe variable associated with a constructor argument from [exp]'s definition. Universe variable [Top.19] is the type argument to [Eq]. The constraint for [Top.19] effectively says that [Top.19] must be less than [Top.8], the universe of [exp]'s indices; an intermediate variable [Top.9] appears as an artifact of the way the constraint was generated.
adamc@227 265
adamc@227 266 The next constraint, for [Top.15], is more complicated. This is the universe of the second argument to the [Pair] constructor. Not only must [Top.15] be less than [Top.8], but it also comes out that [Top.8] must be less than [Coq.Init.Datatypes.38]. What is this new universe variable? It is from the definition of the [prod] inductive family, to which types of the form [A * B] are desugared. *)
adamc@227 267
adamc@227 268 Print prod.
adamc@227 269 (** %\vspace{-.15in}% [[
adamc@227 270 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ )
adamc@227 271 (B : Type $ Coq.Init.Datatypes.38 ^ )
adamc@227 272 : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ :=
adamc@227 273 pair : A -> B -> A * B
adamc@227 274
adamc@227 275 ]]
adamc@227 276
adamc@227 277 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 278
adamc@227 279 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 280
adamc@227 281 %\medskip%
adamc@227 282
adamc@227 283 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 284
adamc@231 285 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 286
adamc@227 287 Check (nat, (Type, Set)).
adamc@227 288 (** %\vspace{-.15in}% [[
adamc@227 289 (nat, (Type $ Top.44 ^ , Set))
adamc@227 290 : Set * (Type $ Top.45 ^ * Type $ Top.46 ^ )
adamc@227 291 ]]
adamc@227 292
adamc@227 293 The same cannot be done with a counterpart to [prod] that does not use parameters. *)
adamc@227 294
adamc@227 295 Inductive prod' : Type -> Type -> Type :=
adamc@227 296 | pair' : forall A B : Type, A -> B -> prod' A B.
adamc@227 297 (** [[
adamc@227 298 Check (pair' nat (pair' Type Set)).
adam@343 299 ]]
adamc@227 300
adam@343 301 <<
adamc@227 302 Error: Universe inconsistency (cannot enforce Top.51 < Top.51).
adam@343 303 >>
adamc@227 304
adamc@233 305 The key benefit parameters bring us is the ability to avoid quantifying over types in the types of constructors. Such quantification induces less-than constraints, while parameters only introduce less-than-or-equal-to constraints.
adamc@233 306
adam@343 307 Coq includes one more (potentially confusing) feature related to parameters. While Gallina does not support real %\index{universe polymorphism}%universe polymorphism, there is a convenience facility that mimics universe polymorphism in some cases. We can illustrate what this means with a simple example. *)
adamc@233 308
adamc@233 309 Inductive foo (A : Type) : Type :=
adamc@233 310 | Foo : A -> foo A.
adamc@229 311
adamc@229 312 (* begin hide *)
adamc@229 313 Unset Printing Universes.
adamc@229 314 (* end hide *)
adamc@229 315
adamc@233 316 Check foo nat.
adamc@233 317 (** %\vspace{-.15in}% [[
adamc@233 318 foo nat
adamc@233 319 : Set
adam@302 320 ]]
adam@302 321 *)
adamc@233 322
adamc@233 323 Check foo Set.
adamc@233 324 (** %\vspace{-.15in}% [[
adamc@233 325 foo Set
adamc@233 326 : Type
adam@302 327 ]]
adam@302 328 *)
adamc@233 329
adamc@233 330 Check foo True.
adamc@233 331 (** %\vspace{-.15in}% [[
adamc@233 332 foo True
adamc@233 333 : Prop
adamc@233 334
adamc@233 335 ]]
adamc@233 336
adam@287 337 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 338
adamc@233 339 Imitation polymorphism can be confusing in some contexts. For instance, it is what is responsible for this weird behavior. *)
adamc@233 340
adamc@233 341 Inductive bar : Type := Bar : bar.
adamc@233 342
adamc@233 343 Check bar.
adamc@233 344 (** %\vspace{-.15in}% [[
adamc@233 345 bar
adamc@233 346 : Prop
adamc@233 347 ]]
adamc@233 348
adamc@233 349 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *)
adamc@233 350
adamc@229 351
adamc@229 352 (** * The [Prop] Universe *)
adamc@229 353
adam@287 354 (** 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 355
adamc@229 356 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 357
adamc@229 358 Print sig.
adamc@229 359 (** %\vspace{-.15in}% [[
adamc@229 360 Inductive sig (A : Type) (P : A -> Prop) : Type :=
adamc@229 361 exist : forall x : A, P x -> sig P
adam@302 362 ]]
adam@302 363 *)
adamc@229 364
adamc@229 365 Print ex.
adamc@229 366 (** %\vspace{-.15in}% [[
adamc@229 367 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
adamc@229 368 ex_intro : forall x : A, P x -> ex P
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 Definition projE A (P : A -> Prop) (x : ex P) : A :=
adamc@229 381 match x with
adamc@229 382 | ex_intro v _ => v
adamc@229 383 end.
adam@343 384 ]]
adamc@229 385
adam@343 386 <<
adamc@229 387 Error:
adamc@229 388 Incorrect elimination of "x" in the inductive type "ex":
adamc@229 389 the return type has sort "Type" while it should be "Prop".
adamc@229 390 Elimination of an inductive object of sort Prop
adamc@229 391 is not allowed on a predicate in sort Type
adamc@229 392 because proofs can be eliminated only to build proofs.
adam@343 393 >>
adamc@229 394
adam@343 395 In formal Coq parlance, %\index{elimination}``%#"#elimination#"#%''% means %``%#"#pattern-matching.#"#%''% The typing rules of Gallina forbid us from pattern-matching on a discriminee whose type belongs to [Prop], whenever the result type of the [match] has a type besides [Prop]. This is a sort of %``%#"#information flow#"#%''% policy, where the type system ensures that the details of proofs can never have any effect on parts of a development that are not also marked as proofs.
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
adam@343 399 Recall that %\index{program extraction}%extraction is Coq's facility for translating Coq developments into programs in general-purpose programming languages like OCaml. Extraction %\textit{%#<i>#erases#</i>#%}% proofs and leaves programs intact. A simple example with [sig] and [ex] demonstrates the distinction. *)
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
adam@343 429 Extraction is very helpful as an optimization over programs that contain proofs. In languages like Haskell, advanced features make it possible to program with proofs, as a way of convincing the type checker to accept particular definitions. Unfortunately, when proofs are encoded as values in GADTs%~\cite{GADT}%, these proofs exist at runtime and consume resources. In contrast, with Coq, as long as all proofs are kept within [Prop], extraction is guaranteed to erase them.
adamc@229 430
adam@343 431 Many fans of the %\index{Curry-Howard correspondence}%Curry-Howard correspondence support the idea of %\textit{%#<i>#extracting programs from proofs#</i>#%}%. In reality, few users of Coq and related tools do any such thing. Instead, extraction is better thought of as an optimization that reduces the runtime costs of expressive typing.
adamc@229 432
adamc@229 433 %\medskip%
adamc@229 434
adam@343 435 We have seen two of the differences between proofs and programs: proofs are subject to an elimination restriction and are elided by extraction. The remaining difference is that [Prop] is %\index{impredicativity}\textit{%#<i>#impredicative#</i>#%}%, as this example shows. *)
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
adam@343 510 (** Stating equality facts about proofs may seem baroque, but we have already seen its utility in the chapter on reasoning about equality proofs. *)
adam@343 511
adamc@230 512
adamc@230 513 (** * Axioms *)
adamc@230 514
adam@343 515 (** While the specific logic Gallina is hardcoded into Coq's implementation, it is possible to add certain logical rules in a controlled way. In other words, Coq may be used to reason about many different refinements of Gallina where strictly more theorems are provable. We achieve this by asserting %\index{axioms}\textit{%#<i>#axioms#</i>#%}% without proof.
adamc@230 516
adamc@230 517 We will motivate the idea by touring through some standard axioms, as enumerated in Coq's online FAQ. I will add additional commentary as appropriate. *)
adamc@230 518
adamc@230 519 (** ** The Basics *)
adamc@230 520
adam@343 521 (** One simple example of a useful axiom is the %\index{law of the excluded middle}%law of the excluded middle. *)
adamc@230 522
adamc@230 523 Require Import Classical_Prop.
adamc@230 524 Print classic.
adamc@230 525 (** %\vspace{-.15in}% [[
adamc@230 526 *** [ classic : forall P : Prop, P \/ ~ P ]
adamc@230 527 ]]
adamc@230 528
adam@343 529 In the implementation of module [Classical_Prop], this axiom was defined with the command%\index{Vernacular commands!Axiom}% *)
adamc@230 530
adamc@230 531 Axiom classic : forall P : Prop, P \/ ~ P.
adamc@230 532
adam@343 533 (** An [Axiom] may be declared with any type, in any of the universes. There is a synonym %\index{Vernacular commands!Parameter}%[Parameter] for [Axiom], and that synonym is often clearer for assertions not of type [Prop]. For instance, we can assert the existence of objects with certain properties. *)
adamc@230 534
adamc@230 535 Parameter n : nat.
adamc@230 536 Axiom positive : n > 0.
adamc@230 537 Reset n.
adamc@230 538
adam@287 539 (** This kind of %``%#"#axiomatic presentation#"#%''% of a theory is very common outside of higher-order logic. However, in Coq, it is almost always preferable to stick to defining your objects, functions, and predicates via inductive definitions and functional programming.
adamc@230 540
adam@343 541 In general, there is a significant burden associated with any use of axioms. It is easy to assert a set of axioms that together is %\index{inconsistent axioms}\textit{%#<i>#inconsistent#</i>#%}%. That is, a set of axioms may imply [False], which allows any theorem to proved, which defeats the purpose of a proof assistant. For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *)
adamc@230 542
adam@287 543 Axiom not_classic : ~ forall P : Prop, P \/ ~ P.
adamc@230 544
adamc@230 545 Theorem uhoh : False.
adam@287 546 generalize classic not_classic; tauto.
adamc@230 547 Qed.
adamc@230 548
adamc@230 549 Theorem uhoh_again : 1 + 1 = 3.
adamc@230 550 destruct uhoh.
adamc@230 551 Qed.
adamc@230 552
adamc@230 553 Reset not_classic.
adamc@230 554
adam@343 555 (** On the subject of the law of the excluded middle itself, this axiom is usually quite harmless, and many practical Coq developments assume it. It has been proved metatheoretically to be consistent with CIC. Here, %``%#"#proved metatheoretically#"#%''% means that someone proved on paper that excluded middle holds in a %\textit{%#<i>#model#</i>#%}% of CIC in set theory%~\cite{SetsInTypes}%. All of the other axioms that we will survey in this section hold in the same model, so they are all consistent together.
adamc@230 556
adam@343 557 Recall that Coq implements %\index{constructive logic}\textit{%#<i>#constructive#</i>#%}% logic by default, where excluded middle is not provable. Proofs in constructive logic can be thought of as programs. A [forall] quantifier denotes a dependent function type, and a disjunction denotes a variant type. In such a setting, excluded middle could be interpreted as a decision procedure for arbitrary propositions, which computability theory tells us cannot exist. Thus, constructive logic with excluded middle can no longer be associated with our usual notion of programming.
adamc@230 558
adamc@231 559 Given all this, why is it all right to assert excluded middle as an axiom? The intuitive justification is that the elimination restriction for [Prop] prevents us from treating proofs as programs. An excluded middle axiom that quantified over [Set] instead of [Prop] %\textit{%#<i>#would#</i>#%}% be problematic. If a development used that axiom, we would not be able to extract the code to OCaml (soundly) without implementing a genuine universal decision procedure. In contrast, values whose types belong to [Prop] are always erased by extraction, so we sidestep the axiom's algorithmic consequences.
adamc@230 560
adam@343 561 Because the proper use of axioms is so precarious, there are helpful commands for determining which axioms a theorem relies on.%\index{Vernacular commands!Print Assumptions}% *)
adamc@230 562
adamc@230 563 Theorem t1 : forall P : Prop, P -> ~ ~ P.
adamc@230 564 tauto.
adamc@230 565 Qed.
adamc@230 566
adamc@230 567 Print Assumptions t1.
adam@343 568 (** <<
adamc@230 569 Closed under the global context
adam@343 570 >>
adam@302 571 *)
adamc@230 572
adamc@230 573 Theorem t2 : forall P : Prop, ~ ~ P -> P.
adamc@230 574 (** [[
adamc@230 575 tauto.
adam@343 576 ]]
adam@343 577 <<
adamc@230 578 Error: tauto failed.
adam@343 579 >>
adam@302 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@231 590 It is possible to avoid this dependence in some specific cases, where excluded middle %\textit{%#<i>#is#</i>#%}% provable, for decidable families of propositions. *)
adamc@230 591
adam@287 592 Theorem nat_eq_dec : forall n m : nat, n = m \/ n <> m.
adamc@230 593 induction n; destruct m; intuition; generalize (IHn m); intuition.
adamc@230 594 Qed.
adamc@230 595
adamc@230 596 Theorem t2' : forall n m : nat, ~ ~ (n = m) -> n = m.
adam@287 597 intros n m; destruct (nat_eq_dec n m); tauto.
adamc@230 598 Qed.
adamc@230 599
adamc@230 600 Print Assumptions t2'.
adam@343 601 (** <<
adamc@230 602 Closed under the global context
adam@343 603 >>
adamc@230 604
adamc@230 605 %\bigskip%
adamc@230 606
adam@343 607 Mainstream mathematical practice assumes excluded middle, so it can be useful to have it available in Coq developments, though it is also nice to know that a theorem is proved in a simpler formal system than classical logic. There is a similar story for %\index{proof irrelevance}\textit{%#<i>#proof irrelevance#</i>#%}%, which simplifies proof issues that would not even arise in mainstream math. *)
adamc@230 608
adamc@230 609 Require Import ProofIrrelevance.
adamc@230 610 Print proof_irrelevance.
adamc@230 611 (** %\vspace{-.15in}% [[
adamc@230 612 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ]
adamc@230 613 ]]
adamc@230 614
adamc@231 615 This axiom asserts that any two proofs of the same proposition are equal. If we replaced [p1 = p2] by [p1 <-> p2], then the statement would be provable. However, equality is a stronger notion than logical equivalence. Recall this example function from Chapter 6. *)
adamc@230 616
adamc@230 617 (* begin hide *)
adamc@230 618 Lemma zgtz : 0 > 0 -> False.
adamc@230 619 crush.
adamc@230 620 Qed.
adamc@230 621 (* end hide *)
adamc@230 622
adamc@230 623 Definition pred_strong1 (n : nat) : n > 0 -> nat :=
adamc@230 624 match n with
adamc@230 625 | O => fun pf : 0 > 0 => match zgtz pf with end
adamc@230 626 | S n' => fun _ => n'
adamc@230 627 end.
adamc@230 628
adam@343 629 (** 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 630
adamc@230 631 Theorem pred_strong1_irrel : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
adamc@230 632 destruct n; crush.
adamc@230 633 Qed.
adamc@230 634
adamc@230 635 (** 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 636
adamc@230 637 Theorem pred_strong1_irrel' : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
adamc@230 638 intros; f_equal; apply proof_irrelevance.
adamc@230 639 Qed.
adamc@230 640
adamc@230 641
adamc@230 642 (** %\bigskip%
adamc@230 643
adamc@230 644 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 645
adamc@230 646 Require Import Eqdep.
adamc@230 647 Import Eq_rect_eq.
adamc@230 648 Print eq_rect_eq.
adamc@230 649 (** %\vspace{-.15in}% [[
adamc@230 650 *** [ eq_rect_eq :
adamc@230 651 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@230 652 x = eq_rect p Q x p h ]
adamc@230 653 ]]
adamc@230 654
adam@343 655 This axiom says that it is permissible to simplify pattern matches over proofs of equalities like [e = e]. The axiom is logically equivalent to some simpler corollaries. In the theorem names, %``%#"#UIP#"#%''% stands for %\index{unicity of identity proofs}``%#"#unicity of identity proofs#"#%''%, where %``%#"#identity#"#%''% is a synonym for %``%#"#equality.#"#%''% *)
adamc@230 656
adamc@230 657 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = refl_equal x.
adamc@230 658 intros; replace pf with (eq_rect x (eq x) (refl_equal x) x pf); [
adamc@230 659 symmetry; apply eq_rect_eq
adamc@230 660 | exact (match pf as pf' return match pf' in _ = y return x = y with
adamc@230 661 | refl_equal => refl_equal x
adamc@230 662 end = pf' with
adamc@230 663 | refl_equal => refl_equal _
adamc@230 664 end) ].
adamc@230 665 Qed.
adamc@230 666
adamc@230 667 Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2.
adamc@230 668 intros; generalize pf1 pf2; subst; intros;
adamc@230 669 match goal with
adamc@230 670 | [ |- ?pf1 = ?pf2 ] => rewrite (UIP_refl pf1); rewrite (UIP_refl pf2); reflexivity
adamc@230 671 end.
adamc@230 672 Qed.
adamc@230 673
adamc@231 674 (** 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 675
adamc@230 676 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 677
adamc@230 678 %\bigskip%
adamc@230 679
adamc@230 680 There are two more basic axioms that are often assumed, to avoid complications that do not arise in set theory. *)
adamc@230 681
adamc@230 682 Require Import FunctionalExtensionality.
adamc@230 683 Print functional_extensionality_dep.
adamc@230 684 (** %\vspace{-.15in}% [[
adamc@230 685 *** [ functional_extensionality_dep :
adamc@230 686 forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
adamc@230 687 (forall x : A, f x = g x) -> f = g ]
adamc@230 688
adamc@230 689 ]]
adamc@230 690
adamc@230 691 This axiom says that two functions are equal if they map equal inputs to equal outputs. Such facts are not provable in general in CIC, but it is consistent to assume that they are.
adamc@230 692
adam@343 693 A simple corollary shows that the same property applies to predicates. *)
adamc@230 694
adamc@230 695 Corollary predicate_extensionality : forall (A : Type) (B : A -> Prop) (f g : forall x : A, B x),
adamc@230 696 (forall x : A, f x = g x) -> f = g.
adamc@230 697 intros; apply functional_extensionality_dep; assumption.
adamc@230 698 Qed.
adamc@230 699
adam@343 700 (** In some cases, one might prefer to assert this corollary as the axiom, to restrict the consequences to proofs and not programs. *)
adam@343 701
adamc@230 702
adamc@230 703 (** ** Axioms of Choice *)
adamc@230 704
adam@343 705 (** Some Coq axioms are also points of contention in mainstream math. The most prominent example is the %\index{axiom of choice}%axiom of choice. In fact, there are multiple versions that we might consider, and, considered in isolation, none of these versions means quite what it means in classical set theory.
adamc@230 706
adamc@230 707 First, it is possible to implement a choice operator %\textit{%#<i>#without#</i>#%}% axioms in some potentially surprising cases. *)
adamc@230 708
adamc@230 709 Require Import ConstructiveEpsilon.
adamc@230 710 Check constructive_definite_description.
adamc@230 711 (** %\vspace{-.15in}% [[
adamc@230 712 constructive_definite_description
adamc@230 713 : forall (A : Set) (f : A -> nat) (g : nat -> A),
adamc@230 714 (forall x : A, g (f x) = x) ->
adamc@230 715 forall P : A -> Prop,
adamc@230 716 (forall x : A, {P x} + {~ P x}) ->
adamc@230 717 (exists! x : A, P x) -> {x : A | P x}
adam@302 718 ]]
adam@302 719 *)
adamc@230 720
adamc@230 721 Print Assumptions constructive_definite_description.
adam@343 722 (** <<
adamc@230 723 Closed under the global context
adam@343 724 >>
adamc@230 725
adamc@231 726 This function transforms a decidable predicate [P] into a function that produces an element satisfying [P] from a proof that such an element exists. The functions [f] and [g], in conjunction with an associated injectivity property, are used to express the idea that the set [A] is countable. Under these conditions, a simple brute force algorithm gets the job done: we just enumerate all elements of [A], stopping when we find one satisfying [P]. The existence proof, specified in terms of %\textit{%#<i>#unique#</i>#%}% existence [exists!], guarantees termination. The definition of this operator in Coq uses some interesting techniques, as seen in the implementation of the [ConstructiveEpsilon] module.
adamc@230 727
adamc@230 728 Countable choice is provable in set theory without appealing to the general axiom of choice. To support the more general principle in Coq, we must also add an axiom. Here is a functional version of the axiom of unique choice. *)
adamc@230 729
adamc@230 730 Require Import ClassicalUniqueChoice.
adamc@230 731 Check dependent_unique_choice.
adamc@230 732 (** %\vspace{-.15in}% [[
adamc@230 733 dependent_unique_choice
adamc@230 734 : forall (A : Type) (B : A -> Type) (R : forall x : A, B x -> Prop),
adamc@230 735 (forall x : A, exists! y : B x, R x y) ->
adam@343 736 exists f : forall x : A, B x,
adam@343 737 forall x : A, R x (f x)
adamc@230 738 ]]
adamc@230 739
adamc@230 740 This axiom lets us convert a relational specification [R] into a function implementing that specification. We need only prove that [R] is truly a function. An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs. We also simplify the statement of the theorem by considering only non-dependent function types. *)
adamc@230 741
adamc@230 742 Require Import ClassicalChoice.
adamc@230 743 Check choice.
adamc@230 744 (** %\vspace{-.15in}% [[
adamc@230 745 choice
adamc@230 746 : forall (A B : Type) (R : A -> B -> Prop),
adamc@230 747 (forall x : A, exists y : B, R x y) ->
adamc@230 748 exists f : A -> B, forall x : A, R x (f x)
adamc@230 749
adamc@230 750 ]]
adamc@230 751
adamc@230 752 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 753
adamc@230 754 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 755
adamc@230 756 Definition choice_Set (A B : Type) (R : A -> B -> Prop) (H : forall x : A, {y : B | R x y})
adamc@230 757 : {f : A -> B | forall x : A, R x (f x)} :=
adamc@230 758 exist (fun f => forall x : A, R x (f x))
adamc@230 759 (fun x => proj1_sig (H x)) (fun x => proj2_sig (H x)).
adamc@230 760
adam@287 761 (** 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 762
adam@287 763 However, when we combine an axiom of choice with the law of the excluded middle, the idea of %``%#"#choice#"#%''% becomes more interesting. Excluded middle gives us a highly non-computational way of constructing proofs, but it does not change the computational nature of programs. Thus, the axiom of choice is still giving us a way of translating between two different sorts of %``%#"#programs,#"#%''% but the input programs (which are proofs) may be written in a rich language that goes beyond normal computability. This truly is more than repackaging a function with a different type.
adamc@230 764
adamc@230 765 %\bigskip%
adamc@230 766
adam@343 767 The Coq tools support a command-line flag %\index{impredicative Set}\texttt{%#<tt>#-impredicative-set#</tt>#%}%, which modifies Gallina in a more fundamental way by making [Set] impredicative. A term like [forall T : Set, T] has type [Set], and inductive definitions in [Set] may have constructors that quantify over arguments of any types. To maintain consistency, an elimination restriction must be imposed, similarly to the restriction for [Prop]. The restriction only applies to large inductive types, where some constructor quantifies over a type of type [Type]. In such cases, a value in this inductive type may only be pattern-matched over to yield a result type whose type is [Set] or [Prop]. This contrasts with [Prop], where the restriction applies even to non-large inductive types, and where the result type may only have type [Prop].
adamc@230 768
adamc@230 769 In old versions of Coq, [Set] was impredicative by default. Later versions make [Set] predicative to avoid inconsistency with some classical axioms. In particular, one should watch out when using impredicative [Set] with axioms of choice. In combination with excluded middle or predicate extensionality, this can lead to inconsistency. Impredicative [Set] can be useful for modeling inherently impredicative mathematical concepts, but almost all Coq developments get by fine without it. *)
adamc@230 770
adamc@230 771 (** ** Axioms and Computation *)
adamc@230 772
adamc@230 773 (** 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 774
adamc@230 775 Definition cast (x y : Set) (pf : x = y) (v : x) : y :=
adamc@230 776 match pf with
adamc@230 777 | refl_equal => v
adamc@230 778 end.
adamc@230 779
adamc@230 780 (** Computation over programs that use [cast] can proceed smoothly. *)
adamc@230 781
adamc@230 782 Eval compute in (cast (refl_equal (nat -> nat)) (fun n => S n)) 12.
adam@343 783 (** %\vspace{-.15in}%[[
adamc@230 784 = 13
adamc@230 785 : nat
adam@302 786 ]]
adam@302 787 *)
adamc@230 788
adamc@230 789 (** Things do not go as smoothly when we use [cast] with proofs that rely on axioms. *)
adamc@230 790
adamc@230 791 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
adamc@230 792 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
adamc@230 793 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
adamc@230 794 Qed.
adamc@230 795
adamc@230 796 Eval compute in (cast t3 (fun _ => First)) 12.
adamc@230 797 (** [[
adamc@230 798 = match t3 in (_ = P) return P with
adamc@230 799 | refl_equal => fun n : nat => First
adamc@230 800 end 12
adamc@230 801 : fin (12 + 1)
adamc@230 802 ]]
adamc@230 803
adamc@230 804 Computation gets stuck in a pattern-match on the proof [t3]. The structure of [t3] is not known, so the match cannot proceed. It turns out a more basic problem leads to this particular situation. We ended the proof of [t3] with [Qed], so the definition of [t3] is not available to computation. That is easily fixed. *)
adamc@230 805
adamc@230 806 Reset t3.
adamc@230 807
adamc@230 808 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
adamc@230 809 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
adamc@230 810 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
adamc@230 811 Defined.
adamc@230 812
adamc@230 813 Eval compute in (cast t3 (fun _ => First)) 12.
adamc@230 814 (** [[
adamc@230 815 = match
adamc@230 816 match
adamc@230 817 match
adamc@230 818 functional_extensionality
adamc@230 819 ....
adamc@230 820 ]]
adamc@230 821
adamc@230 822 We elide most of the details. A very unwieldy tree of nested matches on equality proofs appears. This time evaluation really %\textit{%#<i>#is#</i>#%}% stuck on a use of an axiom.
adamc@230 823
adamc@230 824 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *)
adamc@230 825
adamc@230 826 Lemma plus1 : forall n, S n = n + 1.
adamc@230 827 induction n; simpl; intuition.
adamc@230 828 Defined.
adamc@230 829
adamc@230 830 Theorem t4 : forall n, fin (S n) = fin (n + 1).
adamc@230 831 intro; f_equal; apply plus1.
adamc@230 832 Defined.
adamc@230 833
adamc@230 834 Eval compute in cast (t4 13) First.
adamc@230 835 (** %\vspace{-.15in}% [[
adamc@230 836 = First
adamc@230 837 : fin (13 + 1)
adam@302 838 ]]
adam@343 839
adam@343 840 This simple computational reduction hides the use of a recursive function to produce a suitable [refl_equal] proof term. The recursion originates in our use of [induction] in [t4]'s proof. *)
adam@343 841
adam@344 842
adam@344 843 (** ** Methods for Avoiding Axioms *)
adam@344 844
adam@344 845 (** The last section demonstrated one reason to avoid axioms: they interfere with computational behavior of terms. A further reason is to reduce the philosophical commitment of a theorem. The more axioms one assumes, the harder it becomes to convince oneself that the formal system corresponds appropriately to one's intuitions. A refinement of this last point, in applications like %\index{proof-carrying code}%proof-carrying code%~\cite{PCC}% in computer security, has to do with minimizing the size of a %\index{trusted code base}\emph{%#<i>#trusted code base#</i>#%}%. To convince ourselves that a theorem is true, we must convince ourselves of the correctness of the program that checks the theorem. Axioms effectively become new source code for the checking program, increasing the effort required to perform a correctness audit.
adam@344 846
adam@344 847 An earlier section gave one example of avoiding an axiom. We proved that [pred_strong1] is agnostic to details of the proofs passed to it as arguments, by unfolding the definition of the function. A %``%#"#simpler#"#%''% proof keeps the function definition opaque and instead applies a proof irrelevance axiom. By accepting a more complex proof, we reduce our philosophical commitment and trusted base. (By the way, the less-than relation that the proofs in question here prove turns out to admit proof irrelevance as a theorem provable within normal Gallina!)
adam@344 848
adam@344 849 One dark secret of the [dep_destruct] tactic that we have used several times is reliance on an axiom. Consider this simple case analysis principle for [fin] values: *)
adam@344 850
adam@344 851 Theorem fin_cases : forall n (f : fin (S n)), f = First \/ exists f', f = Next f'.
adam@344 852 intros; dep_destruct f; eauto.
adam@344 853 Qed.
adam@344 854
adam@344 855 Print Assumptions fin_cases.
adam@344 856 (** %\vspace{-.15in}%[[
adam@344 857 Axioms:
adam@344 858 JMeq.JMeq_eq : forall (A : Type) (x y : A), JMeq.JMeq x y -> x = y
adam@344 859 ]]
adam@344 860
adam@344 861 The proof depends on the [JMeq_eq] axiom that we met in the chapter on equality proofs. However, a smarter tactic could have avoided an axiom dependence. Here is an alternate proof via a slightly strange looking lemma. *)
adam@344 862
adam@344 863 (* begin thide *)
adam@344 864 Lemma fin_cases_again' : forall n (f : fin n),
adam@344 865 match n return fin n -> Prop with
adam@344 866 | O => fun _ => False
adam@344 867 | S n' => fun f => f = First \/ exists f', f = Next f'
adam@344 868 end f.
adam@344 869 destruct f; eauto.
adam@344 870 Qed.
adam@344 871
adam@344 872 (** We apply a variant of the %\index{convoy pattern}%convoy pattern, which we are used to seeing in function implementations. Here, the pattern helps us state a lemma in a form where the argument to [fin] is a variable. Recall that, thanks to basic typing rules for pattern-matching, [destruct] will only work effectively on types whose non-parameter arguments are variables. The %\index{tactics!exact}%[exact] tactic, which takes as argument a literal proof term, now gives us an easy way of proving the original theorem. *)
adam@344 873
adam@344 874 Theorem fin_cases_again : forall n (f : fin (S n)), f = First \/ exists f', f = Next f'.
adam@344 875 intros; exact (fin_cases_again' f).
adam@344 876 Qed.
adam@344 877 (* end thide *)
adam@344 878
adam@344 879 Print Assumptions fin_cases_again.
adam@344 880 (** %\vspace{-.15in}%
adam@344 881 <<
adam@344 882 Closed under the global context
adam@344 883 >>
adam@344 884
adam@344 885 As another example, consider the following type of formulas in first-order logic. The intent of the type definition will not be important in what follows, but we give a quick intuition for the curious reader. Our formulas may include [forall] quantification over arbitrary [Type]s, and we index formulas by environments telling which variables are in scope and what their types are; such an environment is a [list Type]. A constructor [Inject] lets us include any Coq [Prop] as a formula, and [VarEq] and [Lift] can be used for variable references, in what is essentially the de Bruijn index convention. (Again, the detail in this paragraph is not important to understand the discussion that follows!) *)
adam@344 886
adam@344 887 Inductive formula : list Type -> Type :=
adam@344 888 | Inject : forall Ts, Prop -> formula Ts
adam@344 889 | VarEq : forall T Ts, T -> formula (T :: Ts)
adam@344 890 | Lift : forall T Ts, formula Ts -> formula (T :: Ts)
adam@344 891 | Forall : forall T Ts, formula (T :: Ts) -> formula Ts
adam@344 892 | And : forall Ts, formula Ts -> formula Ts -> formula Ts.
adam@344 893
adam@344 894 (** This example is based on my own experiences implementing variants of a program logic called XCAP%~\cite{XCAP}%, which also includes an inductive predicate for characterizing which formulas are provable. Here I include a pared-down version of such a predicate, with only two constructors, which is sufficient to illustrate certain tricky issues. *)
adam@344 895
adam@344 896 Inductive proof : formula nil -> Prop :=
adam@344 897 | PInject : forall (P : Prop), P -> proof (Inject nil P)
adam@344 898 | PAnd : forall p q, proof p -> proof q -> proof (And p q).
adam@344 899
adam@344 900 (** Let us prove a lemma showing that a %``%#"#[P /\ Q -> P]#"#%''% rule is derivable within the rules of [proof]. *)
adam@344 901
adam@344 902 Theorem proj1 : forall p q, proof (And p q) -> proof p.
adam@344 903 destruct 1.
adam@344 904 (** %\vspace{-.15in}%[[
adam@344 905 p : formula nil
adam@344 906 q : formula nil
adam@344 907 P : Prop
adam@344 908 H : P
adam@344 909 ============================
adam@344 910 proof p
adam@344 911 ]]
adam@344 912 *)
adam@344 913
adam@344 914 (** We are reminded that [induction] and [destruct] do not work effectively on types with non-variable arguments. The first subgoal, shown above, is clearly unprovable. (Consider the case where [p = Inject nil False].)
adam@344 915
adam@344 916 An application of the %\index{tactics!dependent destruction}%[dependent destruction] tactic (the basis for [dep_destruct]) solves the problem handily. We use a shorthand with the %\index{tactics!intros}%[intros] tactic that lets us use question marks for variable names that do not matter. *)
adam@344 917
adam@344 918 Restart.
adam@344 919 Require Import Program.
adam@344 920 intros ? ? H; dependent destruction H; auto.
adam@344 921 Qed.
adam@344 922
adam@344 923 Print Assumptions proj1.
adam@344 924 (** %\vspace{-.15in}%[[
adam@344 925 Axioms:
adam@344 926 eq_rect_eq : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@344 927 x = eq_rect p Q x p h
adam@344 928 ]]
adam@344 929
adam@344 930 Unfortunately, that built-in tactic appeals to an axiom. It is still possible to avoid axioms by giving the proof via another odd-looking lemma. Here is a first attempt that fails at remaining axiom-free, using a common equality-based trick for supporting induction on non-variable arguments to type families. The trick works fine without axioms for datatypes more traditional than [formula], but we run into trouble with our current type. *)
adam@344 931
adam@344 932 Lemma proj1_again' : forall r, proof r
adam@344 933 -> forall p q, r = And p q -> proof p.
adam@344 934 destruct 1; crush.
adam@344 935 (** %\vspace{-.15in}%[[
adam@344 936 H0 : Inject [] P = And p q
adam@344 937 ============================
adam@344 938 proof p
adam@344 939 ]]
adam@344 940
adam@344 941 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *)
adam@344 942
adam@344 943 discriminate.
adam@344 944 (** %\vspace{-.15in}%[[
adam@344 945 H : proof p
adam@344 946 H1 : And p q = And p0 q0
adam@344 947 ============================
adam@344 948 proof p0
adam@344 949 ]]
adam@344 950
adam@344 951 It looks like we are almost done. Hypothesis [H1] gives [p = p0] by injectivity of constructors, and then [H] finishes the case. *)
adam@344 952
adam@344 953 injection H1; intros.
adam@344 954
adam@344 955 (** Unfortunately, the %``%#"#equality#"#%''% that we expected between [p] and [p0] comes in a strange form:
adam@344 956
adam@344 957 [[
adam@344 958 H3 : existT (fun Ts : list Type => formula Ts) []%list p =
adam@344 959 existT (fun Ts : list Type => formula Ts) []%list p0
adam@344 960 ============================
adam@344 961 proof p0
adam@344 962 ]]
adam@344 963
adam@344 964 It may take a bit of tinkering, but, reviewing Chapter 3's discussion of writing injection principles manually, it makes sense that an [existT] type is the most direct way to express the output of [inversion] on a dependently typed constructor. The constructor [And] is dependently typed, since it takes a parameter [Ts] upon which the types of [p] and [q] depend. Let us not dwell further here on why this goal appears; the reader may like to attempt the (impossible) exercise of building a better injection lemma for [And], without using axioms.
adam@344 965
adam@344 966 How exactly does an axiom come into the picture here? Let us ask [crush] to finish the proof. *)
adam@344 967
adam@344 968 crush.
adam@344 969 Qed.
adam@344 970
adam@344 971 Print Assumptions proj1_again'.
adam@344 972 (** %\vspace{-.15in}%[[
adam@344 973 Axioms:
adam@344 974 eq_rect_eq : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@344 975 x = eq_rect p Q x p h
adam@344 976 ]]
adam@344 977
adam@344 978 It turns out that this familiar axiom about equality (or some other axiom) is required to deduce [p = p0] from the hypothesis [H3] above. The soundness of that proof step is neither provable nor disprovable in Gallina.
adam@344 979
adam@344 980 Hope is not lost, however. We can produce an even stranger looking lemma, which gives us the theorem without axioms. *)
adam@344 981
adam@344 982 Lemma proj1_again'' : forall r, proof r
adam@344 983 -> match r with
adam@344 984 | And Ps p _ => match Ps return formula Ps -> Prop with
adam@344 985 | nil => fun p => proof p
adam@344 986 | _ => fun _ => True
adam@344 987 end p
adam@344 988 | _ => True
adam@344 989 end.
adam@344 990 destruct 1; auto.
adam@344 991 Qed.
adam@344 992
adam@344 993 Theorem proj1_again : forall p q, proof (And p q) -> proof p.
adam@344 994 intros ? ? H; exact (proj1_again'' H).
adam@344 995 Qed.
adam@344 996
adam@344 997 Print Assumptions proj1_again.
adam@344 998 (** <<
adam@344 999 Closed under the global context
adam@344 1000 >>
adam@344 1001
adam@344 1002 This example illustrates again how some of the same design patterns we learned for dependently typed programming can be used fruitfully in theorem statements. *)