Certified Programming with Dependent Types: src/Universes.v annotate

annotate src/Universes.v @ 350:ad315efc3b6b

Stub out new chapter

author	Adam Chlipala <adam@chlipala.net>
date	Wed, 26 Oct 2011 11:19:52 -0400
parents	518c8994a715
children	3322367e955d

rev	line source
adam@343	1 (* Copyright (c) 2009-2011, Adam Chlipala
adamc@227	2 *
adamc@227	3 * This work is licensed under a
adamc@227	4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@227	5 * Unported License.
adamc@227	6 * The license text is available at:
adamc@227	7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@227	8 *)
adamc@227	9
adamc@227	10 (* begin hide *)
adam@314	11 Require Import DepList CpdtTactics.
adamc@227	12
adamc@227	13 Set Implicit Arguments.
adamc@227	14 (* end hide *)
adamc@227	15
adamc@227	16
adamc@227	17 (** %\chapter{Universes and Axioms}% *)
adamc@227	18
adam@343	19 (** Many traditional theorems can be proved in Coq without special knowledge of CIC, the logic behind the prover. A development just seems to be using a particular ASCII notation for standard formulas based on %\index{set theory}%set theory. Nonetheless, as we saw in Chapter 4, CIC differs from set theory in starting from fewer orthogonal primitives. It is possible to define the usual logical connectives as derived notions. The foundation of it all is a dependently typed functional programming language, based on dependent function types and inductive type families. By using the facilities of this language directly, we can accomplish some things much more easily than in mainstream math.
adamc@227	20
adam@343	21 %\index{Gallina}%Gallina, which adds features to the more theoretical CIC%~\cite{CIC}%, is the logic implemented in Coq. It has a relatively simple foundation that can be defined rigorously in a page or two of formal proof rules. Still, there are some important subtleties that have practical ramifications. This chapter focuses on those subtleties, avoiding formal metatheory in favor of example code. *)
adamc@227	22
adamc@227	23
adamc@227	24 (** * The [Type] Hierarchy *)
adamc@227	25
adam@343	26 (** %\index{type hierarchy}%Every object in Gallina has a type. *)
adamc@227	27
adamc@227	28 Check 0.
adamc@227	29 (** %\vspace{-.15in}% [[
adamc@227	30 0
adamc@227	31 : nat
adamc@227	32
adamc@227	33 ]]
adamc@227	34
adamc@227	35 It is natural enough that zero be considered as a natural number. *)
adamc@227	36
adamc@227	37 Check nat.
adamc@227	38 (** %\vspace{-.15in}% [[
adamc@227	39 nat
adamc@227	40 : Set
adamc@227	41
adamc@227	42 ]]
adamc@227	43
adam@287	44 From a set theory perspective, it is unsurprising to consider the natural numbers as a %``%#"#set.#"#%''% *)
adamc@227	45
adamc@227	46 Check Set.
adamc@227	47 (** %\vspace{-.15in}% [[
adamc@227	48 Set
adamc@227	49 : Type
adamc@227	50
adamc@227	51 ]]
adamc@227	52
adam@343	53 The type [Set] may be considered as the set of all sets, a concept that set theory handles in terms of %\index{class (in set theory)}\textit{%#<i>#classes#</i>#%}%. In Coq, this more general notion is [Type]. *)
adamc@227	54
adamc@227	55 Check Type.
adamc@227	56 (** %\vspace{-.15in}% [[
adamc@227	57 Type
adamc@227	58 : Type
adamc@227	59
adamc@227	60 ]]
adamc@227	61
adam@343	62 Strangely enough, [Type] appears to be its own type. It is known that polymorphic languages with this property are inconsistent, via %\index{Girard's paradox}%Girard's paradox%~\cite{GirardsParadox}%. That is, using such a language to encode proofs is unwise, because it is possible to %``%#"#prove#"#%''% any proposition. What is really going on here?
adamc@227	63
adam@343	64 Let us repeat some of our queries after toggling a flag related to Coq's printing behavior.%\index{Vernacular commands!Set Printing Universes}% *)
adamc@227	65
adamc@227	66 Set Printing Universes.
adamc@227	67
adamc@227	68 Check nat.
adamc@227	69 (** %\vspace{-.15in}% [[
adamc@227	70 nat
adamc@227	71 : Set
adam@302	72 ]]
adam@302	73 *)
adamc@227	74
adamc@227	75 (** printing $ %({}% #(<a/># *)
adamc@227	76 (** printing ^ %{})% #<a/>)# *)
adamc@227	77
adamc@227	78 Check Set.
adamc@227	79 (** %\vspace{-.15in}% [[
adamc@227	80 Set
adamc@227	81 : Type $ (0)+1 ^
adamc@227	82
adam@302	83 ]]
adam@302	84 *)
adamc@227	85
adamc@227	86 Check Type.
adamc@227	87 (** %\vspace{-.15in}% [[
adamc@227	88 Type $ Top.3 ^
adamc@227	89 : Type $ (Top.3)+1 ^
adamc@227	90
adamc@227	91 ]]
adamc@227	92
adam@287	93 Occurrences of [Type] are annotated with some additional information, inside comments. These annotations have to do with the secret behind [Type]: it really stands for an infinite hierarchy of types. The type of [Set] is [Type(0)], the type of [Type(0)] is [Type(1)], the type of [Type(1)] is [Type(2)], and so on. This is how we avoid the %``%#"#[Type : Type]#"#%''% paradox. As a convenience, the universe hierarchy drives Coq's one variety of subtyping. Any term whose type is [Type] at level [i] is automatically also described by [Type] at level [j] when [j > i].
adamc@227	94
adamc@227	95 In the outputs of our first [Check] query, we see that the type level of [Set]'s type is [(0)+1]. Here [0] stands for the level of [Set], and we increment it to arrive at the level that %\textit{%#<i>#classifies#</i>#%}% [Set].
adamc@227	96
adam@343	97 In the second query's output, we see that the occurrence of [Type] that we check is assigned a fresh %\index{universe variable}\textit{%#<i>#universe variable#</i>#%}% [Top.3]. The output type increments [Top.3] to move up a level in the universe hierarchy. As we write code that uses definitions whose types mention universe variables, unification may refine the values of those variables. Luckily, the user rarely has to worry about the details.
adamc@227	98
adam@343	99 Another crucial concept in CIC is %\index{predicativity}\textit{%#<i>#predicativity#</i>#%}%. Consider these queries. *)
adamc@227	100
adamc@227	101 Check forall T : nat, fin T.
adamc@227	102 (** %\vspace{-.15in}% [[
adamc@227	103 forall T : nat, fin T
adamc@227	104 : Set
adam@302	105 ]]
adam@302	106 *)
adamc@227	107
adamc@227	108 Check forall T : Set, T.
adamc@227	109 (** %\vspace{-.15in}% [[
adamc@227	110 forall T : Set, T
adamc@227	111 : Type $ max(0, (0)+1) ^
adam@302	112 ]]
adam@302	113 *)
adamc@227	114
adamc@227	115 Check forall T : Type, T.
adamc@227	116 (** %\vspace{-.15in}% [[
adamc@227	117 forall T : Type $ Top.9 ^ , T
adamc@227	118 : Type $ max(Top.9, (Top.9)+1) ^
adamc@227	119
adamc@227	120 ]]
adamc@227	121
adamc@227	122 These outputs demonstrate the rule for determining which universe a [forall] type lives in. In particular, for a type [forall x : T1, T2], we take the maximum of the universes of [T1] and [T2]. In the first example query, both [T1] ([nat]) and [T2] ([fin T]) are in [Set], so the [forall] type is in [Set], too. In the second query, [T1] is [Set], which is at level [(0)+1]; and [T2] is [T], which is at level [0]. Thus, the [forall] exists at the maximum of these two levels. The third example illustrates the same outcome, where we replace [Set] with an occurrence of [Type] that is assigned universe variable [Top.9]. This universe variable appears in the places where [0] appeared in the previous query.
adamc@227	123
adam@287	124 The behind-the-scenes manipulation of universe variables gives us predicativity. Consider this simple definition of a polymorphic identity function, where the first argument [T] will automatically be marked as implicit, since it can be inferred from the type of the second argument [x]. *)
adamc@227	125
adamc@227	126 Definition id (T : Set) (x : T) : T := x.
adamc@227	127
adamc@227	128 Check id 0.
adamc@227	129 (** %\vspace{-.15in}% [[
adamc@227	130 id 0
adamc@227	131 : nat
adamc@227	132
adamc@227	133 Check id Set.
adam@343	134 ]]
adamc@227	135
adam@343	136 <<
adamc@227	137 Error: Illegal application (Type Error):
adamc@227	138 ...
adam@343	139 The 1st term has type "Type (* (Top.15)+1 *)" which should be coercible to "Set".
adam@343	140 >>
adamc@227	141
adam@343	142 The parameter [T] of [id] must be instantiated with a [Set]. The type [nat] is a [Set], but [Set] is not. We can try fixing the problem by generalizing our definition of [id]. *)
adamc@227	143
adamc@227	144 Reset id.
adamc@227	145 Definition id (T : Type) (x : T) : T := x.
adamc@227	146 Check id 0.
adamc@227	147 (** %\vspace{-.15in}% [[
adamc@227	148 id 0
adamc@227	149 : nat
adam@302	150 ]]
adam@302	151 *)
adamc@227	152
adamc@227	153 Check id Set.
adamc@227	154 (** %\vspace{-.15in}% [[
adamc@227	155 id Set
adamc@227	156 : Type $ Top.17 ^
adam@302	157 ]]
adam@302	158 *)
adamc@227	159
adamc@227	160 Check id Type.
adamc@227	161 (** %\vspace{-.15in}% [[
adamc@227	162 id Type $ Top.18 ^
adamc@227	163 : Type $ Top.19 ^
adam@302	164 ]]
adam@302	165 *)
adamc@227	166
adamc@227	167 (** So far so good. As we apply [id] to different [T] values, the inferred index for [T]'s [Type] occurrence automatically moves higher up the type hierarchy.
adamc@227	168 [[
adamc@227	169 Check id id.
adam@343	170 ]]
adamc@227	171
adam@343	172 <<
adamc@227	173 Error: Universe inconsistency (cannot enforce Top.16 < Top.16).
adam@343	174 >>
adamc@227	175
adam@343	176 %\index{universe inconsistency}%This error message reminds us that the universe variable for [T] still exists, even though it is usually hidden. To apply [id] to itself, that variable would need to be less than itself in the type hierarchy. Universe inconsistency error messages announce cases like this one where a term could only type-check by violating an implied constraint over universe variables. Such errors demonstrate that [Type] is %\textit{%#<i>#predicative#</i>#%}%, where this word has a CIC meaning closely related to its usual mathematical meaning. A predicative system enforces the constraint that, for any object of quantified type, none of those quantifiers may ever be instantiated with the object itself. %\index{impredicativity}%Impredicativity is associated with popular paradoxes in set theory, involving inconsistent constructions like %``%#"#the set of all sets that do not contain themselves#"#%''% (%\index{Russell's paradox}%Russell's paradox). Similar paradoxes would result from uncontrolled impredicativity in Coq. *)
adamc@227	177
adamc@227	178
adamc@227	179 ( Inductive Definitions *)
adamc@227	180
adamc@227	181 (** Predicativity restrictions also apply to inductive definitions. As an example, let us consider a type of expression trees that allows injection of any native Coq value. The idea is that an [exp T] stands for a reflected expression of type [T].
adamc@227	182
adamc@227	183 [[
adamc@227	184 Inductive exp : Set -> Set :=
adamc@227	185 \| Const : forall T : Set, T -> exp T
adamc@227	186 \| Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227	187 \| Eq : forall T, exp T -> exp T -> exp bool.
adam@343	188 ]]
adamc@227	189
adam@343	190 <<
adamc@227	191 Error: Large non-propositional inductive types must be in Type.
adam@343	192 >>
adamc@227	193
adam@343	194 This definition is %\index{large inductive types}\textit{%#<i>#large#</i>#%}% in the sense that at least one of its constructors takes an argument whose type has type [Type]. Coq would be inconsistent if we allowed definitions like this one in their full generality. Instead, we must change [exp] to live in [Type]. We will go even further and move [exp]'s index to [Type] as well. *)
adamc@227	195
adamc@227	196 Inductive exp : Type -> Type :=
adamc@227	197 \| Const : forall T, T -> exp T
adamc@227	198 \| Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227	199 \| Eq : forall T, exp T -> exp T -> exp bool.
adamc@227	200
adamc@228	201 (** Note that before we had to include an annotation [: Set] for the variable [T] in [Const]'s type, but we need no annotation now. When the type of a variable is not known, and when that variable is used in a context where only types are allowed, Coq infers that the variable is of type [Type]. That is the right behavior here, but it was wrong for the [Set] version of [exp].
adamc@228	202
adamc@228	203 Our new definition is accepted. We can build some sample expressions. *)
adamc@227	204
adamc@227	205 Check Const 0.
adamc@227	206 (** %\vspace{-.15in}% [[
adamc@227	207 Const 0
adamc@227	208 : exp nat
adam@302	209 ]]
adam@302	210 *)
adamc@227	211
adamc@227	212 Check Pair (Const 0) (Const tt).
adamc@227	213 (** %\vspace{-.15in}% [[
adamc@227	214 Pair (Const 0) (Const tt)
adamc@227	215 : exp (nat * unit)
adam@302	216 ]]
adam@302	217 *)
adamc@227	218
adamc@227	219 Check Eq (Const Set) (Const Type).
adamc@227	220 (** %\vspace{-.15in}% [[
adamc@228	221 Eq (Const Set) (Const Type $ Top.59 ^ )
adamc@227	222 : exp bool
adamc@227	223
adamc@227	224 ]]
adamc@227	225
adamc@227	226 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall.
adamc@227	227
adamc@227	228 [[
adamc@227	229 Check Const (Const O).
adam@343	230 ]]
adamc@227	231
adam@343	232 <<
adamc@227	233 Error: Universe inconsistency (cannot enforce Top.42 < Top.42).
adam@343	234 >>
adamc@227	235
adamc@227	236 We are unable to instantiate the parameter [T] of [Const] with an [exp] type. To see why, it is helpful to print the annotated version of [exp]'s inductive definition. *)
adamc@227	237
adamc@227	238 Print exp.
adamc@227	239 (** %\vspace{-.15in}% [[
adamc@227	240 Inductive exp
adamc@227	241 : Type $ Top.8 ^ ->
adamc@227	242 Type
adamc@227	243 $ max(0, (Top.11)+1, (Top.14)+1, (Top.15)+1, (Top.19)+1) ^ :=
adamc@227	244 Const : forall T : Type $ Top.11 ^ , T -> exp T
adamc@227	245 \| Pair : forall (T1 : Type $ Top.14 ^ ) (T2 : Type $ Top.15 ^ ),
adamc@227	246 exp T1 -> exp T2 -> exp (T1 * T2)
adamc@227	247 \| Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool
adamc@227	248
adamc@227	249 ]]
adamc@227	250
adamc@227	251 We see that the index type of [exp] has been assigned to universe level [Top.8]. In addition, each of the four occurrences of [Type] in the types of the constructors gets its own universe variable. Each of these variables appears explicitly in the type of [exp]. In particular, any type [exp T] lives at a universe level found by incrementing by one the maximum of the four argument variables. A consequence of this is that [exp] %\textit{%#<i>#must#</i>#%}% live at a higher universe level than any type which may be passed to one of its constructors. This consequence led to the universe inconsistency.
adamc@227	252
adam@343	253 Strangely, the universe variable [Top.8] only appears in one place. Is there no restriction imposed on which types are valid arguments to [exp]? In fact, there is a restriction, but it only appears in a global set of universe constraints that are maintained %``%#"#off to the side,#"#%''% not appearing explicitly in types. We can print the current database.%\index{Vernacular commands!Print Universes}% *)
adamc@227	254
adamc@227	255 Print Universes.
adamc@227	256 (** %\vspace{-.15in}% [[
adamc@227	257 Top.19 < Top.9 <= Top.8
adamc@227	258 Top.15 < Top.9 <= Top.8 <= Coq.Init.Datatypes.38
adamc@227	259 Top.14 < Top.9 <= Top.8 <= Coq.Init.Datatypes.37
adamc@227	260 Top.11 < Top.9 <= Top.8
adamc@227	261
adamc@227	262 ]]
adamc@227	263
adam@343	264 The command outputs many more constraints, but we have collected only those that mention [Top] variables. We see one constraint for each universe variable associated with a constructor argument from [exp]'s definition. Universe variable [Top.19] is the type argument to [Eq]. The constraint for [Top.19] effectively says that [Top.19] must be less than [Top.8], the universe of [exp]'s indices; an intermediate variable [Top.9] appears as an artifact of the way the constraint was generated.
adamc@227	265
adamc@227	266 The next constraint, for [Top.15], is more complicated. This is the universe of the second argument to the [Pair] constructor. Not only must [Top.15] be less than [Top.8], but it also comes out that [Top.8] must be less than [Coq.Init.Datatypes.38]. What is this new universe variable? It is from the definition of the [prod] inductive family, to which types of the form [A * B] are desugared. *)
adamc@227	267
adamc@227	268 Print prod.
adamc@227	269 (** %\vspace{-.15in}% [[
adamc@227	270 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ )
adamc@227	271 (B : Type $ Coq.Init.Datatypes.38 ^ )
adamc@227	272 : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ :=
adamc@227	273 pair : A -> B -> A * B
adamc@227	274
adamc@227	275 ]]
adamc@227	276
adamc@227	277 We see that the constraint is enforcing that indices to [exp] must not live in a higher universe level than [B]-indices to [prod]. The next constraint above establishes a symmetric condition for [A].
adamc@227	278
adamc@227	279 Thus it is apparent that Coq maintains a tortuous set of universe variable inequalities behind the scenes. It may look like some functions are polymorphic in the universe levels of their arguments, but what is really happening is imperative updating of a system of constraints, such that all uses of a function are consistent with a global set of universe levels. When the constraint system may not be evolved soundly, we get a universe inconsistency error.
adamc@227	280
adamc@227	281 %\medskip%
adamc@227	282
adamc@227	283 Something interesting is revealed in the annotated definition of [prod]. A type [prod A B] lives at a universe that is the maximum of the universes of [A] and [B]. From our earlier experiments, we might expect that [prod]'s universe would in fact need to be %\textit{%#<i>#one higher#</i>#%}% than the maximum. The critical difference is that, in the definition of [prod], [A] and [B] are defined as %\textit{%#<i>#parameters#</i>#%}%; that is, they appear named to the left of the main colon, rather than appearing (possibly unnamed) to the right.
adamc@227	284
adamc@231	285 Parameters are not as flexible as normal inductive type arguments. The range types of all of the constructors of a parameterized type must share the same parameters. Nonetheless, when it is possible to define a polymorphic type in this way, we gain the ability to use the new type family in more ways, without triggering universe inconsistencies. For instance, nested pairs of types are perfectly legal. *)
adamc@227	286
adamc@227	287 Check (nat, (Type, Set)).
adamc@227	288 (** %\vspace{-.15in}% [[
adamc@227	289 (nat, (Type $ Top.44 ^ , Set))
adamc@227	290 : Set * (Type $ Top.45 ^ * Type $ Top.46 ^ )
adamc@227	291 ]]
adamc@227	292
adamc@227	293 The same cannot be done with a counterpart to [prod] that does not use parameters. *)
adamc@227	294
adamc@227	295 Inductive prod' : Type -> Type -> Type :=
adamc@227	296 \| pair' : forall A B : Type, A -> B -> prod' A B.
adamc@227	297 (** [[
adamc@227	298 Check (pair' nat (pair' Type Set)).
adam@343	299 ]]
adamc@227	300
adam@343	301 <<
adamc@227	302 Error: Universe inconsistency (cannot enforce Top.51 < Top.51).
adam@343	303 >>
adamc@227	304
adamc@233	305 The key benefit parameters bring us is the ability to avoid quantifying over types in the types of constructors. Such quantification induces less-than constraints, while parameters only introduce less-than-or-equal-to constraints.
adamc@233	306
adam@343	307 Coq includes one more (potentially confusing) feature related to parameters. While Gallina does not support real %\index{universe polymorphism}%universe polymorphism, there is a convenience facility that mimics universe polymorphism in some cases. We can illustrate what this means with a simple example. *)
adamc@233	308
adamc@233	309 Inductive foo (A : Type) : Type :=
adamc@233	310 \| Foo : A -> foo A.
adamc@229	311
adamc@229	312 (* begin hide *)
adamc@229	313 Unset Printing Universes.
adamc@229	314 (* end hide *)
adamc@229	315
adamc@233	316 Check foo nat.
adamc@233	317 (** %\vspace{-.15in}% [[
adamc@233	318 foo nat
adamc@233	319 : Set
adam@302	320 ]]
adam@302	321 *)
adamc@233	322
adamc@233	323 Check foo Set.
adamc@233	324 (** %\vspace{-.15in}% [[
adamc@233	325 foo Set
adamc@233	326 : Type
adam@302	327 ]]
adam@302	328 *)
adamc@233	329
adamc@233	330 Check foo True.
adamc@233	331 (** %\vspace{-.15in}% [[
adamc@233	332 foo True
adamc@233	333 : Prop
adamc@233	334
adamc@233	335 ]]
adamc@233	336
adam@287	337 The basic pattern here is that Coq is willing to automatically build a %``%#"#copied-and-pasted#"#%''% version of an inductive definition, where some occurrences of [Type] have been replaced by [Set] or [Prop]. In each context, the type-checker tries to find the valid replacements that are lowest in the type hierarchy. Automatic cloning of definitions can be much more convenient than manual cloning. We have already taken advantage of the fact that we may re-use the same families of tuple and list types to form values in [Set] and [Type].
adamc@233	338
adamc@233	339 Imitation polymorphism can be confusing in some contexts. For instance, it is what is responsible for this weird behavior. *)
adamc@233	340
adamc@233	341 Inductive bar : Type := Bar : bar.
adamc@233	342
adamc@233	343 Check bar.
adamc@233	344 (** %\vspace{-.15in}% [[
adamc@233	345 bar
adamc@233	346 : Prop
adamc@233	347 ]]
adamc@233	348
adamc@233	349 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *)
adamc@233	350
adamc@229	351
adamc@229	352 (** * The [Prop] Universe *)
adamc@229	353
adam@287	354 (** In Chapter 4, we saw parallel versions of useful datatypes for %``%#"#programs#"#%''% and %``%#"#proofs.#"#%''% The convention was that programs live in [Set], and proofs live in [Prop]. We gave little explanation for why it is useful to maintain this distinction. There is certainly documentation value from separating programs from proofs; in practice, different concerns apply to building the two types of objects. It turns out, however, that these concerns motivate formal differences between the two universes in Coq.
adamc@229	355
adamc@229	356 Recall the types [sig] and [ex], which are the program and proof versions of existential quantification. Their definitions differ only in one place, where [sig] uses [Type] and [ex] uses [Prop]. *)
adamc@229	357
adamc@229	358 Print sig.
adamc@229	359 (** %\vspace{-.15in}% [[
adamc@229	360 Inductive sig (A : Type) (P : A -> Prop) : Type :=
adamc@229	361 exist : forall x : A, P x -> sig P
adam@302	362 ]]
adam@302	363 *)
adamc@229	364
adamc@229	365 Print ex.
adamc@229	366 (** %\vspace{-.15in}% [[
adamc@229	367 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
adamc@229	368 ex_intro : forall x : A, P x -> ex P
adamc@229	369 ]]
adamc@229	370
adamc@229	371 It is natural to want a function to extract the first components of data structures like these. Doing so is easy enough for [sig]. *)
adamc@229	372
adamc@229	373 Definition projS A (P : A -> Prop) (x : sig P) : A :=
adamc@229	374 match x with
adamc@229	375 \| exist v _ => v
adamc@229	376 end.
adamc@229	377
adamc@229	378 (** We run into trouble with a version that has been changed to work with [ex].
adamc@229	379 [[
adamc@229	380 Definition projE A (P : A -> Prop) (x : ex P) : A :=
adamc@229	381 match x with
adamc@229	382 \| ex_intro v _ => v
adamc@229	383 end.
adam@343	384 ]]
adamc@229	385
adam@343	386 <<
adamc@229	387 Error:
adamc@229	388 Incorrect elimination of "x" in the inductive type "ex":
adamc@229	389 the return type has sort "Type" while it should be "Prop".
adamc@229	390 Elimination of an inductive object of sort Prop
adamc@229	391 is not allowed on a predicate in sort Type
adamc@229	392 because proofs can be eliminated only to build proofs.
adam@343	393 >>
adamc@229	394
adam@343	395 In formal Coq parlance, %\index{elimination}``%#"#elimination#"#%''% means %``%#"#pattern-matching.#"#%''% The typing rules of Gallina forbid us from pattern-matching on a discriminee whose type belongs to [Prop], whenever the result type of the [match] has a type besides [Prop]. This is a sort of %``%#"#information flow#"#%''% policy, where the type system ensures that the details of proofs can never have any effect on parts of a development that are not also marked as proofs.
adamc@229	396
adamc@229	397 This restriction matches informal practice. We think of programs and proofs as clearly separated, and, outside of constructive logic, the idea of computing with proofs is ill-formed. The distinction also has practical importance in Coq, where it affects the behavior of extraction.
adamc@229	398
adam@343	399 Recall that %\index{program extraction}%extraction is Coq's facility for translating Coq developments into programs in general-purpose programming languages like OCaml. Extraction %\textit{%#<i>#erases#</i>#%}% proofs and leaves programs intact. A simple example with [sig] and [ex] demonstrates the distinction. *)
adamc@229	400
adamc@229	401 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) :=
adamc@229	402 match x with
adamc@229	403 \| exist n pf => exist _ n (sym_eq pf)
adamc@229	404 end.
adamc@229	405
adamc@229	406 Extraction sym_sig.
adamc@229	407 (** <<
adamc@229	408 ( val sym_sig : nat -> nat )
adamc@229	409
adamc@229	410 let sym_sig x = x
adamc@229	411 >>
adamc@229	412
adamc@229	413 Since extraction erases proofs, the second components of [sig] values are elided, making [sig] a simple identity type family. The [sym_sig] operation is thus an identity function. *)
adamc@229	414
adamc@229	415 Definition sym_ex (x : ex (fun n => n = 0)) : ex (fun n => 0 = n) :=
adamc@229	416 match x with
adamc@229	417 \| ex_intro n pf => ex_intro _ n (sym_eq pf)
adamc@229	418 end.
adamc@229	419
adamc@229	420 Extraction sym_ex.
adamc@229	421 (** <<
adamc@229	422 ( val sym_ex : __ )
adamc@229	423
adamc@229	424 let sym_ex = __
adamc@229	425 >>
adamc@229	426
adam@302	427 In this example, the [ex] type itself is in [Prop], so whole [ex] packages are erased. Coq extracts every proposition as the (Coq-specific) type %\texttt{\_\_}%#<tt>__</tt>#, whose single constructor is %\texttt{\_\_}%#<tt>__</tt>#. Not only are proofs replaced by [__], but proof arguments to functions are also removed completely, as we see here.
adamc@229	428
adam@343	429 Extraction is very helpful as an optimization over programs that contain proofs. In languages like Haskell, advanced features make it possible to program with proofs, as a way of convincing the type checker to accept particular definitions. Unfortunately, when proofs are encoded as values in GADTs%~\cite{GADT}%, these proofs exist at runtime and consume resources. In contrast, with Coq, as long as all proofs are kept within [Prop], extraction is guaranteed to erase them.
adamc@229	430
adam@343	431 Many fans of the %\index{Curry-Howard correspondence}%Curry-Howard correspondence support the idea of %\textit{%#<i>#extracting programs from proofs#</i>#%}%. In reality, few users of Coq and related tools do any such thing. Instead, extraction is better thought of as an optimization that reduces the runtime costs of expressive typing.
adamc@229	432
adamc@229	433 %\medskip%
adamc@229	434
adam@343	435 We have seen two of the differences between proofs and programs: proofs are subject to an elimination restriction and are elided by extraction. The remaining difference is that [Prop] is %\index{impredicativity}\textit{%#<i>#impredicative#</i>#%}%, as this example shows. *)
adamc@229	436
adamc@229	437 Check forall P Q : Prop, P \/ Q -> Q \/ P.
adamc@229	438 (** %\vspace{-.15in}% [[
adamc@229	439 forall P Q : Prop, P \/ Q -> Q \/ P
adamc@229	440 : Prop
adamc@229	441
adamc@229	442 ]]
adamc@229	443
adamc@230	444 We see that it is possible to define a [Prop] that quantifies over other [Prop]s. This is fortunate, as we start wanting that ability even for such basic purposes as stating propositional tautologies. In the next section of this chapter, we will see some reasons why unrestricted impredicativity is undesirable. The impredicativity of [Prop] interacts crucially with the elimination restriction to avoid those pitfalls.
adamc@230	445
adamc@230	446 Impredicativity also allows us to implement a version of our earlier [exp] type that does not suffer from the weakness that we found. *)
adamc@230	447
adamc@230	448 Inductive expP : Type -> Prop :=
adamc@230	449 \| ConstP : forall T, T -> expP T
adamc@230	450 \| PairP : forall T1 T2, expP T1 -> expP T2 -> expP (T1 * T2)
adamc@230	451 \| EqP : forall T, expP T -> expP T -> expP bool.
adamc@230	452
adamc@230	453 Check ConstP 0.
adamc@230	454 (** %\vspace{-.15in}% [[
adamc@230	455 ConstP 0
adamc@230	456 : expP nat
adam@302	457 ]]
adam@302	458 *)
adamc@230	459
adamc@230	460 Check PairP (ConstP 0) (ConstP tt).
adamc@230	461 (** %\vspace{-.15in}% [[
adamc@230	462 PairP (ConstP 0) (ConstP tt)
adamc@230	463 : expP (nat * unit)
adam@302	464 ]]
adam@302	465 *)
adamc@230	466
adamc@230	467 Check EqP (ConstP Set) (ConstP Type).
adamc@230	468 (** %\vspace{-.15in}% [[
adamc@230	469 EqP (ConstP Set) (ConstP Type)
adamc@230	470 : expP bool
adam@302	471 ]]
adam@302	472 *)
adamc@230	473
adamc@230	474 Check ConstP (ConstP O).
adamc@230	475 (** %\vspace{-.15in}% [[
adamc@230	476 ConstP (ConstP 0)
adamc@230	477 : expP (expP nat)
adamc@230	478
adamc@230	479 ]]
adamc@230	480
adam@287	481 In this case, our victory is really a shallow one. As we have marked [expP] as a family of proofs, we cannot deconstruct our expressions in the usual programmatic ways, which makes them almost useless for the usual purposes. Impredicative quantification is much more useful in defining inductive families that we really think of as judgments. For instance, this code defines a notion of equality that is strictly more permissive than the base equality [=]. *)
adamc@230	482
adamc@230	483 Inductive eqPlus : forall T, T -> T -> Prop :=
adamc@230	484 \| Base : forall T (x : T), eqPlus x x
adamc@230	485 \| Func : forall dom ran (f1 f2 : dom -> ran),
adamc@230	486 (forall x : dom, eqPlus (f1 x) (f2 x))
adamc@230	487 -> eqPlus f1 f2.
adamc@230	488
adamc@230	489 Check (Base 0).
adamc@230	490 (** %\vspace{-.15in}% [[
adamc@230	491 Base 0
adamc@230	492 : eqPlus 0 0
adam@302	493 ]]
adam@302	494 *)
adamc@230	495
adamc@230	496 Check (Func (fun n => n) (fun n => 0 + n) (fun n => Base n)).
adamc@230	497 (** %\vspace{-.15in}% [[
adamc@230	498 Func (fun n : nat => n) (fun n : nat => 0 + n) (fun n : nat => Base n)
adamc@230	499 : eqPlus (fun n : nat => n) (fun n : nat => 0 + n)
adam@302	500 ]]
adam@302	501 *)
adamc@230	502
adamc@230	503 Check (Base (Base 1)).
adamc@230	504 (** %\vspace{-.15in}% [[
adamc@230	505 Base (Base 1)
adamc@230	506 : eqPlus (Base 1) (Base 1)
adam@302	507 ]]
adam@302	508 *)
adamc@230	509
adam@343	510 (** Stating equality facts about proofs may seem baroque, but we have already seen its utility in the chapter on reasoning about equality proofs. *)
adam@343	511
adamc@230	512
adamc@230	513 (** * Axioms *)
adamc@230	514
adam@343	515 (** While the specific logic Gallina is hardcoded into Coq's implementation, it is possible to add certain logical rules in a controlled way. In other words, Coq may be used to reason about many different refinements of Gallina where strictly more theorems are provable. We achieve this by asserting %\index{axioms}\textit{%#<i>#axioms#</i>#%}% without proof.
adamc@230	516
adamc@230	517 We will motivate the idea by touring through some standard axioms, as enumerated in Coq's online FAQ. I will add additional commentary as appropriate. *)
adamc@230	518
adamc@230	519 ( The Basics *)
adamc@230	520
adam@343	521 (** One simple example of a useful axiom is the %\index{law of the excluded middle}%law of the excluded middle. *)
adamc@230	522
adamc@230	523 Require Import Classical_Prop.
adamc@230	524 Print classic.
adamc@230	525 (** %\vspace{-.15in}% [[
adamc@230	526 *** [ classic : forall P : Prop, P \/ ~ P ]
adamc@230	527 ]]
adamc@230	528
adam@343	529 In the implementation of module [Classical_Prop], this axiom was defined with the command%\index{Vernacular commands!Axiom}% *)
adamc@230	530
adamc@230	531 Axiom classic : forall P : Prop, P \/ ~ P.
adamc@230	532
adam@343	533 (** An [Axiom] may be declared with any type, in any of the universes. There is a synonym %\index{Vernacular commands!Parameter}%[Parameter] for [Axiom], and that synonym is often clearer for assertions not of type [Prop]. For instance, we can assert the existence of objects with certain properties. *)
adamc@230	534
adamc@230	535 Parameter n : nat.
adamc@230	536 Axiom positive : n > 0.
adamc@230	537 Reset n.
adamc@230	538
adam@287	539 (** This kind of %``%#"#axiomatic presentation#"#%''% of a theory is very common outside of higher-order logic. However, in Coq, it is almost always preferable to stick to defining your objects, functions, and predicates via inductive definitions and functional programming.
adamc@230	540
adam@343	541 In general, there is a significant burden associated with any use of axioms. It is easy to assert a set of axioms that together is %\index{inconsistent axioms}\textit{%#<i>#inconsistent#</i>#%}%. That is, a set of axioms may imply [False], which allows any theorem to proved, which defeats the purpose of a proof assistant. For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *)
adamc@230	542
adam@287	543 Axiom not_classic : ~ forall P : Prop, P \/ ~ P.
adamc@230	544
adamc@230	545 Theorem uhoh : False.
adam@287	546 generalize classic not_classic; tauto.
adamc@230	547 Qed.
adamc@230	548
adamc@230	549 Theorem uhoh_again : 1 + 1 = 3.
adamc@230	550 destruct uhoh.
adamc@230	551 Qed.
adamc@230	552
adamc@230	553 Reset not_classic.
adamc@230	554
adam@343	555 (** On the subject of the law of the excluded middle itself, this axiom is usually quite harmless, and many practical Coq developments assume it. It has been proved metatheoretically to be consistent with CIC. Here, %``%#"#proved metatheoretically#"#%''% means that someone proved on paper that excluded middle holds in a %\textit{%#<i>#model#</i>#%}% of CIC in set theory%~\cite{SetsInTypes}%. All of the other axioms that we will survey in this section hold in the same model, so they are all consistent together.
adamc@230	556
adam@343	557 Recall that Coq implements %\index{constructive logic}\textit{%#<i>#constructive#</i>#%}% logic by default, where excluded middle is not provable. Proofs in constructive logic can be thought of as programs. A [forall] quantifier denotes a dependent function type, and a disjunction denotes a variant type. In such a setting, excluded middle could be interpreted as a decision procedure for arbitrary propositions, which computability theory tells us cannot exist. Thus, constructive logic with excluded middle can no longer be associated with our usual notion of programming.
adamc@230	558
adamc@231	559 Given all this, why is it all right to assert excluded middle as an axiom? The intuitive justification is that the elimination restriction for [Prop] prevents us from treating proofs as programs. An excluded middle axiom that quantified over [Set] instead of [Prop] %\textit{%#<i>#would#</i>#%}% be problematic. If a development used that axiom, we would not be able to extract the code to OCaml (soundly) without implementing a genuine universal decision procedure. In contrast, values whose types belong to [Prop] are always erased by extraction, so we sidestep the axiom's algorithmic consequences.
adamc@230	560
adam@343	561 Because the proper use of axioms is so precarious, there are helpful commands for determining which axioms a theorem relies on.%\index{Vernacular commands!Print Assumptions}% *)
adamc@230	562
adamc@230	563 Theorem t1 : forall P : Prop, P -> ~ ~ P.
adamc@230	564 tauto.
adamc@230	565 Qed.
adamc@230	566
adamc@230	567 Print Assumptions t1.
adam@343	568 (** <<
adamc@230	569 Closed under the global context
adam@343	570 >>
adam@302	571 *)
adamc@230	572
adamc@230	573 Theorem t2 : forall P : Prop, ~ ~ P -> P.
adamc@230	574 (** [[
adamc@230	575 tauto.
adam@343	576 ]]
adam@343	577 <<
adamc@230	578 Error: tauto failed.
adam@343	579 >>
adam@302	580 *)
adamc@230	581 intro P; destruct (classic P); tauto.
adamc@230	582 Qed.
adamc@230	583
adamc@230	584 Print Assumptions t2.
adamc@230	585 (** %\vspace{-.15in}% [[
adamc@230	586 Axioms:
adamc@230	587 classic : forall P : Prop, P \/ ~ P
adamc@230	588 ]]
adamc@230	589
adamc@231	590 It is possible to avoid this dependence in some specific cases, where excluded middle %\textit{%#<i>#is#</i>#%}% provable, for decidable families of propositions. *)
adamc@230	591
adam@287	592 Theorem nat_eq_dec : forall n m : nat, n = m \/ n <> m.
adamc@230	593 induction n; destruct m; intuition; generalize (IHn m); intuition.
adamc@230	594 Qed.
adamc@230	595
adamc@230	596 Theorem t2' : forall n m : nat, ~ ~ (n = m) -> n = m.
adam@287	597 intros n m; destruct (nat_eq_dec n m); tauto.
adamc@230	598 Qed.
adamc@230	599
adamc@230	600 Print Assumptions t2'.
adam@343	601 (** <<
adamc@230	602 Closed under the global context
adam@343	603 >>
adamc@230	604
adamc@230	605 %\bigskip%
adamc@230	606
adam@343	607 Mainstream mathematical practice assumes excluded middle, so it can be useful to have it available in Coq developments, though it is also nice to know that a theorem is proved in a simpler formal system than classical logic. There is a similar story for %\index{proof irrelevance}\textit{%#<i>#proof irrelevance#</i>#%}%, which simplifies proof issues that would not even arise in mainstream math. *)
adamc@230	608
adamc@230	609 Require Import ProofIrrelevance.
adamc@230	610 Print proof_irrelevance.
adamc@230	611 (** %\vspace{-.15in}% [[
adamc@230	612 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ]
adamc@230	613 ]]
adamc@230	614
adam@350	615 This axiom asserts that any two proofs of the same proposition are equal. If we replaced [p1 = p2] by [p1 <-> p2], then the statement would be provable. However, equality is a stronger notion than logical equivalence. Recall this example function from Chapter 7. *)
adamc@230	616
adamc@230	617 (* begin hide *)
adamc@230	618 Lemma zgtz : 0 > 0 -> False.
adamc@230	619 crush.
adamc@230	620 Qed.
adamc@230	621 (* end hide *)
adamc@230	622
adamc@230	623 Definition pred_strong1 (n : nat) : n > 0 -> nat :=
adamc@230	624 match n with
adamc@230	625 \| O => fun pf : 0 > 0 => match zgtz pf with end
adamc@230	626 \| S n' => fun _ => n'
adamc@230	627 end.
adamc@230	628
adam@343	629 (** We might want to prove that different proofs of [n > 0] do not lead to different results from our richly typed predecessor function. *)
adamc@230	630
adamc@230	631 Theorem pred_strong1_irrel : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
adamc@230	632 destruct n; crush.
adamc@230	633 Qed.
adamc@230	634
adamc@230	635 (** The proof script is simple, but it involved peeking into the definition of [pred_strong1]. For more complicated function definitions, it can be considerably more work to prove that they do not discriminate on details of proof arguments. This can seem like a shame, since the [Prop] elimination restriction makes it impossible to write any function that does otherwise. Unfortunately, this fact is only true metatheoretically, unless we assert an axiom like [proof_irrelevance]. With that axiom, we can prove our theorem without consulting the definition of [pred_strong1]. *)
adamc@230	636
adamc@230	637 Theorem pred_strong1_irrel' : forall n (pf1 pf2 : n > 0), pred_strong1 pf1 = pred_strong1 pf2.
adamc@230	638 intros; f_equal; apply proof_irrelevance.
adamc@230	639 Qed.
adamc@230	640
adamc@230	641
adamc@230	642 (** %\bigskip%
adamc@230	643
adamc@230	644 In the chapter on equality, we already discussed some axioms that are related to proof irrelevance. In particular, Coq's standard library includes this axiom: *)
adamc@230	645
adamc@230	646 Require Import Eqdep.
adamc@230	647 Import Eq_rect_eq.
adamc@230	648 Print eq_rect_eq.
adamc@230	649 (** %\vspace{-.15in}% [[
adamc@230	650 *** [ eq_rect_eq :
adamc@230	651 forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adamc@230	652 x = eq_rect p Q x p h ]
adamc@230	653 ]]
adamc@230	654
adam@343	655 This axiom says that it is permissible to simplify pattern matches over proofs of equalities like [e = e]. The axiom is logically equivalent to some simpler corollaries. In the theorem names, %``%#"#UIP#"#%''% stands for %\index{unicity of identity proofs}``%#"#unicity of identity proofs#"#%''%, where %``%#"#identity#"#%''% is a synonym for %``%#"#equality.#"#%''% *)
adamc@230	656
adamc@230	657 Corollary UIP_refl : forall A (x : A) (pf : x = x), pf = refl_equal x.
adamc@230	658 intros; replace pf with (eq_rect x (eq x) (refl_equal x) x pf); [
adamc@230	659 symmetry; apply eq_rect_eq
adamc@230	660 \| exact (match pf as pf' return match pf' in _ = y return x = y with
adamc@230	661 \| refl_equal => refl_equal x
adamc@230	662 end = pf' with
adamc@230	663 \| refl_equal => refl_equal _
adamc@230	664 end) ].
adamc@230	665 Qed.
adamc@230	666
adamc@230	667 Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2.
adamc@230	668 intros; generalize pf1 pf2; subst; intros;
adamc@230	669 match goal with
adamc@230	670 \| [ \|- ?pf1 = ?pf2 ] => rewrite (UIP_refl pf1); rewrite (UIP_refl pf2); reflexivity
adamc@230	671 end.
adamc@230	672 Qed.
adamc@230	673
adamc@231	674 (** These corollaries are special cases of proof irrelevance. In developments that only need proof irrelevance for equality, there is no need to assert full irrelevance.
adamc@230	675
adamc@230	676 Another facet of proof irrelevance is that, like excluded middle, it is often provable for specific propositions. For instance, [UIP] is provable whenever the type [A] has a decidable equality operation. The module [Eqdep_dec] of the standard library contains a proof. A similar phenomenon applies to other notable cases, including less-than proofs. Thus, it is often possible to use proof irrelevance without asserting axioms.
adamc@230	677
adamc@230	678 %\bigskip%
adamc@230	679
adamc@230	680 There are two more basic axioms that are often assumed, to avoid complications that do not arise in set theory. *)
adamc@230	681
adamc@230	682 Require Import FunctionalExtensionality.
adamc@230	683 Print functional_extensionality_dep.
adamc@230	684 (** %\vspace{-.15in}% [[
adamc@230	685 *** [ functional_extensionality_dep :
adamc@230	686 forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
adamc@230	687 (forall x : A, f x = g x) -> f = g ]
adamc@230	688
adamc@230	689 ]]
adamc@230	690
adamc@230	691 This axiom says that two functions are equal if they map equal inputs to equal outputs. Such facts are not provable in general in CIC, but it is consistent to assume that they are.
adamc@230	692
adam@343	693 A simple corollary shows that the same property applies to predicates. *)
adamc@230	694
adamc@230	695 Corollary predicate_extensionality : forall (A : Type) (B : A -> Prop) (f g : forall x : A, B x),
adamc@230	696 (forall x : A, f x = g x) -> f = g.
adamc@230	697 intros; apply functional_extensionality_dep; assumption.
adamc@230	698 Qed.
adamc@230	699
adam@343	700 (** In some cases, one might prefer to assert this corollary as the axiom, to restrict the consequences to proofs and not programs. *)
adam@343	701
adamc@230	702
adamc@230	703 ( Axioms of Choice *)
adamc@230	704
adam@343	705 (** Some Coq axioms are also points of contention in mainstream math. The most prominent example is the %\index{axiom of choice}%axiom of choice. In fact, there are multiple versions that we might consider, and, considered in isolation, none of these versions means quite what it means in classical set theory.
adamc@230	706
adamc@230	707 First, it is possible to implement a choice operator %\textit{%#<i>#without#</i>#%}% axioms in some potentially surprising cases. *)
adamc@230	708
adamc@230	709 Require Import ConstructiveEpsilon.
adamc@230	710 Check constructive_definite_description.
adamc@230	711 (** %\vspace{-.15in}% [[
adamc@230	712 constructive_definite_description
adamc@230	713 : forall (A : Set) (f : A -> nat) (g : nat -> A),
adamc@230	714 (forall x : A, g (f x) = x) ->
adamc@230	715 forall P : A -> Prop,
adamc@230	716 (forall x : A, {P x} + {~ P x}) ->
adamc@230	717 (exists! x : A, P x) -> {x : A \| P x}
adam@302	718 ]]
adam@302	719 *)
adamc@230	720
adamc@230	721 Print Assumptions constructive_definite_description.
adam@343	722 (** <<
adamc@230	723 Closed under the global context
adam@343	724 >>
adamc@230	725
adamc@231	726 This function transforms a decidable predicate [P] into a function that produces an element satisfying [P] from a proof that such an element exists. The functions [f] and [g], in conjunction with an associated injectivity property, are used to express the idea that the set [A] is countable. Under these conditions, a simple brute force algorithm gets the job done: we just enumerate all elements of [A], stopping when we find one satisfying [P]. The existence proof, specified in terms of %\textit{%#<i>#unique#</i>#%}% existence [exists!], guarantees termination. The definition of this operator in Coq uses some interesting techniques, as seen in the implementation of the [ConstructiveEpsilon] module.
adamc@230	727
adamc@230	728 Countable choice is provable in set theory without appealing to the general axiom of choice. To support the more general principle in Coq, we must also add an axiom. Here is a functional version of the axiom of unique choice. *)
adamc@230	729
adamc@230	730 Require Import ClassicalUniqueChoice.
adamc@230	731 Check dependent_unique_choice.
adamc@230	732 (** %\vspace{-.15in}% [[
adamc@230	733 dependent_unique_choice
adamc@230	734 : forall (A : Type) (B : A -> Type) (R : forall x : A, B x -> Prop),
adamc@230	735 (forall x : A, exists! y : B x, R x y) ->
adam@343	736 exists f : forall x : A, B x,
adam@343	737 forall x : A, R x (f x)
adamc@230	738 ]]
adamc@230	739
adamc@230	740 This axiom lets us convert a relational specification [R] into a function implementing that specification. We need only prove that [R] is truly a function. An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs. We also simplify the statement of the theorem by considering only non-dependent function types. *)
adamc@230	741
adamc@230	742 Require Import ClassicalChoice.
adamc@230	743 Check choice.
adamc@230	744 (** %\vspace{-.15in}% [[
adamc@230	745 choice
adamc@230	746 : forall (A B : Type) (R : A -> B -> Prop),
adamc@230	747 (forall x : A, exists y : B, R x y) ->
adamc@230	748 exists f : A -> B, forall x : A, R x (f x)
adamc@230	749
adamc@230	750 ]]
adamc@230	751
adamc@230	752 This principle is proved as a theorem, based on the unique choice axiom and an additional axiom of relational choice from the [RelationalChoice] module.
adamc@230	753
adamc@230	754 In set theory, the axiom of choice is a fundamental philosophical commitment one makes about the universe of sets. In Coq, the choice axioms say something weaker. For instance, consider the simple restatement of the [choice] axiom where we replace existential quantification by its Curry-Howard analogue, subset types. *)
adamc@230	755
adamc@230	756 Definition choice_Set (A B : Type) (R : A -> B -> Prop) (H : forall x : A, {y : B \| R x y})
adamc@230	757 : {f : A -> B \| forall x : A, R x (f x)} :=
adamc@230	758 exist (fun f => forall x : A, R x (f x))
adamc@230	759 (fun x => proj1_sig (H x)) (fun x => proj2_sig (H x)).
adamc@230	760
adam@287	761 (** Via the Curry-Howard correspondence, this %``%#"#axiom#"#%''% can be taken to have the same meaning as the original. It is implemented trivially as a transformation not much deeper than uncurrying. Thus, we see that the utility of the axioms that we mentioned earlier comes in their usage to build programs from proofs. Normal set theory has no explicit proofs, so the meaning of the usual axiom of choice is subtlely different. In Gallina, the axioms implement a controlled relaxation of the restrictions on information flow from proofs to programs.
adamc@230	762
adam@287	763 However, when we combine an axiom of choice with the law of the excluded middle, the idea of %``%#"#choice#"#%''% becomes more interesting. Excluded middle gives us a highly non-computational way of constructing proofs, but it does not change the computational nature of programs. Thus, the axiom of choice is still giving us a way of translating between two different sorts of %``%#"#programs,#"#%''% but the input programs (which are proofs) may be written in a rich language that goes beyond normal computability. This truly is more than repackaging a function with a different type.
adamc@230	764
adamc@230	765 %\bigskip%
adamc@230	766
adam@343	767 The Coq tools support a command-line flag %\index{impredicative Set}\texttt{%#<tt>#-impredicative-set#</tt>#%}%, which modifies Gallina in a more fundamental way by making [Set] impredicative. A term like [forall T : Set, T] has type [Set], and inductive definitions in [Set] may have constructors that quantify over arguments of any types. To maintain consistency, an elimination restriction must be imposed, similarly to the restriction for [Prop]. The restriction only applies to large inductive types, where some constructor quantifies over a type of type [Type]. In such cases, a value in this inductive type may only be pattern-matched over to yield a result type whose type is [Set] or [Prop]. This contrasts with [Prop], where the restriction applies even to non-large inductive types, and where the result type may only have type [Prop].
adamc@230	768
adamc@230	769 In old versions of Coq, [Set] was impredicative by default. Later versions make [Set] predicative to avoid inconsistency with some classical axioms. In particular, one should watch out when using impredicative [Set] with axioms of choice. In combination with excluded middle or predicate extensionality, this can lead to inconsistency. Impredicative [Set] can be useful for modeling inherently impredicative mathematical concepts, but almost all Coq developments get by fine without it. *)
adamc@230	770
adamc@230	771 ( Axioms and Computation *)
adamc@230	772
adamc@230	773 (** One additional axiom-related wrinkle arises from an aspect of Gallina that is very different from set theory: a notion of %\textit{%#<i>#computational equivalence#</i>#%}% is central to the definition of the formal system. Axioms tend not to play well with computation. Consider this example. We start by implementing a function that uses a type equality proof to perform a safe type-cast. *)
adamc@230	774
adamc@230	775 Definition cast (x y : Set) (pf : x = y) (v : x) : y :=
adamc@230	776 match pf with
adamc@230	777 \| refl_equal => v
adamc@230	778 end.
adamc@230	779
adamc@230	780 (** Computation over programs that use [cast] can proceed smoothly. *)
adamc@230	781
adamc@230	782 Eval compute in (cast (refl_equal (nat -> nat)) (fun n => S n)) 12.
adam@343	783 (** %\vspace{-.15in}%[[
adamc@230	784 = 13
adamc@230	785 : nat
adam@302	786 ]]
adam@302	787 *)
adamc@230	788
adamc@230	789 (** Things do not go as smoothly when we use [cast] with proofs that rely on axioms. *)
adamc@230	790
adamc@230	791 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
adamc@230	792 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
adamc@230	793 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
adamc@230	794 Qed.
adamc@230	795
adamc@230	796 Eval compute in (cast t3 (fun _ => First)) 12.
adamc@230	797 (** [[
adamc@230	798 = match t3 in (_ = P) return P with
adamc@230	799 \| refl_equal => fun n : nat => First
adamc@230	800 end 12
adamc@230	801 : fin (12 + 1)
adamc@230	802 ]]
adamc@230	803
adamc@230	804 Computation gets stuck in a pattern-match on the proof [t3]. The structure of [t3] is not known, so the match cannot proceed. It turns out a more basic problem leads to this particular situation. We ended the proof of [t3] with [Qed], so the definition of [t3] is not available to computation. That is easily fixed. *)
adamc@230	805
adamc@230	806 Reset t3.
adamc@230	807
adamc@230	808 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
adamc@230	809 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
adamc@230	810 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
adamc@230	811 Defined.
adamc@230	812
adamc@230	813 Eval compute in (cast t3 (fun _ => First)) 12.
adamc@230	814 (** [[
adamc@230	815 = match
adamc@230	816 match
adamc@230	817 match
adamc@230	818 functional_extensionality
adamc@230	819 ....
adamc@230	820 ]]
adamc@230	821
adamc@230	822 We elide most of the details. A very unwieldy tree of nested matches on equality proofs appears. This time evaluation really %\textit{%#<i>#is#</i>#%}% stuck on a use of an axiom.
adamc@230	823
adamc@230	824 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *)
adamc@230	825
adamc@230	826 Lemma plus1 : forall n, S n = n + 1.
adamc@230	827 induction n; simpl; intuition.
adamc@230	828 Defined.
adamc@230	829
adamc@230	830 Theorem t4 : forall n, fin (S n) = fin (n + 1).
adamc@230	831 intro; f_equal; apply plus1.
adamc@230	832 Defined.
adamc@230	833
adamc@230	834 Eval compute in cast (t4 13) First.
adamc@230	835 (** %\vspace{-.15in}% [[
adamc@230	836 = First
adamc@230	837 : fin (13 + 1)
adam@302	838 ]]
adam@343	839
adam@343	840 This simple computational reduction hides the use of a recursive function to produce a suitable [refl_equal] proof term. The recursion originates in our use of [induction] in [t4]'s proof. *)
adam@343	841
adam@344	842
adam@344	843 ( Methods for Avoiding Axioms *)
adam@344	844
adam@344	845 (** The last section demonstrated one reason to avoid axioms: they interfere with computational behavior of terms. A further reason is to reduce the philosophical commitment of a theorem. The more axioms one assumes, the harder it becomes to convince oneself that the formal system corresponds appropriately to one's intuitions. A refinement of this last point, in applications like %\index{proof-carrying code}%proof-carrying code%~\cite{PCC}% in computer security, has to do with minimizing the size of a %\index{trusted code base}\emph{%#<i>#trusted code base#</i>#%}%. To convince ourselves that a theorem is true, we must convince ourselves of the correctness of the program that checks the theorem. Axioms effectively become new source code for the checking program, increasing the effort required to perform a correctness audit.
adam@344	846
adam@344	847 An earlier section gave one example of avoiding an axiom. We proved that [pred_strong1] is agnostic to details of the proofs passed to it as arguments, by unfolding the definition of the function. A %``%#"#simpler#"#%''% proof keeps the function definition opaque and instead applies a proof irrelevance axiom. By accepting a more complex proof, we reduce our philosophical commitment and trusted base. (By the way, the less-than relation that the proofs in question here prove turns out to admit proof irrelevance as a theorem provable within normal Gallina!)
adam@344	848
adam@344	849 One dark secret of the [dep_destruct] tactic that we have used several times is reliance on an axiom. Consider this simple case analysis principle for [fin] values: *)
adam@344	850
adam@344	851 Theorem fin_cases : forall n (f : fin (S n)), f = First \/ exists f', f = Next f'.
adam@344	852 intros; dep_destruct f; eauto.
adam@344	853 Qed.
adam@344	854
adam@344	855 Print Assumptions fin_cases.
adam@344	856 (** %\vspace{-.15in}%[[
adam@344	857 Axioms:
adam@344	858 JMeq.JMeq_eq : forall (A : Type) (x y : A), JMeq.JMeq x y -> x = y
adam@344	859 ]]
adam@344	860
adam@344	861 The proof depends on the [JMeq_eq] axiom that we met in the chapter on equality proofs. However, a smarter tactic could have avoided an axiom dependence. Here is an alternate proof via a slightly strange looking lemma. *)
adam@344	862
adam@344	863 (* begin thide *)
adam@344	864 Lemma fin_cases_again' : forall n (f : fin n),
adam@344	865 match n return fin n -> Prop with
adam@344	866 \| O => fun _ => False
adam@344	867 \| S n' => fun f => f = First \/ exists f', f = Next f'
adam@344	868 end f.
adam@344	869 destruct f; eauto.
adam@344	870 Qed.
adam@344	871
adam@344	872 (** We apply a variant of the %\index{convoy pattern}%convoy pattern, which we are used to seeing in function implementations. Here, the pattern helps us state a lemma in a form where the argument to [fin] is a variable. Recall that, thanks to basic typing rules for pattern-matching, [destruct] will only work effectively on types whose non-parameter arguments are variables. The %\index{tactics!exact}%[exact] tactic, which takes as argument a literal proof term, now gives us an easy way of proving the original theorem. *)
adam@344	873
adam@344	874 Theorem fin_cases_again : forall n (f : fin (S n)), f = First \/ exists f', f = Next f'.
adam@344	875 intros; exact (fin_cases_again' f).
adam@344	876 Qed.
adam@344	877 (* end thide *)
adam@344	878
adam@344	879 Print Assumptions fin_cases_again.
adam@344	880 (** %\vspace{-.15in}%
adam@344	881 <<
adam@344	882 Closed under the global context
adam@344	883 >>
adam@344	884
adam@345	885 *)
adam@345	886
adam@345	887 (* begin thide *)
adam@345	888 (** 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	889
adam@345	890 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	891
adam@345	892 Definition finOut n (f : fin n) : match n return fin n -> Type with
adam@345	893 \| O => fun _ => Empty_set
adam@345	894 \| _ => fun f => {f' : _ \| f = Next f'} + {f = First}
adam@345	895 end f :=
adam@345	896 match f with
adam@345	897 \| First _ => inright _ (refl_equal _)
adam@345	898 \| Next _ f' => inleft _ (exist _ f' (refl_equal _))
adam@345	899 end.
adam@345	900 (* end thide *)
adam@345	901
adam@345	902 (** 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	903
adam@344	904 Inductive formula : list Type -> Type :=
adam@344	905 \| Inject : forall Ts, Prop -> formula Ts
adam@344	906 \| VarEq : forall T Ts, T -> formula (T :: Ts)
adam@344	907 \| Lift : forall T Ts, formula Ts -> formula (T :: Ts)
adam@344	908 \| Forall : forall T Ts, formula (T :: Ts) -> formula Ts
adam@344	909 \| And : forall Ts, formula Ts -> formula Ts -> formula Ts.
adam@344	910
adam@344	911 (** 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	912
adam@344	913 Inductive proof : formula nil -> Prop :=
adam@344	914 \| PInject : forall (P : Prop), P -> proof (Inject nil P)
adam@344	915 \| PAnd : forall p q, proof p -> proof q -> proof (And p q).
adam@344	916
adam@344	917 (** Let us prove a lemma showing that a %``%#"#[P /\ Q -> P]#"#%''% rule is derivable within the rules of [proof]. *)
adam@344	918
adam@344	919 Theorem proj1 : forall p q, proof (And p q) -> proof p.
adam@344	920 destruct 1.
adam@344	921 (** %\vspace{-.15in}%[[
adam@344	922 p : formula nil
adam@344	923 q : formula nil
adam@344	924 P : Prop
adam@344	925 H : P
adam@344	926 ============================
adam@344	927 proof p
adam@344	928 ]]
adam@344	929 *)
adam@344	930
adam@344	931 (** 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	932
adam@344	933 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	934
adam@344	935 Restart.
adam@344	936 Require Import Program.
adam@344	937 intros ? ? H; dependent destruction H; auto.
adam@344	938 Qed.
adam@344	939
adam@344	940 Print Assumptions proj1.
adam@344	941 (** %\vspace{-.15in}%[[
adam@344	942 Axioms:
adam@344	943 eq_rect_eq : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@344	944 x = eq_rect p Q x p h
adam@344	945 ]]
adam@344	946
adam@344	947 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	948
adam@344	949 Lemma proj1_again' : forall r, proof r
adam@344	950 -> forall p q, r = And p q -> proof p.
adam@344	951 destruct 1; crush.
adam@344	952 (** %\vspace{-.15in}%[[
adam@344	953 H0 : Inject [] P = And p q
adam@344	954 ============================
adam@344	955 proof p
adam@344	956 ]]
adam@344	957
adam@344	958 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *)
adam@344	959
adam@344	960 discriminate.
adam@344	961 (** %\vspace{-.15in}%[[
adam@344	962 H : proof p
adam@344	963 H1 : And p q = And p0 q0
adam@344	964 ============================
adam@344	965 proof p0
adam@344	966 ]]
adam@344	967
adam@344	968 It looks like we are almost done. Hypothesis [H1] gives [p = p0] by injectivity of constructors, and then [H] finishes the case. *)
adam@344	969
adam@344	970 injection H1; intros.
adam@344	971
adam@344	972 (** Unfortunately, the %``%#"#equality#"#%''% that we expected between [p] and [p0] comes in a strange form:
adam@344	973
adam@344	974 [[
adam@344	975 H3 : existT (fun Ts : list Type => formula Ts) []%list p =
adam@344	976 existT (fun Ts : list Type => formula Ts) []%list p0
adam@344	977 ============================
adam@344	978 proof p0
adam@344	979 ]]
adam@344	980
adam@345	981 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	982
adam@344	983 How exactly does an axiom come into the picture here? Let us ask [crush] to finish the proof. *)
adam@344	984
adam@344	985 crush.
adam@344	986 Qed.
adam@344	987
adam@344	988 Print Assumptions proj1_again'.
adam@344	989 (** %\vspace{-.15in}%[[
adam@344	990 Axioms:
adam@344	991 eq_rect_eq : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
adam@344	992 x = eq_rect p Q x p h
adam@344	993 ]]
adam@344	994
adam@344	995 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	996
adam@344	997 Hope is not lost, however. We can produce an even stranger looking lemma, which gives us the theorem without axioms. *)
adam@344	998
adam@344	999 Lemma proj1_again'' : forall r, proof r
adam@344	1000 -> match r with
adam@344	1001 \| And Ps p _ => match Ps return formula Ps -> Prop with
adam@344	1002 \| nil => fun p => proof p
adam@344	1003 \| _ => fun _ => True
adam@344	1004 end p
adam@344	1005 \| _ => True
adam@344	1006 end.
adam@344	1007 destruct 1; auto.
adam@344	1008 Qed.
adam@344	1009
adam@344	1010 Theorem proj1_again : forall p q, proof (And p q) -> proof p.
adam@344	1011 intros ? ? H; exact (proj1_again'' H).
adam@344	1012 Qed.
adam@344	1013
adam@344	1014 Print Assumptions proj1_again.
adam@344	1015 (** <<
adam@344	1016 Closed under the global context
adam@344	1017 >>
adam@344	1018
adam@344	1019 This example illustrates again how some of the same design patterns we learned for dependently typed programming can be used fruitfully in theorem statements. *)

Mercurial > cpdt > repo

annotate src/Universes.v @ 350:ad315efc3b6b