Mercurial > cpdt > repo
changeset 435:a54a4a2ea6e4
Changes while hacking on coqdoc
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Thu, 26 Jul 2012 19:05:12 -0400 |
| parents | 92f386c33e94 |
| children | 5d5e44f905c7 |
| files | src/Coinductive.v src/Equality.v src/Large.v src/Universes.v |
| diffstat | 4 files changed, 7 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Coinductive.v Thu Jul 26 16:38:44 2012 -0400 +++ b/src/Coinductive.v Thu Jul 26 19:05:12 2012 -0400 @@ -447,7 +447,7 @@ Qed. (* end thide *) -(** Let us put [stream_eq_ind] through its paces a bit more, considering two different ways to compute infinite streams of all factorial values. First, we import the [fact] factorial function from the standard library. *) +(** Let us put [stream_eq_coind] through its paces a bit more, considering two different ways to compute infinite streams of all factorial values. First, we import the [fact] factorial function from the standard library. *) Require Import Arith. Print fact.
--- a/src/Equality.v Thu Jul 26 16:38:44 2012 -0400 +++ b/src/Equality.v Thu Jul 26 19:05:12 2012 -0400 @@ -23,7 +23,7 @@ (** * The Definitional Equality *) -(** We have seen many examples so far where proof goals follow "by computation." That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially. Exactly when this works and when it does not depends on the details of Coq's%\index{definitional equality}% _definitional equality_. This is an untyped binary relation appearing in the formal metatheory of CIC. CIC contains a typing rule allowing the conclusion $E : T$ from the premise $E : T'$ and a proof that $T$ and $T'$ are definitionally equal. +(** We have seen many examples so far where proof goals follow "by computation." That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially. Exactly when this works and when it does not depends on the details of Coq's%\index{definitional equality}% _definitional equality_. This is an untyped binary relation appearing in the formal metatheory of CIC. CIC contains a typing rule allowing the conclusion [E : T] from the premise [E : T'] and a proof that [T] and [T'] are definitionally equal. The %\index{tactics!cbv}%[cbv] tactic will help us illustrate the rules of Coq's definitional equality. We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [0] when applied to [1]. *)
--- a/src/Large.v Thu Jul 26 16:38:44 2012 -0400 +++ b/src/Large.v Thu Jul 26 19:05:12 2012 -0400 @@ -773,7 +773,7 @@ (** As in software development, large Coq projects are much more manageable when split across multiple files and when decomposed into libraries. Coq and Proof General provide very good support for these activities. - Consider a library that we will name [Lib], housed in directory <<LIB>> and split between files <<A.v>>, <<B.v>>, and <<C.v>>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}\texttt{%#<tt>#coq_makefile#</tt>#%}% to do the hard work. + Consider a library that we will name [Lib], housed in directory <<LIB>> and split between files <<A.v>>, <<B.v>>, and <<C.v>>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}%<<coq_makefile>> to do the hard work. << MODULES := A B C @@ -792,7 +792,7 @@ rm -f Makefile.coq >> - The Makefile begins by defining a variable <<VS>> holding the list of filenames to be included in the project. The primary target is <<coq>>, which depends on the construction of an auxiliary Makefile called <<Makefile.coq>>. Another rule explains how to build that file. We call %\texttt{%#<tt>#coq_makefile#</tt>#%}%, using the <<-R>> flag to specify that files in the current directory should be considered to belong to the library [Lib]. This Makefile will build a compiled version of each module, such that <<X.v>> is compiled into <<X.vo>>. + The Makefile begins by defining a variable <<VS>> holding the list of filenames to be included in the project. The primary target is <<coq>>, which depends on the construction of an auxiliary Makefile called <<Makefile.coq>>. Another rule explains how to build that file. We call <<coq_makefile>>, using the <<-R>> flag to specify that files in the current directory should be considered to belong to the library [Lib]. This Makefile will build a compiled version of each module, such that <<X.v>> is compiled into <<X.vo>>. Now code in <<B.v>> may refer to definitions in <<A.v>> after running [[ @@ -821,7 +821,7 @@ rm -f Makefile.coq >> - We change the %\texttt{%#<tt>#coq_makefile#</tt>#%}% call to indicate where the library [Lib] is found. Now <<D.v>> and <<E.v>> can refer to definitions from [Lib] module [A] after running + We change the <<coq_makefile>> call to indicate where the library [Lib] is found. Now <<D.v>> and <<E.v>> can refer to definitions from [Lib] module [A] after running [[ Require Import Lib.A. ]]
--- a/src/Universes.v Thu Jul 26 16:38:44 2012 -0400 +++ b/src/Universes.v Thu Jul 26 19:05:12 2012 -0400 @@ -412,7 +412,7 @@ Unset Printing All. Theorem ex_symmetry : (exists x, x = 0) -> (exists x, 0 = x). - econstructor. + eexists. (** %\vspace{-.15in}%[[ H : exists x : nat, x = 0 ============================ @@ -529,7 +529,7 @@ let sym_ex = __ >> -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. +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. 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.