# HG changeset patch # User Adam Chlipala # Date 1343343912 14400 # Node ID a54a4a2ea6e473cfdeb6b6fe25de3a55c54cc7cb # Parent 92f386c33e9452cf3af284dedc146635c2642c32 Changes while hacking on coqdoc diff -r 92f386c33e94 -r a54a4a2ea6e4 src/Coinductive.v --- 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. diff -r 92f386c33e94 -r a54a4a2ea6e4 src/Equality.v --- 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]. *) diff -r 92f386c33e94 -r a54a4a2ea6e4 src/Large.v --- 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 <> and split between files <>, <>, and <>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}\texttt{%##coq_makefile##%}% to do the hard work. + Consider a library that we will name [Lib], housed in directory <> and split between files <>, <>, and <>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{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 <> holding the list of filenames to be included in the project. The primary target is <>, which depends on the construction of an auxiliary Makefile called <>. Another rule explains how to build that file. We call %\texttt{%##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 <> is compiled into <>. + The Makefile begins by defining a variable <> holding the list of filenames to be included in the project. The primary target is <>, which depends on the construction of an auxiliary Makefile called <>. Another rule explains how to build that file. We call <>, 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 <> is compiled into <>. Now code in <> may refer to definitions in <> after running [[ @@ -821,7 +821,7 @@ rm -f Makefile.coq >> - We change the %\texttt{%##coq_makefile##%}% call to indicate where the library [Lib] is found. Now <> and <> can refer to definitions from [Lib] module [A] after running + We change the <> call to indicate where the library [Lib] is found. Now <> and <> can refer to definitions from [Lib] module [A] after running [[ Require Import Lib.A. ]] diff -r 92f386c33e94 -r a54a4a2ea6e4 src/Universes.v --- 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{\_\_}%#__#, whose single constructor is %\texttt{\_\_}%#__#. 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.