## Mercurial > cpdt > repo

### annotate src/Universes.v @ 547:2c8c693ddaba

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Fixes for Coq 8.6

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Wed, 12 Jul 2017 13:08:24 -0400 |

parents | ed829eaa91b2 |

children | af97676583f3 |

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@377 | 11 Require Import List. |

adam@377 | 12 |

adam@534 | 13 Require Import DepList Cpdt.CpdtTactics. |

adamc@227 | 14 |

adamc@227 | 15 Set Implicit Arguments. |

adam@534 | 16 Set Asymmetric Patterns. |

adamc@227 | 17 (* end hide *) |

adamc@227 | 18 |

adam@398 | 19 (** printing $ %({}*% #(<a/>*# *) |

adam@398 | 20 (** printing ^ %*{})% #*<a/>)# *) |

adam@398 | 21 |

adam@398 | 22 |

adamc@227 | 23 |

adamc@227 | 24 (** %\chapter{Universes and Axioms}% *) |

adamc@227 | 25 |

adam@343 | 26 (** 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 | 27 |

adam@343 | 28 %\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 | 29 |

adamc@227 | 30 |

adamc@227 | 31 (** * The [Type] Hierarchy *) |

adamc@227 | 32 |

adam@343 | 33 (** %\index{type hierarchy}%Every object in Gallina has a type. *) |

adamc@227 | 34 |

adamc@227 | 35 Check 0. |

adamc@227 | 36 (** %\vspace{-.15in}% [[ |

adamc@227 | 37 0 |

adamc@227 | 38 : nat |

adamc@227 | 39 ]] |

adamc@227 | 40 |

adamc@227 | 41 It is natural enough that zero be considered as a natural number. *) |

adamc@227 | 42 |

adamc@227 | 43 Check nat. |

adamc@227 | 44 (** %\vspace{-.15in}% [[ |

adamc@227 | 45 nat |

adamc@227 | 46 : Set |

adamc@227 | 47 ]] |

adamc@227 | 48 |

adam@429 | 49 From a set theory perspective, it is unsurprising to consider the natural numbers as a "set." *) |

adamc@227 | 50 |

adamc@227 | 51 Check Set. |

adamc@227 | 52 (** %\vspace{-.15in}% [[ |

adamc@227 | 53 Set |

adamc@227 | 54 : Type |

adamc@227 | 55 ]] |

adamc@227 | 56 |

adam@409 | 57 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 | 58 |

adamc@227 | 59 Check Type. |

adamc@227 | 60 (** %\vspace{-.15in}% [[ |

adamc@227 | 61 Type |

adamc@227 | 62 : Type |

adamc@227 | 63 ]] |

adamc@227 | 64 |

adam@429 | 65 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 | 66 |

adam@343 | 67 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 | 68 |

adamc@227 | 69 Set Printing Universes. |

adamc@227 | 70 |

adamc@227 | 71 Check nat. |

adamc@227 | 72 (** %\vspace{-.15in}% [[ |

adamc@227 | 73 nat |

adamc@227 | 74 : Set |

adam@302 | 75 ]] |

adam@398 | 76 *) |

adamc@227 | 77 |

adamc@227 | 78 Check Set. |

adamc@227 | 79 (** %\vspace{-.15in}% [[ |

adamc@227 | 80 Set |

adamc@227 | 81 : Type $ (0)+1 ^ |

adam@302 | 82 ]] |

adam@302 | 83 *) |

adamc@227 | 84 |

adamc@227 | 85 Check Type. |

adamc@227 | 86 (** %\vspace{-.15in}% [[ |

adamc@227 | 87 Type $ Top.3 ^ |

adamc@227 | 88 : Type $ (Top.3)+1 ^ |

adamc@227 | 89 ]] |

adamc@227 | 90 |

adam@429 | 91 Occurrences of [Type] are annotated with some additional information, inside comments. These annotations have to do with the secret behind [Type]: it really stands for an infinite hierarchy of types. The type of [Set] is [Type(0)], the type of [Type(0)] is [Type(1)], the type of [Type(1)] is [Type(2)], and so on. This is how we avoid the "[Type : Type]" paradox. As a convenience, the universe hierarchy drives Coq's one variety of subtyping. Any term whose type is [Type] at level [i] is automatically also described by [Type] at level [j] when [j > i]. |

adamc@227 | 92 |

adam@398 | 93 In the outputs of our first [Check] query, we see that the type level of [Set]'s type is [(0)+1]. Here [0] stands for the level of [Set], and we increment it to arrive at the level that _classifies_ [Set]. |

adamc@227 | 94 |

adam@488 | 95 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 | 96 |

adam@409 | 97 Another crucial concept in CIC is%\index{predicativity}% _predicativity_. Consider these queries. *) |

adamc@227 | 98 |

adamc@227 | 99 Check forall T : nat, fin T. |

adamc@227 | 100 (** %\vspace{-.15in}% [[ |

adamc@227 | 101 forall T : nat, fin T |

adamc@227 | 102 : Set |

adam@302 | 103 ]] |

adam@302 | 104 *) |

adamc@227 | 105 |

adamc@227 | 106 Check forall T : Set, T. |

adamc@227 | 107 (** %\vspace{-.15in}% [[ |

adamc@227 | 108 forall T : Set, T |

adamc@227 | 109 : Type $ max(0, (0)+1) ^ |

adam@302 | 110 ]] |

adam@302 | 111 *) |

adamc@227 | 112 |

adamc@227 | 113 Check forall T : Type, T. |

adamc@227 | 114 (** %\vspace{-.15in}% [[ |

adamc@227 | 115 forall T : Type $ Top.9 ^ , T |

adamc@227 | 116 : Type $ max(Top.9, (Top.9)+1) ^ |

adamc@227 | 117 ]] |

adamc@227 | 118 |

adamc@227 | 119 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 | 120 |

adam@287 | 121 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 | 122 |

adamc@227 | 123 Definition id (T : Set) (x : T) : T := x. |

adamc@227 | 124 |

adamc@227 | 125 Check id 0. |

adamc@227 | 126 (** %\vspace{-.15in}% [[ |

adamc@227 | 127 id 0 |

adamc@227 | 128 : nat |

adamc@227 | 129 |

adamc@227 | 130 Check id Set. |

adam@343 | 131 ]] |

adamc@227 | 132 |

adam@343 | 133 << |

adamc@227 | 134 Error: Illegal application (Type Error): |

adamc@227 | 135 ... |

adam@479 | 136 The 1st term has type "Type (* (Top.15)+1 *)" |

adam@479 | 137 which should be coercible to "Set". |

adam@343 | 138 >> |

adamc@227 | 139 |

adam@343 | 140 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 | 141 |

adamc@227 | 142 Reset id. |

adamc@227 | 143 Definition id (T : Type) (x : T) : T := x. |

adamc@227 | 144 Check id 0. |

adamc@227 | 145 (** %\vspace{-.15in}% [[ |

adamc@227 | 146 id 0 |

adamc@227 | 147 : nat |

adam@302 | 148 ]] |

adam@302 | 149 *) |

adamc@227 | 150 |

adamc@227 | 151 Check id Set. |

adamc@227 | 152 (** %\vspace{-.15in}% [[ |

adamc@227 | 153 id Set |

adamc@227 | 154 : Type $ Top.17 ^ |

adam@302 | 155 ]] |

adam@302 | 156 *) |

adamc@227 | 157 |

adamc@227 | 158 Check id Type. |

adamc@227 | 159 (** %\vspace{-.15in}% [[ |

adamc@227 | 160 id Type $ Top.18 ^ |

adamc@227 | 161 : Type $ Top.19 ^ |

adam@302 | 162 ]] |

adam@302 | 163 *) |

adamc@227 | 164 |

adamc@227 | 165 (** 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 | 166 [[ |

adamc@227 | 167 Check id id. |

adam@343 | 168 ]] |

adamc@227 | 169 |

adam@343 | 170 << |

adamc@227 | 171 Error: Universe inconsistency (cannot enforce Top.16 < Top.16). |

adam@343 | 172 >> |

adamc@227 | 173 |

adam@479 | 174 %\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 | 175 |

adamc@227 | 176 |

adamc@227 | 177 (** ** Inductive Definitions *) |

adamc@227 | 178 |

adam@505 | 179 (** 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 | 180 [[ |

adamc@227 | 181 Inductive exp : Set -> Set := |

adamc@227 | 182 | Const : forall T : Set, T -> exp T |

adamc@227 | 183 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) |

adamc@227 | 184 | Eq : forall T, exp T -> exp T -> exp bool. |

adam@343 | 185 ]] |

adamc@227 | 186 |

adam@343 | 187 << |

adamc@227 | 188 Error: Large non-propositional inductive types must be in Type. |

adam@343 | 189 >> |

adamc@227 | 190 |

adam@409 | 191 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 | 192 |

adamc@227 | 193 Inductive exp : Type -> Type := |

adamc@227 | 194 | Const : forall T, T -> exp T |

adamc@227 | 195 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) |

adamc@227 | 196 | Eq : forall T, exp T -> exp T -> exp bool. |

adamc@227 | 197 |

adam@505 | 198 (** 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 | 199 |

adamc@228 | 200 Our new definition is accepted. We can build some sample expressions. *) |

adamc@227 | 201 |

adamc@227 | 202 Check Const 0. |

adamc@227 | 203 (** %\vspace{-.15in}% [[ |

adamc@227 | 204 Const 0 |

adamc@227 | 205 : exp nat |

adam@302 | 206 ]] |

adam@302 | 207 *) |

adamc@227 | 208 |

adamc@227 | 209 Check Pair (Const 0) (Const tt). |

adamc@227 | 210 (** %\vspace{-.15in}% [[ |

adamc@227 | 211 Pair (Const 0) (Const tt) |

adamc@227 | 212 : exp (nat * unit) |

adam@302 | 213 ]] |

adam@302 | 214 *) |

adamc@227 | 215 |

adamc@227 | 216 Check Eq (Const Set) (Const Type). |

adamc@227 | 217 (** %\vspace{-.15in}% [[ |

adamc@228 | 218 Eq (Const Set) (Const Type $ Top.59 ^ ) |

adamc@227 | 219 : exp bool |

adamc@227 | 220 ]] |

adamc@227 | 221 |

adamc@227 | 222 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall. |

adamc@227 | 223 [[ |

adamc@227 | 224 Check Const (Const O). |

adam@343 | 225 ]] |

adamc@227 | 226 |

adam@343 | 227 << |

adamc@227 | 228 Error: Universe inconsistency (cannot enforce Top.42 < Top.42). |

adam@343 | 229 >> |

adamc@227 | 230 |

adamc@227 | 231 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 | 232 (** [[ |

adamc@227 | 233 Print exp. |

adam@417 | 234 ]] |

adam@444 | 235 %\vspace{-.15in}%[[ |

adamc@227 | 236 Inductive exp |

adamc@227 | 237 : Type $ Top.8 ^ -> |

adamc@227 | 238 Type |

adamc@227 | 239 $ max(0, (Top.11)+1, (Top.14)+1, (Top.15)+1, (Top.19)+1) ^ := |

adamc@227 | 240 Const : forall T : Type $ Top.11 ^ , T -> exp T |

adamc@227 | 241 | Pair : forall (T1 : Type $ Top.14 ^ ) (T2 : Type $ Top.15 ^ ), |

adamc@227 | 242 exp T1 -> exp T2 -> exp (T1 * T2) |

adamc@227 | 243 | Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool |

adamc@227 | 244 ]] |

adamc@227 | 245 |

adam@505 | 246 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 | 247 |

adam@429 | 248 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 | 249 |

adamc@227 | 250 Print Universes. |

adamc@227 | 251 (** %\vspace{-.15in}% [[ |

adamc@227 | 252 Top.19 < Top.9 <= Top.8 |

adamc@227 | 253 Top.15 < Top.9 <= Top.8 <= Coq.Init.Datatypes.38 |

adamc@227 | 254 Top.14 < Top.9 <= Top.8 <= Coq.Init.Datatypes.37 |

adamc@227 | 255 Top.11 < Top.9 <= Top.8 |

adamc@227 | 256 ]] |

adamc@227 | 257 |

adam@343 | 258 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 | 259 |

adamc@227 | 260 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 | 261 |

adam@417 | 262 (* begin hide *) |

adam@437 | 263 (* begin thide *) |

adam@417 | 264 Inductive prod := pair. |

adam@417 | 265 Reset prod. |

adam@437 | 266 (* end thide *) |

adam@417 | 267 (* end hide *) |

adam@417 | 268 |

adam@444 | 269 (** %\vspace{-.3in}%[[ |

adamc@227 | 270 Print prod. |

adam@417 | 271 ]] |

adam@444 | 272 %\vspace{-.15in}%[[ |

adamc@227 | 273 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ ) |

adamc@227 | 274 (B : Type $ Coq.Init.Datatypes.38 ^ ) |

adamc@227 | 275 : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ := |

adamc@227 | 276 pair : A -> B -> A * B |

adamc@227 | 277 ]] |

adamc@227 | 278 |

adamc@227 | 279 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 | 280 |

adamc@227 | 281 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 | 282 |

adamc@227 | 283 %\medskip% |

adamc@227 | 284 |

adam@505 | 285 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 | 286 |

adamc@231 | 287 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 | 288 |

adamc@227 | 289 Check (nat, (Type, Set)). |

adamc@227 | 290 (** %\vspace{-.15in}% [[ |

adamc@227 | 291 (nat, (Type $ Top.44 ^ , Set)) |

adamc@227 | 292 : Set * (Type $ Top.45 ^ * Type $ Top.46 ^ ) |

adamc@227 | 293 ]] |

adamc@227 | 294 |

adamc@227 | 295 The same cannot be done with a counterpart to [prod] that does not use parameters. *) |

adamc@227 | 296 |

adamc@227 | 297 Inductive prod' : Type -> Type -> Type := |

adamc@227 | 298 | pair' : forall A B : Type, A -> B -> prod' A B. |

adam@444 | 299 (** %\vspace{-.15in}%[[ |

adamc@227 | 300 Check (pair' nat (pair' Type Set)). |

adam@343 | 301 ]] |

adamc@227 | 302 |

adam@343 | 303 << |

adamc@227 | 304 Error: Universe inconsistency (cannot enforce Top.51 < Top.51). |

adam@343 | 305 >> |

adamc@227 | 306 |

adamc@233 | 307 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 | 308 |

adam@343 | 309 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 | 310 |

adamc@233 | 311 Inductive foo (A : Type) : Type := |

adamc@233 | 312 | Foo : A -> foo A. |

adamc@229 | 313 |

adamc@229 | 314 (* begin hide *) |

adamc@229 | 315 Unset Printing Universes. |

adamc@229 | 316 (* end hide *) |

adamc@229 | 317 |

adamc@233 | 318 Check foo nat. |

adamc@233 | 319 (** %\vspace{-.15in}% [[ |

adamc@233 | 320 foo nat |

adamc@233 | 321 : Set |

adam@302 | 322 ]] |

adam@302 | 323 *) |

adamc@233 | 324 |

adamc@233 | 325 Check foo Set. |

adamc@233 | 326 (** %\vspace{-.15in}% [[ |

adamc@233 | 327 foo Set |

adamc@233 | 328 : Type |

adam@302 | 329 ]] |

adam@302 | 330 *) |

adamc@233 | 331 |

adamc@233 | 332 Check foo True. |

adamc@233 | 333 (** %\vspace{-.15in}% [[ |

adamc@233 | 334 foo True |

adamc@233 | 335 : Prop |

adamc@233 | 336 ]] |

adamc@233 | 337 |

adam@429 | 338 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 | 339 |

adamc@233 | 340 Imitation polymorphism can be confusing in some contexts. For instance, it is what is responsible for this weird behavior. *) |

adamc@233 | 341 |

adamc@233 | 342 Inductive bar : Type := Bar : bar. |

adamc@233 | 343 |

adamc@233 | 344 Check bar. |

adamc@233 | 345 (** %\vspace{-.15in}% [[ |

adamc@233 | 346 bar |

adamc@233 | 347 : Prop |

adamc@233 | 348 ]] |

adamc@233 | 349 |

adamc@233 | 350 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *) |

adamc@233 | 351 |

adamc@229 | 352 |

adam@388 | 353 (** ** Deciphering Baffling Messages About Inability to Unify *) |

adam@388 | 354 |

adam@388 | 355 (** 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 | 356 |

adam@388 | 357 Theorem symmetry : forall A B : Type, |

adam@388 | 358 A = B |

adam@388 | 359 -> B = A. |

adam@388 | 360 intros ? ? H; rewrite H; reflexivity. |

adam@388 | 361 Qed. |

adam@388 | 362 |

adam@388 | 363 (** Let us attempt an admittedly silly proof of the following theorem. *) |

adam@388 | 364 |

adam@388 | 365 Theorem illustrative_but_silly_detour : unit = unit. |

adam@444 | 366 (** %\vspace{-.25in}%[[ |

adam@444 | 367 apply symmetry. |

adam@388 | 368 ]] |

adam@388 | 369 << |

adam@388 | 370 Error: Impossible to unify "?35 = ?34" with "unit = unit". |

adam@388 | 371 >> |

adam@388 | 372 |

adam@458 | 373 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 | 374 |

adam@510 | 375 The following command is the secret to getting better error messages in such cases:%\index{Vernacular commands!Set Printing All}% *) |

adam@388 | 376 |

adam@388 | 377 Set Printing All. |

adam@444 | 378 (** %\vspace{-.15in}%[[ |

adam@444 | 379 apply symmetry. |

adam@388 | 380 ]] |

adam@388 | 381 << |

adam@388 | 382 Error: Impossible to unify "@eq Type ?46 ?45" with "@eq Set unit unit". |

adam@388 | 383 >> |

adam@388 | 384 |

adam@398 | 385 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 | 386 |

adam@388 | 387 Abort. |

adam@388 | 388 |

adam@388 | 389 (** 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 | 390 |

adam@388 | 391 Theorem illustrative_but_silly_detour : (unit : Type) = unit. |

adam@388 | 392 apply symmetry; reflexivity. |

adam@388 | 393 Qed. |

adam@388 | 394 |

adam@388 | 395 (** 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 | 396 |

adam@388 | 397 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 | 398 |

adam@388 | 399 Unset Printing All. |

adam@388 | 400 |

adam@388 | 401 Theorem ex_symmetry : (exists x, x = 0) -> (exists x, 0 = x). |

adam@435 | 402 eexists. |

adam@388 | 403 (** %\vspace{-.15in}%[[ |

adam@388 | 404 H : exists x : nat, x = 0 |

adam@388 | 405 ============================ |

adam@388 | 406 0 = ?98 |

adam@388 | 407 ]] |

adam@388 | 408 *) |

adam@388 | 409 |

adam@388 | 410 destruct H. |

adam@388 | 411 (** %\vspace{-.15in}%[[ |

adam@388 | 412 x : nat |

adam@388 | 413 H : x = 0 |

adam@388 | 414 ============================ |

adam@388 | 415 0 = ?99 |

adam@388 | 416 ]] |

adam@388 | 417 *) |

adam@388 | 418 |

adam@444 | 419 (** %\vspace{-.2in}%[[ |

adam@444 | 420 symmetry; exact H. |

adam@388 | 421 ]] |

adam@388 | 422 |

adam@388 | 423 << |

adam@388 | 424 Error: In environment |

adam@388 | 425 x : nat |

adam@388 | 426 H : x = 0 |

adam@388 | 427 The term "H" has type "x = 0" while it is expected to have type |

adam@388 | 428 "?99 = 0". |

adam@388 | 429 >> |

adam@388 | 430 |

adam@398 | 431 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 | 432 |

adam@388 | 433 Restart. |

adam@388 | 434 destruct 1 as [x]; apply ex_intro with x; symmetry; assumption. |

adam@388 | 435 Qed. |

adam@388 | 436 |

adam@429 | 437 (** 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 | 438 |

adam@388 | 439 |

adamc@229 | 440 (** * The [Prop] Universe *) |

adamc@229 | 441 |

adam@429 | 442 (** 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 | 443 |

adamc@229 | 444 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 | 445 |

adamc@229 | 446 Print sig. |

adamc@229 | 447 (** %\vspace{-.15in}% [[ |

adamc@229 | 448 Inductive sig (A : Type) (P : A -> Prop) : Type := |

adamc@229 | 449 exist : forall x : A, P x -> sig P |

adam@302 | 450 ]] |

adam@302 | 451 *) |

adamc@229 | 452 |

adamc@229 | 453 Print ex. |

adamc@229 | 454 (** %\vspace{-.15in}% [[ |

adamc@229 | 455 Inductive ex (A : Type) (P : A -> Prop) : Prop := |

adamc@229 | 456 ex_intro : forall x : A, P x -> ex P |

adamc@229 | 457 ]] |

adamc@229 | 458 |

adamc@229 | 459 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 | 460 |

adamc@229 | 461 Definition projS A (P : A -> Prop) (x : sig P) : A := |

adamc@229 | 462 match x with |

adamc@229 | 463 | exist v _ => v |

adamc@229 | 464 end. |

adamc@229 | 465 |

adam@429 | 466 (* begin hide *) |

adam@437 | 467 (* begin thide *) |

adam@429 | 468 Definition projE := O. |

adam@437 | 469 (* end thide *) |

adam@429 | 470 (* end hide *) |

adam@429 | 471 |

adamc@229 | 472 (** We run into trouble with a version that has been changed to work with [ex]. |

adamc@229 | 473 [[ |

adamc@229 | 474 Definition projE A (P : A -> Prop) (x : ex P) : A := |

adamc@229 | 475 match x with |

adamc@229 | 476 | ex_intro v _ => v |

adamc@229 | 477 end. |

adam@343 | 478 ]] |

adamc@229 | 479 |

adam@343 | 480 << |

adamc@229 | 481 Error: |

adamc@229 | 482 Incorrect elimination of "x" in the inductive type "ex": |

adamc@229 | 483 the return type has sort "Type" while it should be "Prop". |

adamc@229 | 484 Elimination of an inductive object of sort Prop |

adamc@229 | 485 is not allowed on a predicate in sort Type |

adamc@229 | 486 because proofs can be eliminated only to build proofs. |

adam@343 | 487 >> |

adamc@229 | 488 |

adam@429 | 489 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 | 490 |

adamc@229 | 491 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 | 492 |

adam@398 | 493 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 | 494 |

adamc@229 | 495 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) := |

adamc@229 | 496 match x with |

adamc@229 | 497 | exist n pf => exist _ n (sym_eq pf) |

adamc@229 | 498 end. |

adamc@229 | 499 |

adamc@229 | 500 Extraction sym_sig. |

adamc@229 | 501 (** << |

adamc@229 | 502 (** val sym_sig : nat -> nat **) |

adamc@229 | 503 |

adamc@229 | 504 let sym_sig x = x |

adamc@229 | 505 >> |

adamc@229 | 506 |

adamc@229 | 507 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 | 508 |

adamc@229 | 509 Definition sym_ex (x : ex (fun n => n = 0)) : ex (fun n => 0 = n) := |

adamc@229 | 510 match x with |

adamc@229 | 511 | ex_intro n pf => ex_intro _ n (sym_eq pf) |

adamc@229 | 512 end. |

adamc@229 | 513 |

adamc@229 | 514 Extraction sym_ex. |

adamc@229 | 515 (** << |

adamc@229 | 516 (** val sym_ex : __ **) |

adamc@229 | 517 |

adamc@229 | 518 let sym_ex = __ |

adamc@229 | 519 >> |

adamc@229 | 520 |

adam@435 | 521 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 | 522 |

adam@419 | 523 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 | 524 |

adam@398 | 525 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 | 526 |

adamc@229 | 527 %\medskip% |

adamc@229 | 528 |

adam@409 | 529 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 | 530 |

adamc@229 | 531 Check forall P Q : Prop, P \/ Q -> Q \/ P. |

adamc@229 | 532 (** %\vspace{-.15in}% [[ |

adamc@229 | 533 forall P Q : Prop, P \/ Q -> Q \/ P |

adamc@229 | 534 : Prop |

adamc@229 | 535 ]] |

adamc@229 | 536 |

adamc@230 | 537 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 | 538 |

adamc@230 | 539 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 | 540 |

adamc@230 | 541 Inductive expP : Type -> Prop := |

adamc@230 | 542 | ConstP : forall T, T -> expP T |

adamc@230 | 543 | PairP : forall T1 T2, expP T1 -> expP T2 -> expP (T1 * T2) |

adamc@230 | 544 | EqP : forall T, expP T -> expP T -> expP bool. |

adamc@230 | 545 |

adamc@230 | 546 Check ConstP 0. |

adamc@230 | 547 (** %\vspace{-.15in}% [[ |

adamc@230 | 548 ConstP 0 |

adamc@230 | 549 : expP nat |

adam@302 | 550 ]] |

adam@302 | 551 *) |

adamc@230 | 552 |

adamc@230 | 553 Check PairP (ConstP 0) (ConstP tt). |

adamc@230 | 554 (** %\vspace{-.15in}% [[ |

adamc@230 | 555 PairP (ConstP 0) (ConstP tt) |

adamc@230 | 556 : expP (nat * unit) |

adam@302 | 557 ]] |

adam@302 | 558 *) |

adamc@230 | 559 |

adamc@230 | 560 Check EqP (ConstP Set) (ConstP Type). |

adamc@230 | 561 (** %\vspace{-.15in}% [[ |

adamc@230 | 562 EqP (ConstP Set) (ConstP Type) |

adamc@230 | 563 : expP bool |

adam@302 | 564 ]] |

adam@302 | 565 *) |

adamc@230 | 566 |

adamc@230 | 567 Check ConstP (ConstP O). |

adamc@230 | 568 (** %\vspace{-.15in}% [[ |

adamc@230 | 569 ConstP (ConstP 0) |

adamc@230 | 570 : expP (expP nat) |

adamc@230 | 571 ]] |

adamc@230 | 572 |

adam@287 | 573 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 | 574 |

adamc@230 | 575 Inductive eqPlus : forall T, T -> T -> Prop := |

adamc@230 | 576 | Base : forall T (x : T), eqPlus x x |

adamc@230 | 577 | Func : forall dom ran (f1 f2 : dom -> ran), |

adamc@230 | 578 (forall x : dom, eqPlus (f1 x) (f2 x)) |

adamc@230 | 579 -> eqPlus f1 f2. |

adamc@230 | 580 |

adamc@230 | 581 Check (Base 0). |

adamc@230 | 582 (** %\vspace{-.15in}% [[ |

adamc@230 | 583 Base 0 |

adamc@230 | 584 : eqPlus 0 0 |

adam@302 | 585 ]] |

adam@302 | 586 *) |

adamc@230 | 587 |

adamc@230 | 588 Check (Func (fun n => n) (fun n => 0 + n) (fun n => Base n)). |

adamc@230 | 589 (** %\vspace{-.15in}% [[ |

adamc@230 | 590 Func (fun n : nat => n) (fun n : nat => 0 + n) (fun n : nat => Base n) |

adamc@230 | 591 : eqPlus (fun n : nat => n) (fun n : nat => 0 + n) |

adam@302 | 592 ]] |

adam@302 | 593 *) |

adamc@230 | 594 |

adamc@230 | 595 Check (Base (Base 1)). |

adamc@230 | 596 (** %\vspace{-.15in}% [[ |

adamc@230 | 597 Base (Base 1) |

adamc@230 | 598 : eqPlus (Base 1) (Base 1) |

adam@302 | 599 ]] |

adam@302 | 600 *) |

adamc@230 | 601 |

adam@343 | 602 (** 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 | 603 |

adamc@230 | 604 |

adamc@230 | 605 (** * Axioms *) |

adamc@230 | 606 |

adam@409 | 607 (** 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 | 608 |

adamc@230 | 609 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 | 610 |

adamc@230 | 611 (** ** The Basics *) |

adamc@230 | 612 |

adam@343 | 613 (** One simple example of a useful axiom is the %\index{law of the excluded middle}%law of the excluded middle. *) |

adamc@230 | 614 |

adamc@230 | 615 Require Import Classical_Prop. |

adamc@230 | 616 Print classic. |

adamc@230 | 617 (** %\vspace{-.15in}% [[ |

adamc@230 | 618 *** [ classic : forall P : Prop, P \/ ~ P ] |

adamc@230 | 619 ]] |

adamc@230 | 620 |

adam@343 | 621 In the implementation of module [Classical_Prop], this axiom was defined with the command%\index{Vernacular commands!Axiom}% *) |

adamc@230 | 622 |

adamc@230 | 623 Axiom classic : forall P : Prop, P \/ ~ P. |

adamc@230 | 624 |

adam@343 | 625 (** 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 | 626 |

adam@458 | 627 Parameter num : nat. |

adam@458 | 628 Axiom positive : num > 0. |

adam@458 | 629 Reset num. |

adamc@230 | 630 |

adam@429 | 631 (** 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 | 632 |

adam@409 | 633 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 | 634 |

adam@287 | 635 Axiom not_classic : ~ forall P : Prop, P \/ ~ P. |

adamc@230 | 636 |

adamc@230 | 637 Theorem uhoh : False. |

adam@287 | 638 generalize classic not_classic; tauto. |

adamc@230 | 639 Qed. |

adamc@230 | 640 |

adamc@230 | 641 Theorem uhoh_again : 1 + 1 = 3. |

adamc@230 | 642 destruct uhoh. |

adamc@230 | 643 Qed. |

adamc@230 | 644 |

adamc@230 | 645 Reset not_classic. |

adamc@230 | 646 |

adam@429 | 647 (** 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 | 648 |

adam@475 | 649 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 | 650 |

adam@398 | 651 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 | 652 |

adam@343 | 653 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 | 654 |

adamc@230 | 655 Theorem t1 : forall P : Prop, P -> ~ ~ P. |

adamc@230 | 656 tauto. |

adamc@230 | 657 Qed. |

adamc@230 | 658 |

adamc@230 | 659 Print Assumptions t1. |

adam@343 | 660 (** << |

adamc@230 | 661 Closed under the global context |

adam@343 | 662 >> |

adam@302 | 663 *) |

adamc@230 | 664 |

adamc@230 | 665 Theorem t2 : forall P : Prop, ~ ~ P -> P. |

adam@444 | 666 (** %\vspace{-.25in}%[[ |

adamc@230 | 667 tauto. |

adam@343 | 668 ]] |

adam@343 | 669 << |

adamc@230 | 670 Error: tauto failed. |

adam@343 | 671 >> |

adam@302 | 672 *) |

adamc@230 | 673 intro P; destruct (classic P); tauto. |

adamc@230 | 674 Qed. |

adamc@230 | 675 |

adamc@230 | 676 Print Assumptions t2. |

adamc@230 | 677 (** %\vspace{-.15in}% [[ |

adamc@230 | 678 Axioms: |

adamc@230 | 679 classic : forall P : Prop, P \/ ~ P |

adamc@230 | 680 ]] |

adamc@230 | 681 |

adam@398 | 682 It is possible to avoid this dependence in some specific cases, where excluded middle _is_ provable, for decidable families of propositions. *) |

adamc@230 | 683 |

adam@287 | 684 Theorem nat_eq_dec : forall n m : nat, n = m \/ n <> m. |

adamc@230 | 685 induction n; destruct m; intuition; generalize (IHn m); intuition. |

adamc@230 | 686 Qed. |

adamc@230 | 687 |

adamc@230 | 688 Theorem t2' : forall n m : nat, ~ ~ (n = m) -> n = m. |

adam@287 | 689 intros n m; destruct (nat_eq_dec n m); tauto. |

adamc@230 | 690 Qed. |

adamc@230 | 691 |

adamc@230 | 692 Print Assumptions t2'. |

adam@343 | 693 (** << |

adamc@230 | 694 Closed under the global context |

adam@343 | 695 >> |

adamc@230 | 696 |

adamc@230 | 697 %\bigskip% |

adamc@230 | 698 |

adam@409 | 699 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 | 700 |

adamc@230 | 701 Require Import ProofIrrelevance. |

adamc@230 | 702 Print proof_irrelevance. |

adam@458 | 703 |

adamc@230 | 704 (** %\vspace{-.15in}% [[ |

adamc@230 | 705 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ] |

adamc@230 | 706 ]] |

adamc@230 | 707 |

adam@458 | 708 This axiom asserts that any two proofs of the same proposition are equal. Recall this example function from Chapter 6. *) |

adamc@230 | 709 |

adamc@230 | 710 (* begin hide *) |

adamc@230 | 711 Lemma zgtz : 0 > 0 -> False. |

adamc@230 | 712 crush. |

adamc@230 | 713 Qed. |

adamc@230 | 714 (* end hide *) |

adamc@230 | 715 |

adamc@230 | 716 Definition pred_strong1 (n : nat) : n > 0 -> nat := |

adamc@230 | 717 match n with |

adamc@230 | 718 | O => fun pf : 0 > 0 => match zgtz pf with end |

adamc@230 | 719 | S n' => fun _ => n' |

adamc@230 | 720 end. |

adamc@230 | 721 |

adam@343 | 722 (** 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 | 723 |

adamc@230 | 724 Theorem pred_strong1_irrel : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2. |

adamc@230 | 725 destruct n; crush. |

adamc@230 | 726 Qed. |

adamc@230 | 727 |

adamc@230 | 728 (** 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 | 729 |

adamc@230 | 730 Theorem pred_strong1_irrel' : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2. |

adamc@230 | 731 intros; f_equal; apply proof_irrelevance. |

adamc@230 | 732 Qed. |

adamc@230 | 733 |

adamc@230 | 734 |

adamc@230 | 735 (** %\bigskip% |

adamc@230 | 736 |

adamc@230 | 737 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 | 738 |

adamc@230 | 739 Require Import Eqdep. |

adamc@230 | 740 Import Eq_rect_eq. |

adamc@230 | 741 Print eq_rect_eq. |

adamc@230 | 742 (** %\vspace{-.15in}% [[ |

adamc@230 | 743 *** [ eq_rect_eq : |

adamc@230 | 744 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), |

adamc@230 | 745 x = eq_rect p Q x p h ] |

adamc@230 | 746 ]] |

adamc@230 | 747 |

adam@429 | 748 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 | 749 |

adam@426 | 750 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = eq_refl x. |

adam@426 | 751 intros; replace pf with (eq_rect x (eq x) (eq_refl x) x pf); [ |

adamc@230 | 752 symmetry; apply eq_rect_eq |

adamc@230 | 753 | exact (match pf as pf' return match pf' in _ = y return x = y with |

adam@426 | 754 | eq_refl => eq_refl x |

adamc@230 | 755 end = pf' with |

adam@426 | 756 | eq_refl => eq_refl _ |

adamc@230 | 757 end) ]. |

adamc@230 | 758 Qed. |

adamc@230 | 759 |

adamc@230 | 760 Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2. |

adamc@230 | 761 intros; generalize pf1 pf2; subst; intros; |

adamc@230 | 762 match goal with |

adamc@230 | 763 | [ |- ?pf1 = ?pf2 ] => rewrite (UIP_refl pf1); rewrite (UIP_refl pf2); reflexivity |

adamc@230 | 764 end. |

adamc@230 | 765 Qed. |

adamc@230 | 766 |

adam@436 | 767 (* begin hide *) |

adam@437 | 768 (* begin thide *) |

adam@436 | 769 Require Eqdep_dec. |

adam@437 | 770 (* end thide *) |

adam@436 | 771 (* end hide *) |

adam@436 | 772 |

adamc@231 | 773 (** 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 | 774 |

adamc@230 | 775 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 | 776 |

adamc@230 | 777 %\bigskip% |

adamc@230 | 778 |

adamc@230 | 779 There are two more basic axioms that are often assumed, to avoid complications that do not arise in set theory. *) |

adamc@230 | 780 |

adamc@230 | 781 Require Import FunctionalExtensionality. |

adamc@230 | 782 Print functional_extensionality_dep. |

adamc@230 | 783 (** %\vspace{-.15in}% [[ |

adamc@230 | 784 *** [ functional_extensionality_dep : |

adamc@230 | 785 forall (A : Type) (B : A -> Type) (f g : forall x : A, B x), |

adamc@230 | 786 (forall x : A, f x = g x) -> f = g ] |

adamc@230 | 787 |

adamc@230 | 788 ]] |

adamc@230 | 789 |

adamc@230 | 790 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 | 791 |

adam@343 | 792 A simple corollary shows that the same property applies to predicates. *) |

adamc@230 | 793 |

adamc@230 | 794 Corollary predicate_extensionality : forall (A : Type) (B : A -> Prop) (f g : forall x : A, B x), |

adamc@230 | 795 (forall x : A, f x = g x) -> f = g. |

adamc@230 | 796 intros; apply functional_extensionality_dep; assumption. |

adamc@230 | 797 Qed. |

adamc@230 | 798 |

adam@343 | 799 (** In some cases, one might prefer to assert this corollary as the axiom, to restrict the consequences to proofs and not programs. *) |

adam@343 | 800 |

adamc@230 | 801 |

adamc@230 | 802 (** ** Axioms of Choice *) |

adamc@230 | 803 |

adam@343 | 804 (** 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 | 805 |

adam@398 | 806 First, it is possible to implement a choice operator _without_ axioms in some potentially surprising cases. *) |

adamc@230 | 807 |

adamc@230 | 808 Require Import ConstructiveEpsilon. |

adamc@230 | 809 Check constructive_definite_description. |

adamc@230 | 810 (** %\vspace{-.15in}% [[ |

adamc@230 | 811 constructive_definite_description |

adamc@230 | 812 : forall (A : Set) (f : A -> nat) (g : nat -> A), |

adamc@230 | 813 (forall x : A, g (f x) = x) -> |

adamc@230 | 814 forall P : A -> Prop, |

adam@505 | 815 (forall x : A, {P x} + { ~ P x}) -> |

adamc@230 | 816 (exists! x : A, P x) -> {x : A | P x} |

adam@302 | 817 ]] |

adam@302 | 818 *) |

adamc@230 | 819 |

adamc@230 | 820 Print Assumptions constructive_definite_description. |

adam@343 | 821 (** << |

adamc@230 | 822 Closed under the global context |

adam@343 | 823 >> |

adamc@230 | 824 |

adam@398 | 825 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 | 826 |

adamc@230 | 827 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 | 828 |

adamc@230 | 829 Require Import ClassicalUniqueChoice. |

adamc@230 | 830 Check dependent_unique_choice. |

adamc@230 | 831 (** %\vspace{-.15in}% [[ |

adamc@230 | 832 dependent_unique_choice |

adamc@230 | 833 : forall (A : Type) (B : A -> Type) (R : forall x : A, B x -> Prop), |

adamc@230 | 834 (forall x : A, exists! y : B x, R x y) -> |

adam@343 | 835 exists f : forall x : A, B x, |

adam@343 | 836 forall x : A, R x (f x) |

adamc@230 | 837 ]] |

adamc@230 | 838 |

adamc@230 | 839 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 | 840 |

adam@436 | 841 (* begin hide *) |

adam@437 | 842 (* begin thide *) |

adam@436 | 843 Require RelationalChoice. |

adam@437 | 844 (* end thide *) |

adam@436 | 845 (* end hide *) |

adam@436 | 846 |

adamc@230 | 847 Require Import ClassicalChoice. |

adamc@230 | 848 Check choice. |

adamc@230 | 849 (** %\vspace{-.15in}% [[ |

adamc@230 | 850 choice |

adamc@230 | 851 : forall (A B : Type) (R : A -> B -> Prop), |

adamc@230 | 852 (forall x : A, exists y : B, R x y) -> |

adamc@230 | 853 exists f : A -> B, forall x : A, R x (f x) |

adam@444 | 854 ]] |

adamc@230 | 855 |

adamc@230 | 856 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 | 857 |

adamc@230 | 858 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 | 859 |

adamc@230 | 860 Definition choice_Set (A B : Type) (R : A -> B -> Prop) (H : forall x : A, {y : B | R x y}) |

adamc@230 | 861 : {f : A -> B | forall x : A, R x (f x)} := |

adamc@230 | 862 exist (fun f => forall x : A, R x (f x)) |

adamc@230 | 863 (fun x => proj1_sig (H x)) (fun x => proj2_sig (H x)). |

adamc@230 | 864 |

adam@458 | 865 (** %\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 | 866 |

adam@505 | 867 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 | 868 |

adamc@230 | 869 %\bigskip% |

adamc@230 | 870 |

adam@505 | 871 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 | 872 |

adam@505 | 873 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 | 874 |

adamc@230 | 875 (** ** Axioms and Computation *) |

adamc@230 | 876 |

adam@398 | 877 (** 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 | 878 |

adamc@230 | 879 Definition cast (x y : Set) (pf : x = y) (v : x) : y := |

adamc@230 | 880 match pf with |

adam@426 | 881 | eq_refl => v |

adamc@230 | 882 end. |

adamc@230 | 883 |

adamc@230 | 884 (** Computation over programs that use [cast] can proceed smoothly. *) |

adamc@230 | 885 |

adam@426 | 886 Eval compute in (cast (eq_refl (nat -> nat)) (fun n => S n)) 12. |

adam@343 | 887 (** %\vspace{-.15in}%[[ |

adamc@230 | 888 = 13 |

adamc@230 | 889 : nat |

adam@302 | 890 ]] |

adam@302 | 891 *) |

adamc@230 | 892 |

adamc@230 | 893 (** Things do not go as smoothly when we use [cast] with proofs that rely on axioms. *) |

adamc@230 | 894 |

adamc@230 | 895 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)). |

adamc@230 | 896 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n)); |

adamc@230 | 897 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush. |

adamc@230 | 898 Qed. |

adamc@230 | 899 |

adamc@230 | 900 Eval compute in (cast t3 (fun _ => First)) 12. |

adam@444 | 901 (** %\vspace{-.15in}%[[ |

adamc@230 | 902 = match t3 in (_ = P) return P with |

adam@426 | 903 | eq_refl => fun n : nat => First |

adamc@230 | 904 end 12 |

adamc@230 | 905 : fin (12 + 1) |

adamc@230 | 906 ]] |

adamc@230 | 907 |

adam@458 | 908 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 | 909 |

adamc@230 | 910 Reset t3. |

adamc@230 | 911 |

adamc@230 | 912 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)). |

adamc@230 | 913 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n)); |

adamc@230 | 914 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush. |

adamc@230 | 915 Defined. |

adamc@230 | 916 |

adamc@230 | 917 Eval compute in (cast t3 (fun _ => First)) 12. |

adam@444 | 918 (** %\vspace{-.15in}%[[ |

adamc@230 | 919 = match |

adamc@230 | 920 match |

adamc@230 | 921 match |

adamc@230 | 922 functional_extensionality |

adamc@230 | 923 .... |

adamc@230 | 924 ]] |

adamc@230 | 925 |

adam@398 | 926 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 | 927 |

adamc@230 | 928 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *) |

adamc@230 | 929 |

adamc@230 | 930 Lemma plus1 : forall n, S n = n + 1. |

adamc@230 | 931 induction n; simpl; intuition. |

adamc@230 | 932 Defined. |

adamc@230 | 933 |

adamc@230 | 934 Theorem t4 : forall n, fin (S n) = fin (n + 1). |

adamc@230 | 935 intro; f_equal; apply plus1. |

adamc@230 | 936 Defined. |

adamc@230 | 937 |

adamc@230 | 938 Eval compute in cast (t4 13) First. |

adamc@230 | 939 (** %\vspace{-.15in}% [[ |

adamc@230 | 940 = First |

adamc@230 | 941 : fin (13 + 1) |

adam@302 | 942 ]] |

adam@343 | 943 |

adam@426 | 944 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 | 945 |

adam@344 | 946 |

adam@344 | 947 (** ** Methods for Avoiding Axioms *) |

adam@344 | 948 |

adam@409 | 949 (** 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 | 950 |

adam@429 | 951 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 | 952 |

adam@344 | 953 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 | 954 |

adam@344 | 955 Theorem fin_cases : forall n (f : fin (S n)), f = First \/ exists f', f = Next f'. |

adam@344 | 956 intros; dep_destruct f; eauto. |

adam@344 | 957 Qed. |

adam@344 | 958 |

adam@429 | 959 (* begin hide *) |

adam@429 | 960 Require Import JMeq. |

adam@437 | 961 (* begin thide *) |

adam@429 | 962 Definition jme := (JMeq, JMeq_eq). |

adam@437 | 963 (* end thide *) |

adam@429 | 964 (* end hide *) |

adam@429 | 965 |

adam@344 | 966 Print Assumptions fin_cases. |

adam@344 | 967 (** %\vspace{-.15in}%[[ |

adam@344 | 968 Axioms: |

adam@429 | 969 JMeq_eq : forall (A : Type) (x y : A), JMeq x y -> x = y |

adam@344 | 970 ]] |

adam@344 | 971 |

adam@344 | 972 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 | 973 |

adam@344 | 974 (* begin thide *) |

adam@344 | 975 Lemma fin_cases_again' : forall n (f : fin n), |

adam@344 | 976 match n return fin n -> Prop with |

adam@344 | 977 | O => fun _ => False |

adam@344 | 978 | S n' => fun f => f = First \/ exists f', f = Next f' |

adam@344 | 979 end f. |

adam@344 | 980 destruct f; eauto. |

adam@344 | 981 Qed. |

adam@344 | 982 |

adam@344 | 983 (** 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 | 984 |

adam@344 | 985 Theorem fin_cases_again : forall n (f : fin (S n)), f = First \/ exists f', f = Next f'. |

adam@344 | 986 intros; exact (fin_cases_again' f). |

adam@344 | 987 Qed. |

adam@344 | 988 (* end thide *) |

adam@344 | 989 |

adam@344 | 990 Print Assumptions fin_cases_again. |

adam@344 | 991 (** %\vspace{-.15in}% |

adam@344 | 992 << |

adam@344 | 993 Closed under the global context |

adam@344 | 994 >> |

adam@344 | 995 |

adam@345 | 996 *) |

adam@345 | 997 |

adam@345 | 998 (* begin thide *) |

adam@345 | 999 (** 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 | 1000 |

adam@429 | 1001 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 | 1002 |

adam@345 | 1003 Definition finOut n (f : fin n) : match n return fin n -> Type with |

adam@345 | 1004 | O => fun _ => Empty_set |

adam@345 | 1005 | _ => fun f => {f' : _ | f = Next f'} + {f = First} |

adam@345 | 1006 end f := |

adam@345 | 1007 match f with |

adam@426 | 1008 | First _ => inright _ (eq_refl _) |

adam@426 | 1009 | Next _ f' => inleft _ (exist _ f' (eq_refl _)) |

adam@345 | 1010 end. |

adam@345 | 1011 (* end thide *) |

adam@345 | 1012 |

adam@345 | 1013 (** 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 | 1014 |

adam@344 | 1015 Inductive formula : list Type -> Type := |

adam@344 | 1016 | Inject : forall Ts, Prop -> formula Ts |

adam@344 | 1017 | VarEq : forall T Ts, T -> formula (T :: Ts) |

adam@344 | 1018 | Lift : forall T Ts, formula Ts -> formula (T :: Ts) |

adam@344 | 1019 | Forall : forall T Ts, formula (T :: Ts) -> formula Ts |

adam@344 | 1020 | And : forall Ts, formula Ts -> formula Ts -> formula Ts. |

adam@344 | 1021 |

adam@344 | 1022 (** 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 | 1023 |

adam@344 | 1024 Inductive proof : formula nil -> Prop := |

adam@344 | 1025 | PInject : forall (P : Prop), P -> proof (Inject nil P) |

adam@344 | 1026 | PAnd : forall p q, proof p -> proof q -> proof (And p q). |

adam@344 | 1027 |

adam@429 | 1028 (** Let us prove a lemma showing that a "[P /\ Q -> P]" rule is derivable within the rules of [proof]. *) |

adam@344 | 1029 |

adam@344 | 1030 Theorem proj1 : forall p q, proof (And p q) -> proof p. |

adam@344 | 1031 destruct 1. |

adam@344 | 1032 (** %\vspace{-.15in}%[[ |

adam@344 | 1033 p : formula nil |

adam@344 | 1034 q : formula nil |

adam@344 | 1035 P : Prop |

adam@344 | 1036 H : P |

adam@344 | 1037 ============================ |

adam@344 | 1038 proof p |

adam@344 | 1039 ]] |

adam@344 | 1040 *) |

adam@344 | 1041 |

adam@344 | 1042 (** 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 | 1043 |

adam@344 | 1044 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 | 1045 |

adam@344 | 1046 Restart. |

adam@344 | 1047 Require Import Program. |

adam@344 | 1048 intros ? ? H; dependent destruction H; auto. |

adam@344 | 1049 Qed. |

adam@344 | 1050 |

adam@344 | 1051 Print Assumptions proj1. |

adam@344 | 1052 (** %\vspace{-.15in}%[[ |

adam@344 | 1053 Axioms: |

adam@344 | 1054 eq_rect_eq : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), |

adam@344 | 1055 x = eq_rect p Q x p h |

adam@344 | 1056 ]] |

adam@344 | 1057 |

adam@344 | 1058 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 | 1059 |

adam@344 | 1060 Lemma proj1_again' : forall r, proof r |

adam@344 | 1061 -> forall p q, r = And p q -> proof p. |

adam@344 | 1062 destruct 1; crush. |

adam@344 | 1063 (** %\vspace{-.15in}%[[ |

adam@344 | 1064 H0 : Inject [] P = And p q |

adam@344 | 1065 ============================ |

adam@344 | 1066 proof p |

adam@344 | 1067 ]] |

adam@344 | 1068 |

adam@344 | 1069 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *) |

adam@344 | 1070 |

adam@547 | 1071 try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically! |

adam@547 | 1072 * This line left here to keep everything working in |

adam@547 | 1073 * 8.4, 8.5, and 8.6. *) |

adam@344 | 1074 (** %\vspace{-.15in}%[[ |

adam@344 | 1075 H : proof p |

adam@344 | 1076 H1 : And p q = And p0 q0 |

adam@344 | 1077 ============================ |

adam@344 | 1078 proof p0 |

adam@344 | 1079 ]] |

adam@344 | 1080 |

adam@344 | 1081 It looks like we are almost done. Hypothesis [H1] gives [p = p0] by injectivity of constructors, and then [H] finishes the case. *) |

adam@344 | 1082 |

adam@344 | 1083 injection H1; intros. |

adam@344 | 1084 |

adam@429 | 1085 (* begin hide *) |

adam@437 | 1086 (* begin thide *) |

adam@429 | 1087 Definition existT' := existT. |

adam@437 | 1088 (* end thide *) |

adam@429 | 1089 (* end hide *) |

adam@429 | 1090 |

adam@429 | 1091 (** Unfortunately, the "equality" that we expected between [p] and [p0] comes in a strange form: |

adam@344 | 1092 |

adam@344 | 1093 [[ |

adam@344 | 1094 H3 : existT (fun Ts : list Type => formula Ts) []%list p = |

adam@344 | 1095 existT (fun Ts : list Type => formula Ts) []%list p0 |

adam@344 | 1096 ============================ |

adam@344 | 1097 proof p0 |

adam@344 | 1098 ]] |

adam@344 | 1099 |

adam@345 | 1100 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 | 1101 |

adam@344 | 1102 How exactly does an axiom come into the picture here? Let us ask [crush] to finish the proof. *) |

adam@344 | 1103 |

adam@344 | 1104 crush. |

adam@344 | 1105 Qed. |

adam@344 | 1106 |

adam@344 | 1107 Print Assumptions proj1_again'. |

adam@344 | 1108 (** %\vspace{-.15in}%[[ |

adam@344 | 1109 Axioms: |

adam@344 | 1110 eq_rect_eq : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), |

adam@344 | 1111 x = eq_rect p Q x p h |

adam@344 | 1112 ]] |

adam@344 | 1113 |

adam@344 | 1114 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 | 1115 |

adam@479 | 1116 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 | 1117 |

adam@344 | 1118 Lemma proj1_again'' : forall r, proof r |

adam@344 | 1119 -> match r with |

adam@344 | 1120 | And Ps p _ => match Ps return formula Ps -> Prop with |

adam@344 | 1121 | nil => fun p => proof p |

adam@344 | 1122 | _ => fun _ => True |

adam@344 | 1123 end p |

adam@344 | 1124 | _ => True |

adam@344 | 1125 end. |

adam@344 | 1126 destruct 1; auto. |

adam@344 | 1127 Qed. |

adam@344 | 1128 |

adam@344 | 1129 Theorem proj1_again : forall p q, proof (And p q) -> proof p. |

adam@344 | 1130 intros ? ? H; exact (proj1_again'' H). |

adam@344 | 1131 Qed. |

adam@344 | 1132 |

adam@344 | 1133 Print Assumptions proj1_again. |

adam@344 | 1134 (** << |

adam@344 | 1135 Closed under the global context |

adam@344 | 1136 >> |

adam@344 | 1137 |

adam@377 | 1138 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 | 1139 |

adam@377 | 1140 %\medskip% |

adam@377 | 1141 |

adam@398 | 1142 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 | 1143 |

adam@377 | 1144 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 | 1145 |

adam@377 | 1146 Section withTypes. |

adam@377 | 1147 Variable types : list Set. |

adam@377 | 1148 |

adam@377 | 1149 (** 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 | 1150 |

adam@377 | 1151 Variable values : hlist (fun x : Set => x) types. |

adam@377 | 1152 |

adam@377 | 1153 (** 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 | 1154 |

adam@377 | 1155 Variable natIndex : nat. |

adam@377 | 1156 Variable natIndex_ok : nth_error types natIndex = Some nat. |

adam@377 | 1157 |

adam@377 | 1158 (** 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 | 1159 |

adam@377 | 1160 Lemma nth_error_nil : forall A n x, |

adam@377 | 1161 nth_error (@nil A) n = Some x |

adam@377 | 1162 -> False. |

adam@377 | 1163 destruct n; simpl; unfold error; congruence. |

adam@377 | 1164 Defined. |

adam@377 | 1165 |

adam@377 | 1166 Implicit Arguments nth_error_nil [A n x]. |

adam@377 | 1167 |

adam@377 | 1168 Lemma Some_inj : forall A (x y : A), |

adam@377 | 1169 Some x = Some y |

adam@377 | 1170 -> x = y. |

adam@377 | 1171 congruence. |

adam@377 | 1172 Defined. |

adam@377 | 1173 |

adam@377 | 1174 Fixpoint getNat (types' : list Set) (values' : hlist (fun x : Set => x) types') |

adam@377 | 1175 (natIndex : nat) : (nth_error types' natIndex = Some nat) -> nat := |

adam@377 | 1176 match values' with |

adam@377 | 1177 | HNil => fun pf => match nth_error_nil pf with end |

adam@377 | 1178 | HCons t ts x values'' => |

adam@377 | 1179 match natIndex return nth_error (t :: ts) natIndex = Some nat -> nat with |

adam@377 | 1180 | O => fun pf => |

adam@377 | 1181 match Some_inj pf in _ = T return T with |

adam@426 | 1182 | eq_refl => x |

adam@377 | 1183 end |

adam@377 | 1184 | S natIndex' => getNat values'' natIndex' |

adam@377 | 1185 end |

adam@377 | 1186 end. |

adam@377 | 1187 End withTypes. |

adam@377 | 1188 |

adam@377 | 1189 (** The problem becomes apparent when we experiment with running [getNat] on a concrete [types] list. *) |

adam@377 | 1190 |

adam@377 | 1191 Definition myTypes := unit :: nat :: bool :: nil. |

adam@377 | 1192 Definition myValues : hlist (fun x : Set => x) myTypes := |

adam@377 | 1193 tt ::: 3 ::: false ::: HNil. |

adam@377 | 1194 |

adam@377 | 1195 Definition myNatIndex := 1. |

adam@377 | 1196 |

adam@377 | 1197 Theorem myNatIndex_ok : nth_error myTypes myNatIndex = Some nat. |

adam@377 | 1198 reflexivity. |

adam@377 | 1199 Defined. |

adam@377 | 1200 |

adam@377 | 1201 Eval compute in getNat myValues myNatIndex myNatIndex_ok. |

adam@377 | 1202 (** %\vspace{-.15in}%[[ |

adam@377 | 1203 = 3 |

adam@377 | 1204 ]] |

adam@377 | 1205 |

adam@398 | 1206 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 | 1207 |

adam@377 | 1208 Theorem getNat_is_reasonable : forall pf, getNat myValues myNatIndex pf = 3. |

adam@377 | 1209 intro; compute. |

adam@377 | 1210 (** |

adam@377 | 1211 << |

adam@377 | 1212 1 subgoal |

adam@377 | 1213 >> |

adam@377 | 1214 %\vspace{-.3in}%[[ |

adam@377 | 1215 pf : nth_error myTypes myNatIndex = Some nat |

adam@377 | 1216 ============================ |

adam@377 | 1217 match |

adam@377 | 1218 match |

adam@377 | 1219 pf in (_ = y) |

adam@377 | 1220 return (nat = match y with |

adam@377 | 1221 | Some H => H |

adam@377 | 1222 | None => nat |

adam@377 | 1223 end) |

adam@377 | 1224 with |

adam@377 | 1225 | eq_refl => eq_refl |

adam@377 | 1226 end in (_ = T) return T |

adam@377 | 1227 with |

adam@377 | 1228 | eq_refl => 3 |

adam@377 | 1229 end = 3 |

adam@377 | 1230 ]] |

adam@377 | 1231 |

adam@377 | 1232 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 | 1233 |

adam@377 | 1234 Abort. |

adam@377 | 1235 |

adam@377 | 1236 (** 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 | 1237 |

adam@377 | 1238 Fixpoint copies A (x : A) (n : nat) : list A := |

adam@377 | 1239 match n with |

adam@377 | 1240 | O => nil |

adam@377 | 1241 | S n' => x :: copies x n' |

adam@377 | 1242 end. |

adam@377 | 1243 |

adam@377 | 1244 Fixpoint update A (ls : list A) (n : nat) (x : A) : list A := |

adam@377 | 1245 match ls with |

adam@377 | 1246 | nil => copies x n ++ x :: nil |

adam@377 | 1247 | y :: ls' => match n with |

adam@377 | 1248 | O => x :: ls' |

adam@377 | 1249 | S n' => y :: update ls' n' x |

adam@377 | 1250 end |

adam@377 | 1251 end. |

adam@377 | 1252 |

adam@377 | 1253 (** Now let us revisit the definition of [getNat]. *) |

adam@377 | 1254 |

adam@377 | 1255 Section withTypes'. |

adam@377 | 1256 Variable types : list Set. |

adam@377 | 1257 Variable natIndex : nat. |

adam@377 | 1258 |

adam@429 | 1259 (** 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 | 1260 |

adam@377 | 1261 Definition types' := update types natIndex nat. |

adam@377 | 1262 |

adam@377 | 1263 Variable values : hlist (fun x : Set => x) types'. |

adam@377 | 1264 |

adam@377 | 1265 (** Now a bit of dependent pattern matching helps us rewrite [getNat] in a way that avoids any use of equality proofs. *) |

adam@377 | 1266 |

adam@378 | 1267 Fixpoint skipCopies (n : nat) |

adam@378 | 1268 : hlist (fun x : Set => x) (copies nat n ++ nat :: nil) -> nat := |

adam@378 | 1269 match n with |

adam@378 | 1270 | O => fun vs => hhd vs |

adam@378 | 1271 | S n' => fun vs => skipCopies n' (htl vs) |

adam@378 | 1272 end. |

adam@378 | 1273 |

adam@377 | 1274 Fixpoint getNat' (types'' : list Set) (natIndex : nat) |

adam@377 | 1275 : hlist (fun x : Set => x) (update types'' natIndex nat) -> nat := |

adam@377 | 1276 match types'' with |

adam@378 | 1277 | nil => skipCopies natIndex |

adam@377 | 1278 | t :: types0 => |

adam@377 | 1279 match natIndex return hlist (fun x : Set => x) |

adam@377 | 1280 (update (t :: types0) natIndex nat) -> nat with |

adam@377 | 1281 | O => fun vs => hhd vs |

adam@377 | 1282 | S natIndex' => fun vs => getNat' types0 natIndex' (htl vs) |

adam@377 | 1283 end |

adam@377 | 1284 end. |

adam@377 | 1285 End withTypes'. |

adam@377 | 1286 |

adam@398 | 1287 (** 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 | 1288 |

adam@377 | 1289 Theorem getNat_is_reasonable : getNat' myTypes myNatIndex myValues = 3. |

adam@377 | 1290 reflexivity. |

adam@377 | 1291 Qed. |

adam@377 | 1292 |

adam@377 | 1293 (** The same parameters as before work without alteration, and we avoid use of axioms. *) |