comparison src/Universes.v @ 398:05efde66559d

Get it working in Coq 8.4beta1; use nice coqdoc notation for italics
author Adam Chlipala <adam@chlipala.net>
date Wed, 06 Jun 2012 11:25:13 -0400
parents 4b1242b277b2
children 934945edc6b5
comparison
equal deleted inserted replaced
397:d62ed7381a0b 398:05efde66559d
13 Require Import DepList CpdtTactics. 13 Require Import DepList CpdtTactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 (** printing $ %({}*% #(<a/>*# *)
19 (** printing ^ %*{})% #*<a/>)# *)
20
21
18 22
19 (** %\chapter{Universes and Axioms}% *) 23 (** %\chapter{Universes and Axioms}% *)
20 24
21 (** 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. 25 (** 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.
22 26
50 Set 54 Set
51 : Type 55 : Type
52 56
53 ]] 57 ]]
54 58
55 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]. *) 59 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]. *)
56 60
57 Check Type. 61 Check Type.
58 (** %\vspace{-.15in}% [[ 62 (** %\vspace{-.15in}% [[
59 Type 63 Type
60 : Type 64 : Type
70 Check nat. 74 Check nat.
71 (** %\vspace{-.15in}% [[ 75 (** %\vspace{-.15in}% [[
72 nat 76 nat
73 : Set 77 : Set
74 ]] 78 ]]
75 *) 79 *)
76
77 (** printing $ %({}*% #(<a/>*# *)
78 (** printing ^ %*{})% #*<a/>)# *)
79 80
80 Check Set. 81 Check Set.
81 (** %\vspace{-.15in}% [[ 82 (** %\vspace{-.15in}% [[
82 Set 83 Set
83 : Type $ (0)+1 ^ 84 : Type $ (0)+1 ^
92 93
93 ]] 94 ]]
94 95
95 Occurrences of [Type] are annotated with some additional information, inside comments. These annotations have to do with the secret behind [Type]: it really stands for an infinite hierarchy of types. The type of [Set] is [Type(0)], the type of [Type(0)] is [Type(1)], the type of [Type(1)] is [Type(2)], and so on. This is how we avoid the %``%#"#[Type : Type]#"#%''% paradox. As a convenience, the universe hierarchy drives Coq's one variety of subtyping. Any term whose type is [Type] at level [i] is automatically also described by [Type] at level [j] when [j > i]. 96 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].
96 97
97 In the outputs of our first [Check] query, we see that the type level of [Set]'s type is [(0)+1]. Here [0] stands for the level of [Set], and we increment it to arrive at the level that %\textit{%#<i>#classifies#</i>#%}% [Set]. 98 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].
98 99
99 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. 100 In the second 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.
100 101
101 Another crucial concept in CIC is %\index{predicativity}\textit{%#<i>#predicativity#</i>#%}%. Consider these queries. *) 102 Another crucial concept in CIC is %\index{predicativity}%_predicativity_. Consider these queries. *)
102 103
103 Check forall T : nat, fin T. 104 Check forall T : nat, fin T.
104 (** %\vspace{-.15in}% [[ 105 (** %\vspace{-.15in}% [[
105 forall T : nat, fin T 106 forall T : nat, fin T
106 : Set 107 : Set
173 174
174 << 175 <<
175 Error: Universe inconsistency (cannot enforce Top.16 < Top.16). 176 Error: Universe inconsistency (cannot enforce Top.16 < Top.16).
176 >> 177 >>
177 178
178 %\index{universe inconsistency}%This error message reminds us that the universe variable for [T] still exists, even though it is usually hidden. To apply [id] to itself, that variable would need to be less than itself in the type hierarchy. Universe inconsistency error messages announce cases like this one where a term could only type-check by violating an implied constraint over universe variables. Such errors demonstrate that [Type] is %\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. *) 179 %\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, 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. *)
179 180
180 181
181 (** ** Inductive Definitions *) 182 (** ** Inductive Definitions *)
182 183
183 (** Predicativity restrictions also apply to inductive definitions. As an example, let us consider a type of expression trees that allows injection of any native Coq value. The idea is that an [exp T] stands for a reflected expression of type [T]. 184 (** 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].
191 192
192 << 193 <<
193 Error: Large non-propositional inductive types must be in Type. 194 Error: Large non-propositional inductive types must be in Type.
194 >> 195 >>
195 196
196 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. *) 197 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. *)
197 198
198 Inductive exp : Type -> Type := 199 Inductive exp : Type -> Type :=
199 | Const : forall T, T -> exp T 200 | Const : forall T, T -> exp T
200 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) 201 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
201 | Eq : forall T, exp T -> exp T -> exp bool. 202 | Eq : forall T, exp T -> exp T -> exp bool.
248 exp T1 -> exp T2 -> exp (T1 * T2) 249 exp T1 -> exp T2 -> exp (T1 * T2)
249 | Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool 250 | Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool
250 251
251 ]] 252 ]]
252 253
253 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. 254 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] _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.
254 255
255 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}% *) 256 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}% *)
256 257
257 Print Universes. 258 Print Universes.
258 (** %\vspace{-.15in}% [[ 259 (** %\vspace{-.15in}% [[
280 281
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. 282 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.
282 283
283 %\medskip% 284 %\medskip%
284 285
285 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. 286 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 _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.
286 287
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. *) 288 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. *)
288 289
289 Check (nat, (Type, Set)). 290 Check (nat, (Type, Set)).
290 (** %\vspace{-.15in}% [[ 291 (** %\vspace{-.15in}% [[
369 ]] 370 ]]
370 << 371 <<
371 Error: Impossible to unify "?35 = ?34" with "unit = unit". 372 Error: Impossible to unify "?35 = ?34" with "unit = unit".
372 >> 373 >>
373 374
374 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 problem is in a part of the unification problem that is %\emph{%#<i>#not#</i>#%}% shown to us in this error message! 375 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 problem is in a part of the unification problem that is _not_ shown to us in this error message!
375 376
376 The following command is the secret to getting better error messages in such cases: *) 377 The following command is the secret to getting better error messages in such cases: *)
377 378
378 Set Printing All. 379 Set Printing All.
379 (** [[ 380 (** [[
381 ]] 382 ]]
382 << 383 <<
383 Error: Impossible to unify "@eq Type ?46 ?45" with "@eq Set unit unit". 384 Error: Impossible to unify "@eq Type ?46 ?45" with "@eq Set unit unit".
384 >> 385 >>
385 386
386 Now we can see the problem: it is the first, %\emph{%#<i>#implicit#</i>#%}% 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. *) 387 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. *)
387 388
388 Abort. 389 Abort.
389 390
390 (** 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. *) 391 (** 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. *)
391 392
427 H : x = 0 428 H : x = 0
428 The term "H" has type "x = 0" while it is expected to have type 429 The term "H" has type "x = 0" while it is expected to have type
429 "?99 = 0". 430 "?99 = 0".
430 >> 431 >>
431 432
432 The problem here is that variable [x] was introduced by [destruct] %\emph{%#<i>#after#</i>#%}% we introduced [?99] with [eexists], so the instantiation of [?99] may not mention [x]. A simple reordering of the proof solves the problem. *) 433 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. *)
433 434
434 Restart. 435 Restart.
435 destruct 1 as [x]; apply ex_intro with x; symmetry; assumption. 436 destruct 1 as [x]; apply ex_intro with x; symmetry; assumption.
436 Qed. 437 Qed.
437 438
483 484
484 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. 485 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.
485 486
486 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. 487 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.
487 488
488 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. *) 489 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. *)
489 490
490 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) := 491 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) :=
491 match x with 492 match x with
492 | exist n pf => exist _ n (sym_eq pf) 493 | exist n pf => exist _ n (sym_eq pf)
493 end. 494 end.
515 516
516 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. 517 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.
517 518
518 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. 519 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.
519 520
520 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. 521 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.
521 522
522 %\medskip% 523 %\medskip%
523 524
524 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. *) 525 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. *)
525 526
526 Check forall P Q : Prop, P \/ Q -> Q \/ P. 527 Check forall P Q : Prop, P \/ Q -> Q \/ P.
527 (** %\vspace{-.15in}% [[ 528 (** %\vspace{-.15in}% [[
528 forall P Q : Prop, P \/ Q -> Q \/ P 529 forall P Q : Prop, P \/ Q -> Q \/ P
529 : Prop 530 : Prop
599 (** Stating equality facts about proofs may seem baroque, but we have already seen its utility in the chapter on reasoning about equality proofs. *) 600 (** Stating equality facts about proofs may seem baroque, but we have already seen its utility in the chapter on reasoning about equality proofs. *)
600 601
601 602
602 (** * Axioms *) 603 (** * Axioms *)
603 604
604 (** 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. 605 (** 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.
605 606
606 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. *) 607 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. *)
607 608
608 (** ** The Basics *) 609 (** ** The Basics *)
609 610
625 Axiom positive : n > 0. 626 Axiom positive : n > 0.
626 Reset n. 627 Reset n.
627 628
628 (** 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. 629 (** 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.
629 630
630 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 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]. *) 631 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]. *)
631 632
632 Axiom not_classic : ~ forall P : Prop, P \/ ~ P. 633 Axiom not_classic : ~ forall P : Prop, P \/ ~ P.
633 634
634 Theorem uhoh : False. 635 Theorem uhoh : False.
635 generalize classic not_classic; tauto. 636 generalize classic not_classic; tauto.
639 destruct uhoh. 640 destruct uhoh.
640 Qed. 641 Qed.
641 642
642 Reset not_classic. 643 Reset not_classic.
643 644
644 (** 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. 645 (** 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.
645 646
646 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. 647 Recall that Coq implements %\index{constructive logic}%_constructive_ 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.
647 648
648 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. 649 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.
649 650
650 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}% *) 651 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}% *)
651 652
652 Theorem t1 : forall P : Prop, P -> ~ ~ P. 653 Theorem t1 : forall P : Prop, P -> ~ ~ P.
653 tauto. 654 tauto.
674 (** %\vspace{-.15in}% [[ 675 (** %\vspace{-.15in}% [[
675 Axioms: 676 Axioms:
676 classic : forall P : Prop, P \/ ~ P 677 classic : forall P : Prop, P \/ ~ P
677 ]] 678 ]]
678 679
679 It is possible to avoid this dependence in some specific cases, where excluded middle %\textit{%#<i>#is#</i>#%}% provable, for decidable families of propositions. *) 680 It is possible to avoid this dependence in some specific cases, where excluded middle _is_ provable, for decidable families of propositions. *)
680 681
681 Theorem nat_eq_dec : forall n m : nat, n = m \/ n <> m. 682 Theorem nat_eq_dec : forall n m : nat, n = m \/ n <> m.
682 induction n; destruct m; intuition; generalize (IHn m); intuition. 683 induction n; destruct m; intuition; generalize (IHn m); intuition.
683 Qed. 684 Qed.
684 685
691 Closed under the global context 692 Closed under the global context
692 >> 693 >>
693 694
694 %\bigskip% 695 %\bigskip%
695 696
696 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. *) 697 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. *)
697 698
698 Require Import ProofIrrelevance. 699 Require Import ProofIrrelevance.
699 Print proof_irrelevance. 700 Print proof_irrelevance.
700 (** %\vspace{-.15in}% [[ 701 (** %\vspace{-.15in}% [[
701 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ] 702 *** [ proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2 ]
791 792
792 (** ** Axioms of Choice *) 793 (** ** Axioms of Choice *)
793 794
794 (** 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. 795 (** 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.
795 796
796 First, it is possible to implement a choice operator %\textit{%#<i>#without#</i>#%}% axioms in some potentially surprising cases. *) 797 First, it is possible to implement a choice operator _without_ axioms in some potentially surprising cases. *)
797 798
798 Require Import ConstructiveEpsilon. 799 Require Import ConstructiveEpsilon.
799 Check constructive_definite_description. 800 Check constructive_definite_description.
800 (** %\vspace{-.15in}% [[ 801 (** %\vspace{-.15in}% [[
801 constructive_definite_description 802 constructive_definite_description
810 Print Assumptions constructive_definite_description. 811 Print Assumptions constructive_definite_description.
811 (** << 812 (** <<
812 Closed under the global context 813 Closed under the global context
813 >> 814 >>
814 815
815 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. 816 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.
816 817
817 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. *) 818 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. *)
818 819
819 Require Import ClassicalUniqueChoice. 820 Require Import ClassicalUniqueChoice.
820 Check dependent_unique_choice. 821 Check dependent_unique_choice.
857 858
858 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. *) 859 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. *)
859 860
860 (** ** Axioms and Computation *) 861 (** ** Axioms and Computation *)
861 862
862 (** 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. *) 863 (** 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. *)
863 864
864 Definition cast (x y : Set) (pf : x = y) (v : x) : y := 865 Definition cast (x y : Set) (pf : x = y) (v : x) : y :=
865 match pf with 866 match pf with
866 | refl_equal => v 867 | refl_equal => v
867 end. 868 end.
906 match 907 match
907 functional_extensionality 908 functional_extensionality
908 .... 909 ....
909 ]] 910 ]]
910 911
911 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. 912 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.
912 913
913 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *) 914 If we are careful in using tactics to prove an equality, we can still compute with casts over the proof. *)
914 915
915 Lemma plus1 : forall n, S n = n + 1. 916 Lemma plus1 : forall n, S n = n + 1.
916 induction n; simpl; intuition. 917 induction n; simpl; intuition.
929 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. *) 930 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. *)
930 931
931 932
932 (** ** Methods for Avoiding Axioms *) 933 (** ** Methods for Avoiding Axioms *)
933 934
934 (** 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. 935 (** 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.
935 936
936 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!) 937 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!)
937 938
938 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: *) 939 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: *)
939 940
1107 1108
1108 This example illustrates again how some of the same design patterns we learned for dependently typed programming can be used fruitfully in theorem statements. 1109 This example illustrates again how some of the same design patterns we learned for dependently typed programming can be used fruitfully in theorem statements.
1109 1110
1110 %\medskip% 1111 %\medskip%
1111 1112
1112 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 %\emph{%#<i>#compute#</i>#%}%. 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. 1113 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.
1113 1114
1114 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. *) 1115 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. *)
1115 1116
1116 Section withTypes. 1117 Section withTypes.
1117 Variable types : list Set. 1118 Variable types : list Set.
1171 Eval compute in getNat myValues myNatIndex myNatIndex_ok. 1172 Eval compute in getNat myValues myNatIndex myNatIndex_ok.
1172 (** %\vspace{-.15in}%[[ 1173 (** %\vspace{-.15in}%[[
1173 = 3 1174 = 3
1174 ]] 1175 ]]
1175 1176
1176 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] %\emph{%#<i>#independently#</i>#%}% of a specific proof. *) 1177 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. *)
1177 1178
1178 Theorem getNat_is_reasonable : forall pf, getNat myValues myNatIndex pf = 3. 1179 Theorem getNat_is_reasonable : forall pf, getNat myValues myNatIndex pf = 3.
1179 intro; compute. 1180 intro; compute.
1180 (** 1181 (**
1181 << 1182 <<
1224 1225
1225 Section withTypes'. 1226 Section withTypes'.
1226 Variable types : list Set. 1227 Variable types : list Set.
1227 Variable natIndex : nat. 1228 Variable natIndex : nat.
1228 1229
1229 (** Here is the trick: instead of asserting properties about the list [types], we build a %``%#"#new#"#%''% list that is %\emph{%#<i>#guaranteed by construction#</i>#%}% to have those properties. *) 1230 (** 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. *)
1230 1231
1231 Definition types' := update types natIndex nat. 1232 Definition types' := update types natIndex nat.
1232 1233
1233 Variable values : hlist (fun x : Set => x) types'. 1234 Variable values : hlist (fun x : Set => x) types'.
1234 1235
1252 | S natIndex' => fun vs => getNat' types0 natIndex' (htl vs) 1253 | S natIndex' => fun vs => getNat' types0 natIndex' (htl vs)
1253 end 1254 end
1254 end. 1255 end.
1255 End withTypes'. 1256 End withTypes'.
1256 1257
1257 (** Now the surprise comes in how easy it is to %\emph{%#<i>#use#</i>#%}% [getNat']. While typing works by modification of a types list, we can choose parameters so that the modification has no effect. *) 1258 (** 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. *)
1258 1259
1259 Theorem getNat_is_reasonable : getNat' myTypes myNatIndex myValues = 3. 1260 Theorem getNat_is_reasonable : getNat' myTypes myNatIndex myValues = 3.
1260 reflexivity. 1261 reflexivity.
1261 Qed. 1262 Qed.
1262 1263