Mercurial > cpdt > repo

comparison src/Universes.v @ 444:0d66f1a710b8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Vertical spacing through end of Part II
author Adam Chlipala <adam@chlipala.net>
date Wed, 01 Aug 2012 17:03:39 -0400
parents 8077352044b2
children b750ec0a8edb
comparison
equal deleted inserted replaced
443:97c60ffdb998 444:0d66f1a710b8
33 33
34 Check 0. 34 Check 0.
35 (** %\vspace{-.15in}% [[ 35 (** %\vspace{-.15in}% [[
36 0 36 0
37 : nat 37 : nat
38
39 ]] 38 ]]
40 39
41 It is natural enough that zero be considered as a natural number. *) 40 It is natural enough that zero be considered as a natural number. *)
42 41
43 Check nat. 42 Check nat.
44 (** %\vspace{-.15in}% [[ 43 (** %\vspace{-.15in}% [[
45 nat 44 nat
46 : Set 45 : Set
47
48 ]] 46 ]]
49 47
50 From a set theory perspective, it is unsurprising to consider the natural numbers as a "set." *) 48 From a set theory perspective, it is unsurprising to consider the natural numbers as a "set." *)
51 49
52 Check Set. 50 Check Set.
53 (** %\vspace{-.15in}% [[ 51 (** %\vspace{-.15in}% [[
54 Set 52 Set
55 : Type 53 : Type
56
57 ]] 54 ]]
58 55
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 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]. *)
60 57
61 Check Type. 58 Check Type.
62 (** %\vspace{-.15in}% [[ 59 (** %\vspace{-.15in}% [[
63 Type 60 Type
64 : Type 61 : Type
65
66 ]] 62 ]]
67 63
68 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? 64 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?
69 65
70 Let us repeat some of our queries after toggling a flag related to Coq's printing behavior.%\index{Vernacular commands!Set Printing Universes}% *) 66 Let us repeat some of our queries after toggling a flag related to Coq's printing behavior.%\index{Vernacular commands!Set Printing Universes}% *)
80 76
81 Check Set. 77 Check Set.
82 (** %\vspace{-.15in}% [[ 78 (** %\vspace{-.15in}% [[
83 Set 79 Set
84 : Type $ (0)+1 ^ 80 : Type $ (0)+1 ^
85
86 ]] 81 ]]
87 *) 82 *)
88 83
89 Check Type. 84 Check Type.
90 (** %\vspace{-.15in}% [[ 85 (** %\vspace{-.15in}% [[
91 Type $ Top.3 ^ 86 Type $ Top.3 ^
92 : Type $ (Top.3)+1 ^ 87 : Type $ (Top.3)+1 ^
93
94 ]] 88 ]]
95 89
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]. 90 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].
97 91
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]. 92 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].
117 111
118 Check forall T : Type, T. 112 Check forall T : Type, T.
119 (** %\vspace{-.15in}% [[ 113 (** %\vspace{-.15in}% [[
120 forall T : Type $ Top.9 ^ , T 114 forall T : Type $ Top.9 ^ , T
121 : Type $ max(Top.9, (Top.9)+1) ^ 115 : Type $ max(Top.9, (Top.9)+1) ^
122
123 ]] 116 ]]
124 117
125 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. 118 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.
126 119
127 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]. *) 120 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]. *)
180 173
181 174
182 (** ** Inductive Definitions *) 175 (** ** Inductive Definitions *)
183 176
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]. 177 (** 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].
185
186 [[ 178 [[
187 Inductive exp : Set -> Set := 179 Inductive exp : Set -> Set :=
188 | Const : forall T : Set, T -> exp T 180 | Const : forall T : Set, T -> exp T
189 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) 181 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
190 | Eq : forall T, exp T -> exp T -> exp bool. 182 | Eq : forall T, exp T -> exp T -> exp bool.
221 213
222 Check Eq (Const Set) (Const Type). 214 Check Eq (Const Set) (Const Type).
223 (** %\vspace{-.15in}% [[ 215 (** %\vspace{-.15in}% [[
224 Eq (Const Set) (Const Type $ Top.59 ^ ) 216 Eq (Const Set) (Const Type $ Top.59 ^ )
225 : exp bool 217 : exp bool
226
227 ]] 218 ]]
228 219
229 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall. 220 We can check many expressions, including fancy expressions that include types. However, it is not hard to hit a type-checking wall.
230
231 [[ 221 [[
232 Check Const (Const O). 222 Check Const (Const O).
233 ]] 223 ]]
234 224
235 << 225 <<
236 Error: Universe inconsistency (cannot enforce Top.42 < Top.42). 226 Error: Universe inconsistency (cannot enforce Top.42 < Top.42).
237 >> 227 >>
238 228
239 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. *) 229 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. *)
240
241 (** [[ 230 (** [[
242 Print exp. 231 Print exp.
243 ]] 232 ]]
244 233 %\vspace{-.15in}%[[
245 [[
246 Inductive exp 234 Inductive exp
247 : Type $ Top.8 ^ -> 235 : Type $ Top.8 ^ ->
248 Type 236 Type
249 $ max(0, (Top.11)+1, (Top.14)+1, (Top.15)+1, (Top.19)+1) ^ := 237 $ max(0, (Top.11)+1, (Top.14)+1, (Top.15)+1, (Top.19)+1) ^ :=
250 Const : forall T : Type $ Top.11 ^ , T -> exp T 238 Const : forall T : Type $ Top.11 ^ , T -> exp T
251 | Pair : forall (T1 : Type $ Top.14 ^ ) (T2 : Type $ Top.15 ^ ), 239 | Pair : forall (T1 : Type $ Top.14 ^ ) (T2 : Type $ Top.15 ^ ),
252 exp T1 -> exp T2 -> exp (T1 * T2) 240 exp T1 -> exp T2 -> exp (T1 * T2)
253 | Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool 241 | Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool
254
255 ]] 242 ]]
256 243
257 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. 244 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.
258 245
259 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}% *) 246 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}% *)
262 (** %\vspace{-.15in}% [[ 249 (** %\vspace{-.15in}% [[
263 Top.19 < Top.9 <= Top.8 250 Top.19 < Top.9 <= Top.8
264 Top.15 < Top.9 <= Top.8 <= Coq.Init.Datatypes.38 251 Top.15 < Top.9 <= Top.8 <= Coq.Init.Datatypes.38
265 Top.14 < Top.9 <= Top.8 <= Coq.Init.Datatypes.37 252 Top.14 < Top.9 <= Top.8 <= Coq.Init.Datatypes.37
266 Top.11 < Top.9 <= Top.8 253 Top.11 < Top.9 <= Top.8
267
268 ]] 254 ]]
269 255
270 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. 256 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.
271 257
272 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. *) 258 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. *)
276 Inductive prod := pair. 262 Inductive prod := pair.
277 Reset prod. 263 Reset prod.
278 (* end thide *) 264 (* end thide *)
279 (* end hide *) 265 (* end hide *)
280 266
281 (** [[ 267 (** %\vspace{-.3in}%[[
282 Print prod. 268 Print prod.
283 ]] 269 ]]
284 270 %\vspace{-.15in}%[[
285 [[
286 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ ) 271 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ )
287 (B : Type $ Coq.Init.Datatypes.38 ^ ) 272 (B : Type $ Coq.Init.Datatypes.38 ^ )
288 : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ := 273 : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ :=
289 pair : A -> B -> A * B 274 pair : A -> B -> A * B
290
291 ]] 275 ]]
292 276
293 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]. 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].
294 278
295 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. 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.
308 292
309 The same cannot be done with a counterpart to [prod] that does not use parameters. *) 293 The same cannot be done with a counterpart to [prod] that does not use parameters. *)
310 294
311 Inductive prod' : Type -> Type -> Type := 295 Inductive prod' : Type -> Type -> Type :=
312 | pair' : forall A B : Type, A -> B -> prod' A B. 296 | pair' : forall A B : Type, A -> B -> prod' A B.
313 (** [[ 297 (** %\vspace{-.15in}%[[
314 Check (pair' nat (pair' Type Set)). 298 Check (pair' nat (pair' Type Set)).
315 ]] 299 ]]
316 300
317 << 301 <<
318 Error: Universe inconsistency (cannot enforce Top.51 < Top.51). 302 Error: Universe inconsistency (cannot enforce Top.51 < Top.51).
345 329
346 Check foo True. 330 Check foo True.
347 (** %\vspace{-.15in}% [[ 331 (** %\vspace{-.15in}% [[
348 foo True 332 foo True
349 : Prop 333 : Prop
350
351 ]] 334 ]]
352 335
353 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]. 336 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].
354 337
355 Imitation polymorphism can be confusing in some contexts. For instance, it is what is responsible for this weird behavior. *) 338 Imitation polymorphism can be confusing in some contexts. For instance, it is what is responsible for this weird behavior. *)
376 Qed. 359 Qed.
377 360
378 (** Let us attempt an admittedly silly proof of the following theorem. *) 361 (** Let us attempt an admittedly silly proof of the following theorem. *)
379 362
380 Theorem illustrative_but_silly_detour : unit = unit. 363 Theorem illustrative_but_silly_detour : unit = unit.
381 (** [[ 364 (** %\vspace{-.25in}%[[
382 apply symmetry. 365 apply symmetry.
383 ]] 366 ]]
384 << 367 <<
385 Error: Impossible to unify "?35 = ?34" with "unit = unit". 368 Error: Impossible to unify "?35 = ?34" with "unit = unit".
386 >> 369 >>
387 370
388 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! 371 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!
389 372
390 The following command is the secret to getting better error messages in such cases: *) 373 The following command is the secret to getting better error messages in such cases: *)
391 374
392 Set Printing All. 375 Set Printing All.
393 (** [[ 376 (** %\vspace{-.15in}%[[
394 apply symmetry. 377 apply symmetry.
395 ]] 378 ]]
396 << 379 <<
397 Error: Impossible to unify "@eq Type ?46 ?45" with "@eq Set unit unit". 380 Error: Impossible to unify "@eq Type ?46 ?45" with "@eq Set unit unit".
398 >> 381 >>
399 382
429 ============================ 412 ============================
430 0 = ?99 413 0 = ?99
431 ]] 414 ]]
432 *) 415 *)
433 416
434 (** [[ 417 (** %\vspace{-.2in}%[[
435 symmetry; exact H. 418 symmetry; exact H.
436 ]] 419 ]]
437 420
438 << 421 <<
439 Error: In environment 422 Error: In environment
440 x : nat 423 x : nat
545 528
546 Check forall P Q : Prop, P \/ Q -> Q \/ P. 529 Check forall P Q : Prop, P \/ Q -> Q \/ P.
547 (** %\vspace{-.15in}% [[ 530 (** %\vspace{-.15in}% [[
548 forall P Q : Prop, P \/ Q -> Q \/ P 531 forall P Q : Prop, P \/ Q -> Q \/ P
549 : Prop 532 : Prop
550
551 ]] 533 ]]
552 534
553 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. 535 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.
554 536
555 Impredicativity also allows us to implement a version of our earlier [exp] type that does not suffer from the weakness that we found. *) 537 Impredicativity also allows us to implement a version of our earlier [exp] type that does not suffer from the weakness that we found. *)
582 564
583 Check ConstP (ConstP O). 565 Check ConstP (ConstP O).
584 (** %\vspace{-.15in}% [[ 566 (** %\vspace{-.15in}% [[
585 ConstP (ConstP 0) 567 ConstP (ConstP 0)
586 : expP (expP nat) 568 : expP (expP nat)
587
588 ]] 569 ]]
589 570
590 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 [=]. *) 571 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 [=]. *)
591 572
592 Inductive eqPlus : forall T, T -> T -> Prop := 573 Inductive eqPlus : forall T, T -> T -> Prop :=
678 Closed under the global context 659 Closed under the global context
679 >> 660 >>
680 *) 661 *)
681 662
682 Theorem t2 : forall P : Prop, ~ ~ P -> P. 663 Theorem t2 : forall P : Prop, ~ ~ P -> P.
683 (** [[ 664 (** %\vspace{-.25in}%[[
684 tauto. 665 tauto.
685 ]] 666 ]]
686 << 667 <<
687 Error: tauto failed. 668 Error: tauto failed.
688 >> 669 >>
865 (** %\vspace{-.15in}% [[ 846 (** %\vspace{-.15in}% [[
866 choice 847 choice
867 : forall (A B : Type) (R : A -> B -> Prop), 848 : forall (A B : Type) (R : A -> B -> Prop),
868 (forall x : A, exists y : B, R x y) -> 849 (forall x : A, exists y : B, R x y) ->
869 exists f : A -> B, forall x : A, R x (f x) 850 exists f : A -> B, forall x : A, R x (f x)
870 851 ]]
871 ]]
872 852
873 This principle is proved as a theorem, based on the unique choice axiom and an additional axiom of relational choice from the [RelationalChoice] module. 853 This principle is proved as a theorem, based on the unique choice axiom and an additional axiom of relational choice from the [RelationalChoice] module.
874 854
875 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. *) 855 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. *)
876 856
913 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n)); 893 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
914 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush. 894 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
915 Qed. 895 Qed.
916 896
917 Eval compute in (cast t3 (fun _ => First)) 12. 897 Eval compute in (cast t3 (fun _ => First)) 12.
918 (** [[ 898 (** %\vspace{-.15in}%[[
919 = match t3 in (_ = P) return P with 899 = match t3 in (_ = P) return P with
920 | eq_refl => fun n : nat => First 900 | eq_refl => fun n : nat => First
921 end 12 901 end 12
922 : fin (12 + 1) 902 : fin (12 + 1)
923 ]] 903 ]]
930 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n)); 910 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
931 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush. 911 rewrite (functional_extensionality (fun n => fin (n + 1)) (fun n => fin (S n))); crush.
932 Defined. 912 Defined.
933 913
934 Eval compute in (cast t3 (fun _ => First)) 12. 914 Eval compute in (cast t3 (fun _ => First)) 12.
935 (** [[ 915 (** %\vspace{-.15in}%[[
936 = match 916 = match
937 match 917 match
938 match 918 match
939 functional_extensionality 919 functional_extensionality
940 .... 920 ....