Mercurial > cpdt > repo

comparison src/Universes.v @ 435:a54a4a2ea6e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Changes while hacking on coqdoc
author Adam Chlipala <adam@chlipala.net>
date Thu, 26 Jul 2012 19:05:12 -0400
parents 5744842c36a8
children 5d5e44f905c7
comparison
equal deleted inserted replaced
434:92f386c33e94 435:a54a4a2ea6e4
410 For completeness, we mention one other class of confusing error message about inability to unify two terms that look obviously unifiable. Each unification variable has a scope; a unification variable instantiation may not mention variables that were not already defined within that scope, at the point in proof search where the unification variable was introduced. Consider this illustrative example: *) 410 For completeness, we mention one other class of confusing error message about inability to unify two terms that look obviously unifiable. Each unification variable has a scope; a unification variable instantiation may not mention variables that were not already defined within that scope, at the point in proof search where the unification variable was introduced. Consider this illustrative example: *)
411 411
412 Unset Printing All. 412 Unset Printing All.
413 413
414 Theorem ex_symmetry : (exists x, x = 0) -> (exists x, 0 = x). 414 Theorem ex_symmetry : (exists x, x = 0) -> (exists x, 0 = x).
415 econstructor. 415 eexists.
416 (** %\vspace{-.15in}%[[ 416 (** %\vspace{-.15in}%[[
417 H : exists x : nat, x = 0 417 H : exists x : nat, x = 0
418 ============================ 418 ============================
419 0 = ?98 419 0 = ?98
420 ]] 420 ]]
527 (** val sym_ex : __ **) 527 (** val sym_ex : __ **)
528 528
529 let sym_ex = __ 529 let sym_ex = __
530 >> 530 >>
531 531
532 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. 532 In this example, the [ex] type itself is in [Prop], so whole [ex] packages are erased. Coq extracts every proposition as the (Coq-specific) type <<__>>, whose single constructor is <<__>>. Not only are proofs replaced by [__], but proof arguments to functions are also removed completely, as we see here.
533 533
534 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. 534 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.
535 535
536 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. 536 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.
537 537