Mercurial > cpdt > repo
comparison src/Universes.v @ 229:2bb1642f597c
Prop section
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 20 Nov 2009 11:02:26 -0500 |
parents | 0be1a42b3035 |
children | 9dbcd6bad488 |
comparison
equal
deleted
inserted
replaced
228:0be1a42b3035 | 229:2bb1642f597c |
---|---|
290 Error: Universe inconsistency (cannot enforce Top.51 < Top.51). | 290 Error: Universe inconsistency (cannot enforce Top.51 < Top.51). |
291 | 291 |
292 ]] | 292 ]] |
293 | 293 |
294 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. *) | 294 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. *) |
295 | |
296 (* begin hide *) | |
297 Unset Printing Universes. | |
298 (* end hide *) | |
299 | |
300 | |
301 (** * The [Prop] Universe *) | |
302 | |
303 (** 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. | |
304 | |
305 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]. *) | |
306 | |
307 Print sig. | |
308 (** %\vspace{-.15in}% [[ | |
309 Inductive sig (A : Type) (P : A -> Prop) : Type := | |
310 exist : forall x : A, P x -> sig P | |
311 ]] *) | |
312 | |
313 Print ex. | |
314 (** %\vspace{-.15in}% [[ | |
315 Inductive ex (A : Type) (P : A -> Prop) : Prop := | |
316 ex_intro : forall x : A, P x -> ex P | |
317 | |
318 ]] | |
319 | |
320 It is natural to want a function to extract the first components of data structures like these. Doing so is easy enough for [sig]. *) | |
321 | |
322 Definition projS A (P : A -> Prop) (x : sig P) : A := | |
323 match x with | |
324 | exist v _ => v | |
325 end. | |
326 | |
327 (** We run into trouble with a version that has been changed to work with [ex]. | |
328 | |
329 [[ | |
330 Definition projE A (P : A -> Prop) (x : ex P) : A := | |
331 match x with | |
332 | ex_intro v _ => v | |
333 end. | |
334 | |
335 Error: | |
336 Incorrect elimination of "x" in the inductive type "ex": | |
337 the return type has sort "Type" while it should be "Prop". | |
338 Elimination of an inductive object of sort Prop | |
339 is not allowed on a predicate in sort Type | |
340 because proofs can be eliminated only to build proofs. | |
341 | |
342 ]] | |
343 | |
344 In formal Coq parlance, "elimination" means "pattern-matching." The typing rules of Gallina forbid us from pattern-matching on a discriminee whose types 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. | |
345 | |
346 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. | |
347 | |
348 Recall that 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. *) | |
349 | |
350 Definition sym_sig (x : sig (fun n => n = 0)) : sig (fun n => 0 = n) := | |
351 match x with | |
352 | exist n pf => exist _ n (sym_eq pf) | |
353 end. | |
354 | |
355 Extraction sym_sig. | |
356 (** << | |
357 (** val sym_sig : nat -> nat **) | |
358 | |
359 let sym_sig x = x | |
360 >> | |
361 | |
362 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. *) | |
363 | |
364 Definition sym_ex (x : ex (fun n => n = 0)) : ex (fun n => 0 = n) := | |
365 match x with | |
366 | ex_intro n pf => ex_intro _ n (sym_eq pf) | |
367 end. | |
368 | |
369 Extraction sym_ex. | |
370 (** << | |
371 (** val sym_ex : __ **) | |
372 | |
373 let sym_ex = __ | |
374 >> | |
375 | |
376 In this example, the [ex] type itself is in [Prop], so whole [ex] packages are erased. Coq extracts every proposition as the 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. | |
377 | |
378 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, these proofs exist at runtime and consume resources. In contrast, with Coq, as long as you keep all of your proofs within [Prop], extraction is guaranteed to erase them. | |
379 | |
380 Many fans of the 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. | |
381 | |
382 %\medskip% | |
383 | |
384 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 %\textit{%#<i>#impredicative#</i>#%}%, as this example shows. *) | |
385 | |
386 Check forall P Q : Prop, P \/ Q -> Q \/ P. | |
387 (** %\vspace{-.15in}% [[ | |
388 forall P Q : Prop, P \/ Q -> Q \/ P | |
389 : Prop | |
390 | |
391 ]] | |
392 | |
393 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. *) |