Mercurial > cpdt > repo

annotate src/Universes.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents 0ce9829efa3b
children
rev   line source
adam@534 1 (* Copyright (c) 2009-2012, 2015, 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@574 11 Require Import List Lia.
adam@574 12 Hint Extern 2 False => lia.
adam@574 13 Hint Extern 2 (@eq nat _ _) => lia.
adam@377 14
adam@534 15 Require Import DepList Cpdt.CpdtTactics.
adamc@227 16
adam@563 17 Require Extraction.
adam@563 18
adamc@227 19 Set Implicit Arguments.
adam@534 20 Set Asymmetric Patterns.
adamc@227 21 (* end hide *)
adamc@227 22
adam@398 23 (** printing $ %({}*% #(<a/>*# *)
adam@398 24 (** printing ^ %*{})% #*<a/>)# *)
adam@398 25
adam@398 26
adamc@227 27
adamc@227 28 (** %\chapter{Universes and Axioms}% *)
adamc@227 29
adam@343 30 (** 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 31
adam@343 32 %\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 33
adamc@227 34
adamc@227 35 (** * The [Type] Hierarchy *)
adamc@227 36
adam@343 37 (** %\index{type hierarchy}%Every object in Gallina has a type. *)
adamc@227 38
adamc@227 39 Check 0.
adamc@227 40 (** %\vspace{-.15in}% [[
adamc@227 41 0
adamc@227 42 : nat
adamc@227 43 ]]
adamc@227 44
adamc@227 45 It is natural enough that zero be considered as a natural number. *)
adamc@227 46
adamc@227 47 Check nat.
adamc@227 48 (** %\vspace{-.15in}% [[
adamc@227 49 nat
adamc@227 50 : Set
adamc@227 51 ]]
adamc@227 52
adam@429 53 From a set theory perspective, it is unsurprising to consider the natural numbers as a "set." *)
adamc@227 54
adamc@227 55 Check Set.
adamc@227 56 (** %\vspace{-.15in}% [[
adamc@227 57 Set
adamc@227 58 : Type
adamc@227 59 ]]
adamc@227 60
adam@409 61 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)}% _classes_. In Coq, this more general notion is [Type]. *)
adamc@227 62
adamc@227 63 Check Type.
adamc@227 64 (** %\vspace{-.15in}% [[
adamc@227 65 Type
adamc@227 66 : Type
adamc@227 67 ]]
adamc@227 68
adam@429 69 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 70
adam@343 71 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 72
adamc@227 73 Set Printing Universes.
adamc@227 74
adamc@227 75 Check nat.
adamc@227 76 (** %\vspace{-.15in}% [[
adamc@227 77 nat
adamc@227 78 : Set
adam@302 79 ]]
adam@398 80 *)
adamc@227 81
adamc@227 82 Check Set.
adamc@227 83 (** %\vspace{-.15in}% [[
adamc@227 84 Set
adamc@227 85 : Type $ (0)+1 ^
adam@302 86 ]]
adam@302 87 *)
adamc@227 88
adamc@227 89 Check Type.
adamc@227 90 (** %\vspace{-.15in}% [[
adamc@227 91 Type $ Top.3 ^
adamc@227 92 : Type $ (Top.3)+1 ^
adamc@227 93 ]]
adamc@227 94
adam@429 95 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 96
adam@398 97 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 _classifies_ [Set].
adamc@227 98
adam@488 99 In the third query's output, we see that the occurrence of [Type] that we check is assigned a fresh%\index{universe variable}% _universe variable_ [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 100
adam@409 101 Another crucial concept in CIC is%\index{predicativity}% _predicativity_. Consider these queries. *)
adamc@227 102
adamc@227 103 Check forall T : nat, fin T.
adamc@227 104 (** %\vspace{-.15in}% [[
adamc@227 105 forall T : nat, fin T
adamc@227 106 : Set
adam@302 107 ]]
adam@302 108 *)
adamc@227 109
adamc@227 110 Check forall T : Set, T.
adamc@227 111 (** %\vspace{-.15in}% [[
adamc@227 112 forall T : Set, T
adamc@227 113 : Type $ max(0, (0)+1) ^
adam@302 114 ]]
adam@302 115 *)
adamc@227 116
adamc@227 117 Check forall T : Type, T.
adamc@227 118 (** %\vspace{-.15in}% [[
adamc@227 119 forall T : Type $ Top.9 ^ , T
adamc@227 120 : Type $ max(Top.9, (Top.9)+1) ^
adamc@227 121 ]]
adamc@227 122
adamc@227 123 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 124
adam@287 125 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 126
adamc@227 127 Definition id (T : Set) (x : T) : T := x.
adamc@227 128
adamc@227 129 Check id 0.
adamc@227 130 (** %\vspace{-.15in}% [[
adamc@227 131 id 0
adamc@227 132 : nat
adamc@227 133
adamc@227 134 Check id Set.
adam@343 135 ]]
adamc@227 136
adam@343 137 <<
adamc@227 138 Error: Illegal application (Type Error):
adamc@227 139 ...
adam@479 140 The 1st term has type "Type (* (Top.15)+1 *)"
adam@479 141 which should be coercible to "Set".
adam@343 142 >>
adamc@227 143
adam@343 144 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 145
adamc@227 146 Reset id.
adamc@227 147 Definition id (T : Type) (x : T) : T := x.
adamc@227 148 Check id 0.
adamc@227 149 (** %\vspace{-.15in}% [[
adamc@227 150 id 0
adamc@227 151 : nat
adam@302 152 ]]
adam@302 153 *)
adamc@227 154
adamc@227 155 Check id Set.
adamc@227 156 (** %\vspace{-.15in}% [[
adamc@227 157 id Set
adamc@227 158 : Type $ Top.17 ^
adam@302 159 ]]
adam@302 160 *)
adamc@227 161
adamc@227 162 Check id Type.
adamc@227 163 (** %\vspace{-.15in}% [[
adamc@227 164 id Type $ Top.18 ^
adamc@227 165 : Type $ Top.19 ^
adam@302 166 ]]
adam@302 167 *)
adamc@227 168
adamc@227 169 (** 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 170 [[
adamc@227 171 Check id id.
adam@343 172 ]]
adamc@227 173
adam@343 174 <<
adamc@227 175 Error: Universe inconsistency (cannot enforce Top.16 < Top.16).
adam@343 176 >>
adamc@227 177
adam@479 178 %\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 _predicative_, where this word has a CIC meaning closely related to its usual mathematical meaning. A predicative system enforces the constraint that, when an object is defined using some sort of quantifier, none of the 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 179
adamc@227 180
adamc@227 181 (** ** Inductive Definitions *)
adamc@227 182
adam@505 183 (** 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 an encoded expression of type [T].
adamc@227 184 [[
adamc@227 185 Inductive exp : Set -> Set :=
adamc@227 186 | Const : forall T : Set, T -> exp T
adamc@227 187 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 188 | Eq : forall T, exp T -> exp T -> exp bool.
adam@343 189 ]]
adamc@227 190
adam@343 191 <<
adamc@227 192 Error: Large non-propositional inductive types must be in Type.
adam@343 193 >>
adamc@227 194
adam@409 195 This definition is%\index{large inductive types}% _large_ 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 196
adamc@227 197 Inductive exp : Type -> Type :=
adamc@227 198 | Const : forall T, T -> exp T
adamc@227 199 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227 200 | Eq : forall T, exp T -> exp T -> exp bool.
adamc@227 201
adam@505 202 (** 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], the right behavior here, though it was wrong for the [Set] version of [exp].
adamc@228 203
adamc@228 204 Our new definition is accepted. We can build some sample expressions. *)
adamc@227 205
adamc@227 206 Check Const 0.
adamc@227 207 (** %\vspace{-.15in}% [[
adamc@227 208 Const 0
adamc@227 209 : exp nat
adam@302 210 ]]
adam@302 211 *)
adamc@227 212
adamc@227 213 Check Pair (Const 0) (Const tt).
adamc@227 214 (** %\vspace{-.15in}% [[
adamc@227 215 Pair (Const 0) (Const tt)
adamc@227 216 : exp (nat * unit)
adam@302 217 ]]
adam@302 218 *)
adamc@227 219
adamc@227 220 Check Eq (Const Set) (Const Type).
adamc@227 221 (** %\vspace{-.15in}% [[
adamc@228 222 Eq (Const Set) (Const Type $ Top.59 ^ )
adamc@227 223 : exp bool
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 Check Const (Const O).
adam@343 229 ]]
adamc@227 230
adam@343 231 <<
adamc@227 232 Error: Universe inconsistency (cannot enforce Top.42 < Top.42).
adam@343 233 >>
adamc@227 234
adamc@227 235 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. *)
adam@417 236 (** [[
adamc@227 237 Print exp.
adam@417 238 ]]
adam@444 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
adam@505 250 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. Therefore, [exp] _must_ 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 251
adam@429 252 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 253
adamc@227 254 Print Universes.
adamc@227 255 (** %\vspace{-.15in}% [[
adamc@227 256 Top.19 < Top.9 <= Top.8
adamc@227 257 Top.15 < Top.9 <= Top.8 <= Coq.Init.Datatypes.38
adamc@227 258 Top.14 < Top.9 <= Top.8 <= Coq.Init.Datatypes.37
adamc@227 259 Top.11 < Top.9 <= Top.8
adamc@227 260 ]]
adamc@227 261
adam@343 262 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 263
adamc@227 264 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 265
adam@417 266 (* begin hide *)
adam@437 267 (* begin thide *)
adam@417 268 Inductive prod := pair.
adam@417 269 Reset prod.
adam@437 270 (* end thide *)
adam@417 271 (* end hide *)
adam@417 272
adam@444 273 (** %\vspace{-.3in}%[[
adamc@227 274 Print prod.
adam@417 275 ]]
adam@444 276 %\vspace{-.15in}%[[
adamc@227 277 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ )
adamc@227 278 (B : Type $ Coq.Init.Datatypes.38 ^ )
adamc@227 279 : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ :=
adamc@227 280 pair : A -> B -> A * B
adamc@227 281 ]]
adamc@227 282
adamc@227 283 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 284
adamc@227 285 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 286
adamc@227 287 %\medskip%
adamc@227 288
adam@505 289 The annotated definition of [prod] reveals something interesting. 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 _one higher_ than the maximum. The critical difference is that, in the definition of [prod], [A] and [B] are defined as _parameters_; that is, they appear named to the left of the main colon, rather than appearing (possibly unnamed) to the right.
adamc@227 290
adamc@231 291 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 292
adamc@227 293 Check (nat, (Type, Set)).
adamc@227 294 (** %\vspace{-.15in}% [[
adamc@227 295 (nat, (Type $ Top.44 ^ , Set))
adamc@227 296 : Set * (Type $ Top.45 ^ * Type $ Top.46 ^ )
adamc@227 297 ]]
adamc@227 298
adamc@227 299 The same cannot be done with a counterpart to [prod] that does not use parameters. *)
adamc@227 300
adamc@227 301 Inductive prod' : Type -> Type -> Type :=
adamc@227 302 | pair' : forall A B : Type, A -> B -> prod' A B.
adam@444 303 (** %\vspace{-.15in}%[[
adamc@227 304 Check (pair' nat (pair' Type Set)).
adam@343 305 ]]
adamc@227 306
adam@343 307 <<
adamc@227 308 Error: Universe inconsistency (cannot enforce Top.51 < Top.51).
adam@343 309 >>
adamc@227 310
adamc@233 311 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 312
adam@343 313 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 314
adamc@233 315 Inductive foo (A : Type) : Type :=
adamc@233 316 | Foo : A -> foo A.
adamc@229 317
adamc@229 318 (* begin hide *)
adamc@229 319 Unset Printing Universes.
adamc@229 320 (* end hide *)
adamc@229 321
adamc@233 322 Check foo nat.
adamc@233 323 (** %\vspace{-.15in}% [[
adamc@233 324 foo nat
adamc@233 325 : Set
adam@302 326 ]]
adam@302 327 *)
adamc@233 328
adamc@233 329 Check foo Set.
adamc@233 330 (** %\vspace{-.15in}% [[
adamc@233 331 foo Set
adamc@233 332 : Type
adam@302 333 ]]
adam@302 334 *)
adamc@233 335
adamc@233 336 Check foo True.
adamc@233 337 (** %\vspace{-.15in}% [[
adamc@233 338 foo True
adamc@233 339 : Prop
adamc@233 340 ]]
adamc@233 341
adam@429 342 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 343
adamc@233 344 Imitation polymorphism can be confusing in some contexts. For instance, it is what is responsible for this weird behavior. *)
adamc@233 345
adamc@233 346 Inductive bar : Type := Bar : bar.
adamc@233 347
adamc@233 348 Check bar.
adamc@233 349 (** %\vspace{-.15in}% [[
adamc@233 350 bar
adamc@233 351 : Prop
adamc@233 352 ]]
adamc@233 353
adamc@233 354 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *)
adamc@233 355
adamc@229 356
adam@388 357 (** ** Deciphering Baffling Messages About Inability to Unify *)
adam@388 358
adam@388 359 (** One of the most confusing sorts of Coq error messages arises from an interplay between universes, syntax notations, and %\index{implicit arguments}%implicit arguments. Consider the following innocuous lemma, which is symmetry of equality for the special case of types. *)
adam@388 360
adam@388 361 Theorem symmetry : forall A B : Type,
adam@388 362 A = B
adam@388 363 -> B = A.
adam@388 364 intros ? ? H; rewrite H; reflexivity.
adam@388 365 Qed.
adam@388 366
adam@388 367 (** Let us attempt an admittedly silly proof of the following theorem. *)
adam@388 368
adam@388 369 Theorem illustrative_but_silly_detour : unit = unit.
adam@444 370 (** %\vspace{-.25in}%[[
adam@444 371 apply symmetry.
adam@388 372 ]]
adam@388 373 <<
adam@388 374 Error: Impossible to unify "?35 = ?34" with "unit = unit".
adam@388 375 >>
adam@388 376
adam@458 377 Coq tells us that we cannot, in fact, apply our lemma [symmetry] here, but the error message seems defective. In particular, one might think that [apply] should unify [?35] and [?34] with [unit] to ensure that the unification goes through. In fact, the issue is in a part of the unification problem that is _not_ shown to us in this error message!
adam@388 378
adam@510 379 The following command is the secret to getting better error messages in such cases:%\index{Vernacular commands!Set Printing All}% *)
adam@388 380
adam@388 381 Set Printing All.
adam@444 382 (** %\vspace{-.15in}%[[
adam@444 383 apply symmetry.
adam@388 384 ]]
adam@388 385 <<
adam@388 386 Error: Impossible to unify "@eq Type ?46 ?45" with "@eq Set unit unit".
adam@388 387 >>
adam@388 388
adam@398 389 Now we can see the problem: it is the first, _implicit_ argument to the underlying equality function [eq] that disagrees across the two terms. The universe [Set] may be both an element and a subtype of [Type], but the two are not definitionally equal. *)
adam@388 390
adam@388 391 Abort.
adam@388 392
adam@388 393 (** A variety of changes to the theorem statement would lead to use of [Type] as the implicit argument of [eq]. Here is one such change. *)
adam@388 394
adam@388 395 Theorem illustrative_but_silly_detour : (unit : Type) = unit.
adam@388 396 apply symmetry; reflexivity.
adam@388 397 Qed.
adam@388 398
adam@388 399 (** There are many related issues that can come up with error messages, where one or both of notations and implicit arguments hide important details. The [Set Printing All] command turns off all such features and exposes underlying CIC terms.
adam@388 400
adam@388 401 For completeness, we mention one other class of confusing error message about inability to unify two terms that look obviously unifiable. Each unification variable has a scope; a unification variable instantiation may not mention variables that were not already defined within that scope, at the point in proof search where the unification variable was introduced. Consider this illustrative example: *)
adam@388 402
adam@388 403 Unset Printing All.
adam@388 404
adam@388 405 Theorem ex_symmetry : (exists x, x = 0) -> (exists x, 0 = x).
adam@435 406 eexists.
adam@388 407 (** %\vspace{-.15in}%[[
adam@388 408 H : exists x : nat, x = 0
adam@388 409 ============================
adam@388 410 0 = ?98
adam@388 411 ]]
adam@388 412 *)
adam@388 413
adam@388 414 destruct H.
adam@388 415 (** %\vspace{-.15in}%[[
adam@388 416 x : nat
adam@388 417 H : x = 0
adam@388 418 ============================
adam@388 419 0 = ?99
adam@388 420 ]]
adam@388 421 *)
adam@388 422
adam@444 423 (** %\vspace{-.2in}%[[
adam@444 424 symmetry; exact H.
adam@388 425 ]]
adam@388 426
adam@388 427 <<
adam@388 428 Error: In environment
adam@388 429 x : nat
adam@388 430 H : x = 0
adam@388 431 The term "H" has type "x = 0" while it is expected to have type
adam@388 432 "?99 = 0".
adam@388 433 >>
adam@388 434
adam@398 435 The problem here is that variable [x] was introduced by [destruct] _after_ we introduced [?99] with [eexists], so the instantiation of [?99] may not mention [x]. A simple reordering of the proof solves the problem. *)
adam@388 436
adam@388 437 Restart.
adam@388 438 destruct 1 as [x]; apply ex_intro with x; symmetry; assumption.
adam@388 439 Qed.
adam@388 440
adam@429 441 (** This restriction for unification variables may seem counterintuitive, but it follows from the fact that CIC contains no concept of unification variable. Rather, to construct the final proof term, at the point in a proof where the unification variable is introduced, we replace it with the instantiation we eventually find for it. It is simply syntactically illegal to refer there to variables that are not in scope. Without such a restriction, we could trivially "prove" such non-theorems as [exists n : nat, forall m : nat, n = m] by [econstructor; intro; reflexivity]. *)
adam@388 442
adam@388 443
adamc@229 444 (** * The [Prop] Universe *)
adamc@229 445
adam@429 446 (** 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 447
adamc@229 448 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 449
adamc@229 450 Print sig.
adamc@229 451 (** %\vspace{-.15in}% [[
adamc@229 452 Inductive sig (A : Type) (P : A -> Prop) : Type :=
adamc@229 453 exist : forall x : A, P x -> sig P
adam@302 454 ]]
adam@302 455 *)
adamc@229 456
adamc@229 457 Print ex.
adamc@229 458 (** %\vspace{-.15in}% [[
adamc@229 459 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
adamc@229 460 ex_intro : forall x : A, P x -> ex P
adamc@229 461 ]]
adamc@229 462
adamc@229 463 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 464
adamc@229 465 Definition projS A (P : A -> Prop) (x : sig P) : A :=
adamc@229 466 match x with
adamc@229 467 | exist v _ => v
adamc@229 468 end.
adamc@229 469
adam@429 470 (* begin hide *)
adam@437 471 (* begin thide *)
adam@429 472 Definition projE := O.
adam@437 473 (* end thide *)
adam@429 474 (* end hide *)
adam@429 475
adamc@229 476 (** We run into trouble with a version that has been changed to work with [ex].
adamc@229 477 [[
adamc@229 478 Definition projE A (P : A -> Prop) (x : ex P) : A :=
adamc@229 479 match x with
adamc@229 480 | ex_intro v _ => v
adamc@229 481 end.
adam@343 482 ]]
adamc@229 483
adam@343 484 <<
adamc@229 485 Error:
adamc@229 486 Incorrect elimination of "x" in the inductive type "ex":
adamc@229 487 the return type has sort "Type" while it should be "Prop".
adamc@229 488 Elimination of an inductive object of sort Prop
adamc@229 489 is not allowed on a predicate in sort Type
adamc@229 490 because proofs can be eliminated only to build proofs.
adam@343 491 >>
adamc@229 492
adam@429 493 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 494
adamc@229 495 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 496
adam@398 497 Recall that %\index{program extraction}%extraction is Coq's facility for translating Coq developments into programs in general-purpose programming languages like OCaml. Extraction _erases_ proofs and leaves programs intact. A simple example with [sig] and [ex] demonstrates the distinction. *)
adamc@229 498
adamc@229 499 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) :=
adamc@229 500 match x with
adamc@229 501 | exist n pf => exist _ n (sym_eq pf)
adamc@229 502 end.
adamc@229 503
adamc@229 504 Extraction sym_sig.
adamc@229 505 (** <<
adamc@229 506 (** val sym_sig : nat -> nat **)
adamc@229 507
adamc@229 508 let sym_sig x = x
adamc@229 509 >>
adamc@229 510
adamc@229 511 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 512
adamc@229 513 Definition sym_ex (x : ex (fun n => n = 0)) : ex (fun n => 0 = n) :=
adamc@229 514 match x with
adamc@229 515 | ex_intro n pf => ex_intro _ n (sym_eq pf)
adamc@229 516 end.
adamc@229 517
adamc@229 518 Extraction sym_ex.
adamc@229 519 (** <<
adamc@229 520 (** val sym_ex : __ **)
adamc@229 521
adamc@229 522 let sym_ex = __
adamc@229 523 >>
adamc@229 524
adam@435 525 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 <<__>>, whose single constructor is <<__>>. Not only are proofs replaced by [__], but proof arguments to functions are also removed completely, as we see here.
adamc@229 526
adam@419 527 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 528
adam@398 529 Many fans of the %\index{Curry-Howard correspondence}%Curry-Howard correspondence support the idea of _extracting programs from proofs_. 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 530
adamc@229 531 %\medskip%
adamc@229 532
adam@409 533 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}% _impredicative_, as this example shows. *)
adamc@229 534
adamc@229 535 Check forall P Q : Prop, P \/ Q -> Q \/ P.
adamc@229 536 (** %\vspace{-.15in}% [[
adamc@229 537 forall P Q : Prop, P \/ Q -> Q \/ P
adamc@229 538 : Prop
adamc@229 539 ]]
adamc@229 540
adamc@230 541 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 542
adamc@230 543 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 544
adamc@230 545 Inductive expP : Type -> Prop :=
adamc@230 546 | ConstP : forall T, T -> expP T
adamc@230 547 | PairP : forall T1 T2, expP T1 -> expP T2 -> expP (T1 * T2)
adamc@230 548 | EqP : forall T, expP T -> expP T -> expP bool.
adamc@230 549
adamc@230 550 Check ConstP 0.
adamc@230 551 (** %\vspace{-.15in}% [[
adamc@230 552 ConstP 0
adamc@230 553 : expP nat
adam@302 554 ]]
adam@302 555 *)
adamc@230 556
adamc@230 557 Check PairP (ConstP 0) (ConstP tt).
adamc@230 558 (** %\vspace{-.15in}% [[
adamc@230 559 PairP (ConstP 0) (ConstP tt)
adamc@230 560 : expP (nat * unit)
adam@302 561 ]]
adam@302 562 *)
adamc@230 563
adamc@230 564 Check EqP (ConstP Set) (ConstP Type).
adamc@230 565 (** %\vspace{-.15in}% [[
adamc@230 566 EqP (ConstP Set) (ConstP Type)
adamc@230 567 : expP bool
adam@302 568 ]]
adam@302 569 *)
adamc@230 570
adamc@230 571 Check ConstP (ConstP O).
adamc@230 572 (** %\vspace{-.15in}% [[
adamc@230 573 ConstP (ConstP 0)
adamc@230 574 : expP (expP nat)
adamc@230 575 ]]
adamc@230 576
adam@287 577 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 578
adamc@230 579 Inductive eqPlus : forall T, T -> T -> Prop :=
adamc@230 580 | Base : forall T (x : T), eqPlus x x
adamc@230 581 | Func : forall dom ran (f1 f2 : dom -> ran),
adamc@230 582 (forall x : dom, eqPlus (f1 x) (f2 x))
adamc@230 583 -> eqPlus f1 f2.
adamc@230 584
adamc@230 585 Check (Base 0).
adamc@230 586 (** %\vspace{-.15in}% [[
adamc@230 587 Base 0
adamc@230 588 : eqPlus 0 0
adam@302 589 ]]
adam@302 590 *)
adamc@230 591
adamc@230 592 Check (Func (fun n => n) (fun n => 0 + n) (fun n => Base n)).
adamc@230 593 (** %\vspace{-.15in}% [[
adamc@230 594 Func (fun n : nat => n) (fun n : nat => 0 + n) (fun n : nat => Base n)
adamc@230 595 : eqPlus (fun n : nat => n) (fun n : nat => 0 + n)
adam@302 596 ]]
adam@302 597 *)
adamc@230 598
adamc@230 599 Check (Base (Base 1)).
adamc@230 600 (** %\vspace{-.15in}% [[
adamc@230 601 Base (Base 1)
adamc@230 602 : eqPlus (Base 1) (Base 1)
adam@302 603 ]]
adam@302 604 *)
adamc@230 605
adam@343 606 (** 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 607
adamc@230 608
adamc@230 609 (** * Axioms *)
adamc@230 610
adam@409 611 (** 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}% _axioms_ without proof.
adamc@230 612
adamc@230 613 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 614
adamc@230 615 (** ** The Basics *)
adamc@230 616
adam@343 617 (** One simple example of a useful axiom is the %\index{law of the excluded middle}%law of the excluded middle. *)
adamc@230 618
adamc@230 619 Require Import Classical_Prop.
adamc@230 620 Print classic.
adamc@230 621 (** %\vspace{-.15in}% [[
adamc@230 622 *** [ classic : forall P : Prop, P \/ ~ P ]
adamc@230 623 ]]
adamc@230 624
adam@343 625 In the implementation of module [Classical_Prop], this axiom was defined with the command%\index{Vernacular commands!Axiom}% *)
adamc@230 626
adamc@230 627 Axiom classic : forall P : Prop, P \/ ~ P.
adamc@230 628
adam@343 629 (** 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 630
adam@458 631 Parameter num : nat.
adam@458 632 Axiom positive : num > 0.
adam@458 633 Reset num.
adamc@230 634
adam@429 635 (** 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 636
adam@409 637 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}% _inconsistent_. That is, a set of axioms may imply [False], which allows any theorem to be 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 638
adam@287 639 Axiom not_classic : ~ forall P : Prop, P \/ ~ P.
adamc@230 640
adamc@230 641 Theorem uhoh : False.
adam@287 642 generalize classic not_classic; tauto.
adamc@230 643 Qed.
adamc@230 644
adamc@230 645 Theorem uhoh_again : 1 + 1 = 3.
adamc@230 646 destruct uhoh.
adamc@230 647 Qed.
adamc@230 648
adamc@230 649 Reset not_classic.
adamc@230 650
adam@429 651 (** 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 _model_ 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 652
adam@475 653 Recall that Coq implements%\index{constructive logic}% _constructive_ logic by default, where the law of the 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 654
adam@398 655 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] _would_ 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 656
adam@343 657 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 658
adamc@230 659 Theorem t1 : forall P : Prop, P -> ~ ~ P.
adamc@230 660 tauto.
adamc@230 661 Qed.
adamc@230 662
adamc@230 663 Print Assumptions t1.
adam@343 664 (** <<
adamc@230 665 Closed under the global context
adam@343 666 >>
adam@302 667 *)
adamc@230 668
adamc@230 669 Theorem t2 : forall P : Prop, ~ ~ P -> P.
adam@444 670 (** %\vspace{-.25in}%[[
adamc@230 671 tauto.
adam@343 672 ]]
adam@343 673 <<
adamc@230 674 Error: tauto failed.
adam@343 675 >>
adam@302 676 *)
adamc@230 677 intro P; destruct (classic P); tauto.
adamc@230 678 Qed.
adamc@230 679
adamc@230 680 Print Assumptions t2.
adamc@230 681 (** %\vspace{-.15in}% [[
adamc@230 682 Axioms:
adamc@230 683 classic : forall P : Prop, P \/ ~ P
adamc@230 684 ]]
adamc@230 685
adam@398 686 It is possible to avoid this dependence in some specific cases, where excluded middle _is_ provable, for decidable families of propositions. *)
adamc@230 687
adam@287 688 Theorem nat_eq_dec : forall n m : nat, n = m \/ n <> m.
adamc@230 689 induction n; destruct m; intuition; generalize (IHn m); intuition.
adamc@230 690 Qed.
adamc@230 691
adamc@230 692 Theorem t2' : forall n m : nat, ~ ~ (n = m) -> n = m.
adam@287 693 intros n m; destruct (nat_eq_dec n m); tauto.
adamc@230 694 Qed.
adamc@230 695
adamc@230 696 Print Assumptions t2'.
adam@343 697 (** <<
adamc@230 698 Closed under the global context
adam@343 699 >>
adamc@230 700
adamc@230 701 %\bigskip%
adamc@230 702
adam@409 703 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}% _proof irrelevance_, which simplifies proof issues that would not even arise in mainstream math. *)
adamc@230 704
adamc@230 705 Require Import ProofIrrelevance.
adamc@230 706 Print proof_irrelevance.
adam@458 707
adamc@230 708 (** %\vspace{-.15in}% [[
adamc@230 709 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ]
adamc@230 710 ]]
adamc@230 711
adam@458 712 This axiom asserts that any two proofs of the same proposition are equal. Recall this example function from Chapter 6. *)
adamc@230 713
adamc@230 714 (* begin hide *)
adamc@230 715 Lemma zgtz : 0 > 0 -> False.
adamc@230 716 crush.
adamc@230 717 Qed.
adamc@230 718 (* end hide *)
adamc@230 719
adamc@230 720 Definition pred_strong1 (n : nat) : n > 0 -> nat :=
adamc@230 721 match n with
adamc@230 722 | O => fun pf : 0 > 0 => match zgtz pf with end
adamc@230 723 | S n' => fun _ => n'
adamc@230 724 end.
adamc@230 725
adam@343 726 (** 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 727
adamc@230 728 Theorem pred_strong1_irrel : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
adamc@230 729 destruct n; crush.
adamc@230 730 Qed.
adamc@230 731
adamc@230 732 (** 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 733
adamc@230 734 Theorem pred_strong1_irrel' : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
adamc@230 735 intros; f_equal; apply proof_irrelevance.
adamc@230 736 Qed.
adamc@230 737
adamc@230 738
adamc@230 739 (** %\bigskip%
adamc@230 740
adamc@230 741 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 742
adamc@230 743 Require Import Eqdep.
adamc@230 744 Import Eq_rect_eq.
adamc@230 745 Print eq_rect_eq.
adamc@230 746 (** %\vspace{-.15in}% [[
adamc@230 747 *** [ eq_rect_eq :
adamc@230 748 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@230 749 x = eq_rect p Q x p h ]
adamc@230 750 ]]
adamc@230 751
adam@429 752 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 753
adam@426 754 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = eq_refl x.
adam@426 755 intros; replace pf with (eq_rect x (eq x) (eq_refl x) x pf); [
adamc@230 756 symmetry; apply eq_rect_eq
adamc@230 757 | exact (match pf as pf' return match pf' in _ = y return x = y with
adam@426 758 | eq_refl => eq_refl x
adamc@230 759 end = pf' with
adam@426 760 | eq_refl => eq_refl _
adamc@230 761 end) ].
adamc@230 762 Qed.
adamc@230 763
adamc@230 764 Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2.
adamc@230 765 intros; generalize pf1 pf2; subst; intros;
adamc@230 766 match goal with
adamc@230 767 | [ |- ?pf1 = ?pf2 ] => rewrite (UIP_refl pf1); rewrite (UIP_refl pf2); reflexivity
adamc@230 768 end.
adamc@230 769 Qed.
adamc@230 770
adam@436 771 (* begin hide *)
adam@437 772 (* begin thide *)
adam@436 773 Require Eqdep_dec.
adam@437 774 (* end thide *)
adam@436 775 (* end hide *)
adam@436 776
adamc@231 777 (** 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 778
adamc@230 779 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 780
adamc@230 781 %\bigskip%
adamc@230 782
adamc@230 783 There are two more basic axioms that are often assumed, to avoid complications that do not arise in set theory. *)
adamc@230 784
adamc@230 785 Require Import FunctionalExtensionality.
adamc@230 786 Print functional_extensionality_dep.
adamc@230 787 (** %\vspace{-.15in}% [[
adamc@230 788 *** [ functional_extensionality_dep :
adamc@230 789 forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
adamc@230 790 (forall x : A, f x = g x) -> f = g ]
adamc@230 791
adamc@230 792 ]]
adamc@230 793
adamc@230 794 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 795
adam@343 796 A simple corollary shows that the same property applies to predicates. *)
adamc@230 797
adamc@230 798 Corollary predicate_extensionality : forall (A : Type) (B : A -> Prop) (f g : forall x : A, B x),
adamc@230 799 (forall x : A, f x = g x) -> f = g.
adamc@230 800 intros; apply functional_extensionality_dep; assumption.
adamc@230 801 Qed.
adamc@230 802
adam@343 803 (** In some cases, one might prefer to assert this corollary as the axiom, to restrict the consequences to proofs and not programs. *)
adam@343 804
adamc@230 805
adamc@230 806 (** ** Axioms of Choice *)
adamc@230 807
adam@343 808 (** 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 809
adam@398 810 First, it is possible to implement a choice operator _without_ axioms in some potentially surprising cases. *)
adamc@230 811
adamc@230 812 Require Import ConstructiveEpsilon.
adamc@230 813 Check constructive_definite_description.
adamc@230 814 (** %\vspace{-.15in}% [[
adamc@230 815 constructive_definite_description
adamc@230 816 : forall (A : Set) (f : A -> nat) (g : nat -> A),
adamc@230 817 (forall x : A, g (f x) = x) ->
adamc@230 818 forall P : A -> Prop,
adam@505 819 (forall x : A, {P x} + { ~ P x}) ->
adamc@230 820 (exists! x : A, P x) -> {x : A | P x}
adam@302 821 ]]
adam@302 822 *)
adamc@230 823
adamc@230 824 Print Assumptions constructive_definite_description.
adam@343 825 (** <<
adamc@230 826 Closed under the global context
adam@343 827 >>
adamc@230 828
adam@398 829 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 _unique_ 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 830
adamc@230 831 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 832
adamc@230 833 Require Import ClassicalUniqueChoice.
adamc@230 834 Check dependent_unique_choice.
adamc@230 835 (** %\vspace{-.15in}% [[
adamc@230 836 dependent_unique_choice
adamc@230 837 : forall (A : Type) (B : A -> Type) (R : forall x : A, B x -> Prop),
adamc@230 838 (forall x : A, exists! y : B x, R x y) ->
adam@343 839 exists f : forall x : A, B x,
adam@343 840 forall x : A, R x (f x)
adamc@230 841 ]]
adamc@230 842
adamc@230 843 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 844
adam@436 845 (* begin hide *)
adam@437 846 (* begin thide *)
adam@436 847 Require RelationalChoice.
adam@437 848 (* end thide *)
adam@436 849 (* end hide *)
adam@436 850
adamc@230 851 Require Import ClassicalChoice.
adamc@230 852 Check choice.
adamc@230 853 (** %\vspace{-.15in}% [[
adamc@230 854 choice
adamc@230 855 : forall (A B : Type) (R : A -> B -> Prop),
adamc@230 856 (forall x : A, exists y : B, R x y) ->
adamc@230 857 exists f : A -> B, forall x : A, R x (f x)
adam@444 858 ]]
adamc@230 859
adamc@230 860 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 861
adamc@230 862 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 863
adamc@230 864 Definition choice_Set (A B : Type) (R : A -> B -> Prop) (H : forall x : A, {y : B | R x y})
adamc@230 865 : {f : A -> B | forall x : A, R x (f x)} :=
adamc@230 866 exist (fun f => forall x : A, R x (f x))
adamc@230 867 (fun x => proj1_sig (H x)) (fun x => proj2_sig (H x)).
adamc@230 868
adam@458 869 (** %\smallskip{}%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 subtly different. In Gallina, the axioms implement a controlled relaxation of the restrictions on information flow from proofs to programs.
adamc@230 870
adam@505 871 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 combination truly is more than repackaging a function with a different type.
adamc@230 872
adamc@230 873 %\bigskip%
adamc@230 874
adam@505 875 The Coq tools support a command-line flag %\index{impredicative Set}%<<-impredicative-set>>, 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 rule contrasts with the rule for [Prop], where the restriction applies even to non-large inductive types, and where the result type may only have type [Prop].
adamc@230 876
adam@505 877 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, inconsistency can result. Impredicative [Set] can be useful for modeling inherently impredicative mathematical concepts, but almost all Coq developments get by fine without it. *)
adamc@230 878
adamc@230 879 (** ** Axioms and Computation *)
adamc@230 880
adam@398 881 (** One additional axiom-related wrinkle arises from an aspect of Gallina that is very different from set theory: a notion of _computational equivalence_ 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 882
adamc@230 883 Definition cast (x y : Set) (pf : x = y) (v : x) : y :=
adamc@230 884 match pf with
adam@426 885 | eq_refl => v
adamc@230 886 end.
adamc@230 887
adamc@230 888 (** Computation over programs that use [cast] can proceed smoothly. *)
adamc@230 889
adam@426 890 Eval compute in (cast (eq_refl (nat -> nat)) (fun n => S n)) 12.
adam@343 891 (** %\vspace{-.15in}%[[
adamc@230 892 = 13
adamc@230 893 : nat
adam@302 894 ]]
adam@302 895 *)
adamc@230 896
adamc@230 897 (** Things do not go as smoothly when we use [cast] with proofs that rely on axioms. *)
adamc@230 898
adamc@230 899 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
adamc@230 900 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
adamc@230 901 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
adamc@230 902 Qed.
adamc@230 903
adamc@230 904 Eval compute in (cast t3 (fun _ => First)) 12.
adam@444 905 (** %\vspace{-.15in}%[[
adamc@230 906 = match t3 in (_ = P) return P with
adam@426 907 | eq_refl => fun n : nat => First
adamc@230 908 end 12
adamc@230 909 : fin (12 + 1)
adamc@230 910 ]]
adamc@230 911
adam@458 912 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 mistake is easily fixed. *)
adamc@230 913
adamc@230 914 Reset t3.
adamc@230 915
adamc@230 916 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
adamc@230 917 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
adamc@230 918 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
adamc@230 919 Defined.
adamc@230 920
adamc@230 921 Eval compute in (cast t3 (fun _ => First)) 12.
adam@444 922 (** %\vspace{-.15in}%[[
adamc@230 923 = match
adamc@230 924 match
adamc@230 925 match
adamc@230 926 functional_extensionality
adamc@230 927 ....
adamc@230 928 ]]
adamc@230 929
adam@398 930 We elide most of the details. A very unwieldy tree of nested matches on equality proofs appears. This time evaluation really _is_ stuck on a use of an axiom.
adamc@230 931
adamc@230 932 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *)
adamc@230 933
adamc@230 934 Lemma plus1 : forall n, S n = n + 1.
adamc@230 935 induction n; simpl; intuition.
adamc@230 936 Defined.
adamc@230 937
adamc@230 938 Theorem t4 : forall n, fin (S n) = fin (n + 1).
adamc@230 939 intro; f_equal; apply plus1.
adamc@230 940 Defined.
adamc@230 941
adamc@230 942 Eval compute in cast (t4 13) First.
adamc@230 943 (** %\vspace{-.15in}% [[
adamc@230 944 = First
adamc@230 945 : fin (13 + 1)
adam@302 946 ]]
adam@343 947
adam@426 948 This simple computational reduction hides the use of a recursive function to produce a suitable [eq_refl] proof term. The recursion originates in our use of [induction] in [t4]'s proof. *)
adam@343 949
adam@344 950
adam@344 951 (** ** Methods for Avoiding Axioms *)
adam@344 952
adam@409 953 (** 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}% _trusted code base_. 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 954
adam@429 955 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 956
adam@344 957 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 958
adam@344 959 Theorem fin_cases : forall n (f : fin (S n)), f = First \/ exists f', f = Next f'.
adam@344 960 intros; dep_destruct f; eauto.
adam@344 961 Qed.
adam@344 962
adam@429 963 (* begin hide *)
adam@429 964 Require Import JMeq.
adam@437 965 (* begin thide *)
adam@429 966 Definition jme := (JMeq, JMeq_eq).
adam@437 967 (* end thide *)
adam@429 968 (* end hide *)
adam@429 969
adam@344 970 Print Assumptions fin_cases.
adam@344 971 (** %\vspace{-.15in}%[[
adam@344 972 Axioms:
adam@429 973 JMeq_eq : forall (A : Type) (x y : A), JMeq x y -> x = y
adam@344 974 ]]
adam@344 975
adam@344 976 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 977
adam@344 978 (* begin thide *)
adam@344 979 Lemma fin_cases_again' : forall n (f : fin n),
adam@344 980 match n return fin n -> Prop with
adam@344 981 | O => fun _ => False
adam@344 982 | S n' => fun f => f = First \/ exists f', f = Next f'
adam@344 983 end f.
adam@344 984 destruct f; eauto.
adam@344 985 Qed.
adam@344 986
adam@344 987 (** 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 988
adam@344 989 Theorem fin_cases_again : forall n (f : fin (S n)), f = First \/ exists f', f = Next f'.
adam@344 990 intros; exact (fin_cases_again' f).
adam@344 991 Qed.
adam@344 992 (* end thide *)
adam@344 993
adam@344 994 Print Assumptions fin_cases_again.
adam@344 995 (** %\vspace{-.15in}%
adam@344 996 <<
adam@344 997 Closed under the global context
adam@344 998 >>
adam@344 999
adam@345 1000 *)
adam@345 1001
adam@345 1002 (* begin thide *)
adam@345 1003 (** As the Curry-Howard correspondence might lead us to expect, the same pattern may be applied in programming as in proving. Axioms are relevant in programming, too, because, while Coq includes useful extensions like [Program] that make dependently typed programming more straightforward, in general these extensions generate code that relies on axioms about equality. We can use clever pattern matching to write our code axiom-free.
adam@345 1004
adam@429 1005 As an example, consider a [Set] version of [fin_cases]. We use [Set] types instead of [Prop] types, so that return values have computational content and may be used to guide the behavior of algorithms. Beside that, we are essentially writing the same "proof" in a more explicit way. *)
adam@345 1006
adam@345 1007 Definition finOut n (f : fin n) : match n return fin n -> Type with
adam@345 1008 | O => fun _ => Empty_set
adam@345 1009 | _ => fun f => {f' : _ | f = Next f'} + {f = First}
adam@345 1010 end f :=
adam@345 1011 match f with
adam@426 1012 | First _ => inright _ (eq_refl _)
adam@426 1013 | Next _ f' => inleft _ (exist _ f' (eq_refl _))
adam@345 1014 end.
adam@345 1015 (* end thide *)
adam@345 1016
adam@345 1017 (** 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 1018
adam@344 1019 Inductive formula : list Type -> Type :=
adam@344 1020 | Inject : forall Ts, Prop -> formula Ts
adam@344 1021 | VarEq : forall T Ts, T -> formula (T :: Ts)
adam@344 1022 | Lift : forall T Ts, formula Ts -> formula (T :: Ts)
adam@344 1023 | Forall : forall T Ts, formula (T :: Ts) -> formula Ts
adam@344 1024 | And : forall Ts, formula Ts -> formula Ts -> formula Ts.
adam@344 1025
adam@344 1026 (** 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 1027
adam@344 1028 Inductive proof : formula nil -> Prop :=
adam@344 1029 | PInject : forall (P : Prop), P -> proof (Inject nil P)
adam@344 1030 | PAnd : forall p q, proof p -> proof q -> proof (And p q).
adam@344 1031
adam@429 1032 (** Let us prove a lemma showing that a "[P /\ Q -> P]" rule is derivable within the rules of [proof]. *)
adam@344 1033
adam@344 1034 Theorem proj1 : forall p q, proof (And p q) -> proof p.
adam@344 1035 destruct 1.
adam@344 1036 (** %\vspace{-.15in}%[[
adam@344 1037 p : formula nil
adam@344 1038 q : formula nil
adam@344 1039 P : Prop
adam@344 1040 H : P
adam@344 1041 ============================
adam@344 1042 proof p
adam@344 1043 ]]
adam@344 1044 *)
adam@344 1045
adam@344 1046 (** 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 1047
adam@344 1048 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 1049
adam@344 1050 Restart.
adam@344 1051 Require Import Program.
adam@344 1052 intros ? ? H; dependent destruction H; auto.
adam@344 1053 Qed.
adam@344 1054
adam@344 1055 Print Assumptions proj1.
adam@344 1056 (** %\vspace{-.15in}%[[
adam@344 1057 Axioms:
adam@344 1058 eq_rect_eq : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@344 1059 x = eq_rect p Q x p h
adam@344 1060 ]]
adam@344 1061
adam@344 1062 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 1063
adam@344 1064 Lemma proj1_again' : forall r, proof r
adam@344 1065 -> forall p q, r = And p q -> proof p.
adam@344 1066 destruct 1; crush.
adam@344 1067 (** %\vspace{-.15in}%[[
adam@344 1068 H0 : Inject [] P = And p q
adam@344 1069 ============================
adam@344 1070 proof p
adam@344 1071 ]]
adam@344 1072
adam@344 1073 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *)
adam@344 1074
adam@547 1075 try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically!
adam@547 1076 * This line left here to keep everything working in
adam@563 1077 * 8.4 and 8.5. *)
adam@344 1078 (** %\vspace{-.15in}%[[
adam@344 1079 H : proof p
adam@344 1080 H1 : And p q = And p0 q0
adam@344 1081 ============================
adam@344 1082 proof p0
adam@344 1083 ]]
adam@344 1084
adam@344 1085 It looks like we are almost done. Hypothesis [H1] gives [p = p0] by injectivity of constructors, and then [H] finishes the case. *)
adam@344 1086
adam@344 1087 injection H1; intros.
adam@344 1088
adam@429 1089 (* begin hide *)
adam@437 1090 (* begin thide *)
adam@429 1091 Definition existT' := existT.
adam@437 1092 (* end thide *)
adam@429 1093 (* end hide *)
adam@429 1094
adam@429 1095 (** Unfortunately, the "equality" that we expected between [p] and [p0] comes in a strange form:
adam@344 1096
adam@344 1097 [[
adam@344 1098 H3 : existT (fun Ts : list Type => formula Ts) []%list p =
adam@344 1099 existT (fun Ts : list Type => formula Ts) []%list p0
adam@344 1100 ============================
adam@344 1101 proof p0
adam@344 1102 ]]
adam@344 1103
adam@345 1104 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 [injection] 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 1105
adam@344 1106 How exactly does an axiom come into the picture here? Let us ask [crush] to finish the proof. *)
adam@344 1107
adam@344 1108 crush.
adam@344 1109 Qed.
adam@344 1110
adam@344 1111 Print Assumptions proj1_again'.
adam@344 1112 (** %\vspace{-.15in}%[[
adam@344 1113 Axioms:
adam@344 1114 eq_rect_eq : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@344 1115 x = eq_rect p Q x p h
adam@344 1116 ]]
adam@344 1117
adam@344 1118 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 1119
adam@479 1120 Hope is not lost, however. We can produce an even stranger looking lemma, which gives us the theorem without axioms. As always when we want to do case analysis on a term with a tricky dependent type, the key is to refactor the theorem statement so that every term we [match] on has _variables_ as its type indices; so instead of talking about proofs of [And p q], we talk about proofs of an arbitrary [r], but we only conclude anything interesting when [r] is an [And]. *)
adam@344 1121
adam@344 1122 Lemma proj1_again'' : forall r, proof r
adam@344 1123 -> match r with
adam@344 1124 | And Ps p _ => match Ps return formula Ps -> Prop with
adam@344 1125 | nil => fun p => proof p
adam@344 1126 | _ => fun _ => True
adam@344 1127 end p
adam@344 1128 | _ => True
adam@344 1129 end.
adam@344 1130 destruct 1; auto.
adam@344 1131 Qed.
adam@344 1132
adam@344 1133 Theorem proj1_again : forall p q, proof (And p q) -> proof p.
adam@344 1134 intros ? ? H; exact (proj1_again'' H).
adam@344 1135 Qed.
adam@344 1136
adam@344 1137 Print Assumptions proj1_again.
adam@344 1138 (** <<
adam@344 1139 Closed under the global context
adam@344 1140 >>
adam@344 1141
adam@377 1142 This example illustrates again how some of the same design patterns we learned for dependently typed programming can be used fruitfully in theorem statements.
adam@377 1143
adam@377 1144 %\medskip%
adam@377 1145
adam@398 1146 To close the chapter, we consider one final way to avoid dependence on axioms. Often this task is equivalent to writing definitions such that they _compute_. That is, we want Coq's normal reduction to be able to run certain programs to completion. Here is a simple example where such computation can get stuck. In proving properties of such functions, we would need to apply axioms like %\index{axiom K}%K manually to make progress.
adam@377 1147
adam@377 1148 Imagine we are working with %\index{deep embedding}%deeply embedded syntax of some programming language, where each term is considered to be in the scope of a number of free variables that hold normal Coq values. To enforce proper typing, we will need to model a Coq typing environment somehow. One natural choice is as a list of types, where variable number [i] will be treated as a reference to the [i]th element of the list. *)
adam@377 1149
adam@377 1150 Section withTypes.
adam@377 1151 Variable types : list Set.
adam@377 1152
adam@377 1153 (** To give the semantics of terms, we will need to represent value environments, which assign each variable a term of the proper type. *)
adam@377 1154
adam@377 1155 Variable values : hlist (fun x : Set => x) types.
adam@377 1156
adam@377 1157 (** Now imagine that we are writing some procedure that operates on a distinguished variable of type [nat]. A hypothesis formalizes this assumption, using the standard library function [nth_error] for looking up list elements by position. *)
adam@377 1158
adam@377 1159 Variable natIndex : nat.
adam@377 1160 Variable natIndex_ok : nth_error types natIndex = Some nat.
adam@377 1161
adam@377 1162 (** It is not hard to use this hypothesis to write a function for extracting the [nat] value in position [natIndex] of [values], starting with two helpful lemmas, each of which we finish with [Defined] to mark the lemma as transparent, so that its definition may be expanded during evaluation. *)
adam@377 1163
adam@377 1164 Lemma nth_error_nil : forall A n x,
adam@377 1165 nth_error (@nil A) n = Some x
adam@377 1166 -> False.
adam@377 1167 destruct n; simpl; unfold error; congruence.
adam@377 1168 Defined.
adam@377 1169
adam@569 1170 Arguments nth_error_nil [A n x] _.
adam@377 1171
adam@377 1172 Lemma Some_inj : forall A (x y : A),
adam@377 1173 Some x = Some y
adam@377 1174 -> x = y.
adam@377 1175 congruence.
adam@377 1176 Defined.
adam@377 1177
adam@377 1178 Fixpoint getNat (types' : list Set) (values' : hlist (fun x : Set => x) types')
adam@377 1179 (natIndex : nat) : (nth_error types' natIndex = Some nat) -> nat :=
adam@377 1180 match values' with
adam@377 1181 | HNil => fun pf => match nth_error_nil pf with end
adam@377 1182 | HCons t ts x values'' =>
adam@377 1183 match natIndex return nth_error (t :: ts) natIndex = Some nat -> nat with
adam@377 1184 | O => fun pf =>
adam@377 1185 match Some_inj pf in _ = T return T with
adam@426 1186 | eq_refl => x
adam@377 1187 end
adam@377 1188 | S natIndex' => getNat values'' natIndex'
adam@377 1189 end
adam@377 1190 end.
adam@377 1191 End withTypes.
adam@377 1192
adam@377 1193 (** The problem becomes apparent when we experiment with running [getNat] on a concrete [types] list. *)
adam@377 1194
adam@377 1195 Definition myTypes := unit :: nat :: bool :: nil.
adam@377 1196 Definition myValues : hlist (fun x : Set => x) myTypes :=
adam@377 1197 tt ::: 3 ::: false ::: HNil.
adam@377 1198
adam@377 1199 Definition myNatIndex := 1.
adam@377 1200
adam@377 1201 Theorem myNatIndex_ok : nth_error myTypes myNatIndex = Some nat.
adam@377 1202 reflexivity.
adam@377 1203 Defined.
adam@377 1204
adam@377 1205 Eval compute in getNat myValues myNatIndex myNatIndex_ok.
adam@377 1206 (** %\vspace{-.15in}%[[
adam@377 1207 = 3
adam@377 1208 ]]
adam@377 1209
adam@398 1210 We have not hit the problem yet, since we proceeded with a concrete equality proof for [myNatIndex_ok]. However, consider a case where we want to reason about the behavior of [getNat] _independently_ of a specific proof. *)
adam@377 1211
adam@377 1212 Theorem getNat_is_reasonable : forall pf, getNat myValues myNatIndex pf = 3.
adam@377 1213 intro; compute.
adam@377 1214 (**
adam@377 1215 <<
adam@377 1216 1 subgoal
adam@377 1217 >>
adam@377 1218 %\vspace{-.3in}%[[
adam@377 1219 pf : nth_error myTypes myNatIndex = Some nat
adam@377 1220 ============================
adam@377 1221 match
adam@377 1222 match
adam@377 1223 pf in (_ = y)
adam@377 1224 return (nat = match y with
adam@377 1225 | Some H => H
adam@377 1226 | None => nat
adam@377 1227 end)
adam@377 1228 with
adam@377 1229 | eq_refl => eq_refl
adam@377 1230 end in (_ = T) return T
adam@377 1231 with
adam@377 1232 | eq_refl => 3
adam@377 1233 end = 3
adam@377 1234 ]]
adam@377 1235
adam@377 1236 Since the details of the equality proof [pf] are not known, computation can proceed no further. A rewrite with axiom K would allow us to make progress, but we can rethink the definitions a bit to avoid depending on axioms. *)
adam@377 1237
adam@377 1238 Abort.
adam@377 1239
adam@377 1240 (** Here is a definition of a function that turns out to be useful, though no doubt its purpose will be mysterious for now. A call [update ls n x] overwrites the [n]th position of the list [ls] with the value [x], padding the end of the list with extra [x] values as needed to ensure sufficient length. *)
adam@377 1241
adam@377 1242 Fixpoint copies A (x : A) (n : nat) : list A :=
adam@377 1243 match n with
adam@377 1244 | O => nil
adam@377 1245 | S n' => x :: copies x n'
adam@377 1246 end.
adam@377 1247
adam@377 1248 Fixpoint update A (ls : list A) (n : nat) (x : A) : list A :=
adam@377 1249 match ls with
adam@377 1250 | nil => copies x n ++ x :: nil
adam@377 1251 | y :: ls' => match n with
adam@377 1252 | O => x :: ls'
adam@377 1253 | S n' => y :: update ls' n' x
adam@377 1254 end
adam@377 1255 end.
adam@377 1256
adam@377 1257 (** Now let us revisit the definition of [getNat]. *)
adam@377 1258
adam@377 1259 Section withTypes'.
adam@377 1260 Variable types : list Set.
adam@377 1261 Variable natIndex : nat.
adam@377 1262
adam@429 1263 (** Here is the trick: instead of asserting properties about the list [types], we build a "new" list that is _guaranteed by construction_ to have those properties. *)
adam@377 1264
adam@377 1265 Definition types' := update types natIndex nat.
adam@377 1266
adam@377 1267 Variable values : hlist (fun x : Set => x) types'.
adam@377 1268
adam@377 1269 (** Now a bit of dependent pattern matching helps us rewrite [getNat] in a way that avoids any use of equality proofs. *)
adam@377 1270
adam@378 1271 Fixpoint skipCopies (n : nat)
adam@378 1272 : hlist (fun x : Set => x) (copies nat n ++ nat :: nil) -> nat :=
adam@378 1273 match n with
adam@378 1274 | O => fun vs => hhd vs
adam@378 1275 | S n' => fun vs => skipCopies n' (htl vs)
adam@378 1276 end.
adam@378 1277
adam@377 1278 Fixpoint getNat' (types'' : list Set) (natIndex : nat)
adam@377 1279 : hlist (fun x : Set => x) (update types'' natIndex nat) -> nat :=
adam@377 1280 match types'' with
adam@378 1281 | nil => skipCopies natIndex
adam@377 1282 | t :: types0 =>
adam@377 1283 match natIndex return hlist (fun x : Set => x)
adam@377 1284 (update (t :: types0) natIndex nat) -> nat with
adam@377 1285 | O => fun vs => hhd vs
adam@377 1286 | S natIndex' => fun vs => getNat' types0 natIndex' (htl vs)
adam@377 1287 end
adam@377 1288 end.
adam@377 1289 End withTypes'.
adam@377 1290
adam@398 1291 (** Now the surprise comes in how easy it is to _use_ [getNat']. While typing works by modification of a types list, we can choose parameters so that the modification has no effect. *)
adam@377 1292
adam@377 1293 Theorem getNat_is_reasonable : getNat' myTypes myNatIndex myValues = 3.
adam@377 1294 reflexivity.
adam@377 1295 Qed.
adam@377 1296
adam@377 1297 (** The same parameters as before work without alteration, and we avoid use of axioms. *)