Mercurial > cpdt > repo
changeset 437:8077352044b2
A pass over all formatting, after big pile of coqdoc changes
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 27 Jul 2012 16:47:28 -0400 |
| parents | 5d5e44f905c7 |
| children | f1f779c6a232 |
| files | src/Coinductive.v src/DataStruct.v src/Equality.v src/GeneralRec.v src/Generic.v src/InductiveTypes.v src/Intro.v src/Large.v src/LogicProg.v src/Match.v src/MoreDep.v src/Reflection.v src/Subset.v src/Universes.v |
| diffstat | 14 files changed, 109 insertions(+), 35 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Coinductive.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/Coinductive.v Fri Jul 27 16:47:28 2012 -0400 @@ -50,7 +50,9 @@ End stream. (* begin hide *) +(* begin thide *) CoInductive evilStream := Nil. +(* end thide *) (* end hide *) (** The definition is surprisingly simple. Starting from the definition of [list], we just need to change the keyword [Inductive] to [CoInductive]. We could have left a [Nil] constructor in our definition, but we will leave it out to force all of our streams to be infinite. @@ -105,7 +107,9 @@ (* end thide *) (* begin hide *) +(* begin thide *) Definition looper := 0. +(* end thide *) (* end hide *) (** So far, it looks like co-inductive types might be a magic bullet, allowing us to import all of the Haskeller's usual tricks. However, there are important restrictions that are dual to the restrictions on the use of inductive types. Fixpoints _consume_ values of inductive types, with restrictions on which _arguments_ may be passed in recursive calls. Dually, co-fixpoints _produce_ values of co-inductive types, with restrictions on what may be done with the _results_ of co-recursive calls. @@ -139,7 +143,9 @@ End map. (* begin hide *) +(* begin thide *) Definition filter := 0. +(* end thide *) (* end hide *) (** This code is a literal copy of that for the list [map] function, with the [nil] case removed and [Fixpoint] changed to [CoFixpoint]. Many other standard functions on lazy data structures can be implemented just as easily. Some, like [filter], cannot be implemented. Since the predicate passed to [filter] may reject every element of the stream, we cannot satisfy the guardedness condition. @@ -215,7 +221,9 @@ Theorem ones_eq : ones = ones'. (* begin hide *) +(* begin thide *) Definition foo := @eq. +(* end thide *) (* end hide *) (** However, faced with the initial subgoal, it is not at all clear how this theorem can be proved. In fact, it is unprovable. The [eq] predicate that we use is fundamentally limited to equalities that can be demonstrated by finite, syntactic arguments. To prove this equivalence, we will need to introduce a new relation. *)
--- a/src/DataStruct.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/DataStruct.v Fri Jul 27 16:47:28 2012 -0400 @@ -161,7 +161,9 @@ (* end thide *) (* begin hide *) +(* begin thide *) Definition map' := map. +(* end thide *) (* end hide *) (** Our [get] function is also quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *) @@ -237,7 +239,8 @@ match mem in member ls' return (match ls' with | nil => Empty_set | x' :: ls'' => - B x' -> (member ls'' -> B elm) -> B elm + B x' -> (member ls'' -> B elm) + -> B elm end) with | MFirst _ => fun x _ => x | MNext _ _ mem' => fun _ get_mls' => get_mls' mem' @@ -472,7 +475,9 @@ (** By pattern-matching on the equality proof [pf], we make that equality known to the type-checker. Exactly why this works can be seen by studying the definition of equality. *) (* begin hide *) - Definition foo := (@eq, @eq_refl). + (* begin thide *) + Definition foo := @eq_refl. + (* end thide *) (* end hide *) Print eq.
--- a/src/Equality.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/Equality.v Fri Jul 27 16:47:28 2012 -0400 @@ -154,7 +154,9 @@ end. (* begin hide *) -Definition foo := @eq. +(* begin thide *) +Definition foo := (@eq, plus). +(* end thide *) (* end hide *) Eval compute in fun ls => addLists' ls nil. @@ -214,7 +216,9 @@ Implicit Arguments fhget [A B elm ls]. (* begin hide *) +(* begin thide *) Definition map := O. +(* end thide *) (* end hide *) (** We can define a [map]-like function for [fhlist]s. *) @@ -233,9 +237,11 @@ Implicit Arguments fhmap [ls]. (* begin hide *) + (* begin thide *) Definition ilist := O. Definition get := O. Definition imap := O. + (* end thide *) (* end hide *) (** For the inductive versions of the [ilist] definitions, we proved a lemma about the interaction of [get] and [imap]. It was a strategic choice not to attempt such a proof for the definitions that we just gave, because that sets us on a collision course with the problems that are the subject of this chapter. *) @@ -369,7 +375,9 @@ (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *) (* begin hide *) + (* begin thide *) Definition lemma3' := O. + (* end thide *) (* end hide *) Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x. @@ -428,7 +436,9 @@ The axiom %\index{Gallina terms!eq\_rect\_eq}%[eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered. The term [eq_rect] is the automatically generated recursion principle for [eq]. Calling [eq_rect] is another way of [match]ing on an equality proof. The proof we match on is the argument [h], and [x] is the body of the [match]. The statement of [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed. We can see this intuition better in code by asking Coq to simplify the theorem statement with the [compute] reduction strategy (which, by the way, applies all applicable rules of the definitional equality presented in this chapter's first section). *) (* begin hide *) + (* begin thide *) Definition False' := False. + (* end thide *) (* end hide *) Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p), @@ -445,7 +455,9 @@ This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *) (* begin hide *) - Definition Streicher_K' := (Streicher_K, UIP_refl__Streicher_K). + (* begin thide *) + Definition Streicher_K' := UIP_refl__Streicher_K. + (* end thide *) (* end hide *) Print Streicher_K. @@ -462,7 +474,9 @@ End fhlist_map. (* begin hide *) +(* begin thide *) Require Eqdep_dec. +(* end thide *) (* end hide *) (** It is worth remarking that it is possible to avoid axioms altogether for equalities on types with decidable equality. The [Eqdep_dec] module of the standard library contains a parametric proof of [UIP_refl] for such cases. To simplify presentation, we will stick with the axiom version in the rest of this chapter. *)
--- a/src/GeneralRec.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/GeneralRec.v Fri Jul 27 16:47:28 2012 -0400 @@ -93,7 +93,9 @@ The bulk of the definitional work devolves to the%\index{accessibility relation}\index{Gallina terms!Acc}% _accessibility_ relation [Acc], whose definition we may also examine. *) (* begin hide *) +(* begin thide *) Definition Acc_intro' := Acc_intro. +(* end thide *) (* end hide *) Print Acc. @@ -752,7 +754,9 @@ (TBind m1 (fun x => m2)) (right associativity, at level 70). (* begin hide *) +(* begin thide *) Definition fib := pred. +(* end thide *) (* end hide *) (** %\vspace{-.15in}%[[
--- a/src/Generic.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/Generic.v Fri Jul 27 16:47:28 2012 -0400 @@ -361,7 +361,9 @@ *) (* begin hide *) +(* begin thide *) Definition append' := append. +(* end thide *) (* end hide *) (** Some of these simplified terms seem overly complex because we have turned off simplification of calls to [append], which is what uses of the [++] operator desugar to. Selective [++] simplification would combine adjacent string literals, yielding more or less the code we would write manually to implement this printing scheme. *) @@ -647,7 +649,9 @@ induction r; crush. (* begin hide *) + (* begin thide *) Definition pred' := pred. + (* end thide *) (* end hide *) (** The base case is discharged automatically, and the inductive case looks like this, where [H] is the outer IH (for induction over [T] values) and [IHn] is the inner IH (for induction over the recursive arguments).
--- a/src/InductiveTypes.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/InductiveTypes.v Fri Jul 27 16:47:28 2012 -0400 @@ -711,9 +711,11 @@ Given our last example of an inductive type, many readers are probably eager to try encoding the syntax of %\index{lambda calculus}%lambda calculus. Indeed, the function-based representation technique that we just used, called%\index{higher-order abstract syntax}\index{HOAS|see{higher-order abstract syntax}}% _higher-order abstract syntax_ (HOAS)%~\cite{HOAS}%, is the representation of choice for lambda calculi in %\index{Twelf}%Twelf and in many applications implemented in Haskell and ML. Let us try to import that choice to Coq: *) (* begin hide *) +(* begin thide *) Inductive term : Set := App | Abs. Reset term. Definition uhoh := O. +(* end thide *) (* end hide *) (** [[ Inductive term : Set := @@ -749,11 +751,8 @@ (** As we have emphasized a few times already, Coq proofs are actually programs, written in the same language we have been using in our examples all along. We can get a first sense of what this means by taking a look at the definitions of some of the %\index{induction principles}%induction principles we have used. A close look at the details here will help us construct induction principles manually, which we will see is necessary for some more advanced inductive definitions. *) -(* begin hide *) Print unit_ind. -(* end hide *) -(** %\noindent%[Print] [unit_ind.] *) -(** [[ +(** %\vspace{-.15in}%[[ unit_ind = fun P : unit -> Prop => unit_rect P : forall P : unit -> Prop, P tt -> forall u : unit, P u @@ -771,11 +770,8 @@ The principle [unit_rect] gives [P] type [unit -> Type] instead of [unit -> Prop]. [Type] is another universe, like [Set] and [Prop]. In fact, it is a common supertype of both. Later on, we will discuss exactly what the significances of the different universes are. For now, it is just important that we can use [Type] as a sort of meta-universe that may turn out to be either [Set] or [Prop]. We can see the symmetry inherent in the subtyping relationship by printing the definition of another principle that was generated for [unit] automatically: *) -(* begin hide *) Print unit_rec. -(* end hide *) -(** %\noindent%[Print] [unit_rec.] *) -(** [[ +(** %\vspace{-.15in}%[[ unit_rec = fun P : unit -> Set => unit_rect P : forall P : unit -> Set, P tt -> forall u : unit, P u @@ -794,11 +790,8 @@ (** Going even further down the rabbit hole, [unit_rect] itself is not even a primitive. It is a functional program that we can write manually. *) -(* begin hide *) Print unit_rect. -(* end hide *) -(** %\noindent%[Print] [unit_rect.] *) -(** [[ +(** %\vspace{-.15in}%[[ unit_rect = fun (P : unit -> Type) (f : P tt) (u : unit) => match u as u0 return (P u0) with @@ -820,7 +813,9 @@ end. (* begin hide *) +(* begin thide *) Definition foo := nat_rect. +(* end thide *) (* end hide *) (** We rely on Coq's heuristics for inferring [match] annotations, which are not consulted in the pretty-printing of terms. @@ -1020,7 +1015,9 @@ All P ls -> P (NNode' n ls). (* begin hide *) + (* begin thide *) Definition list_nat_tree_ind := O. + (* end thide *) (* end hide *) (** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions.
--- a/src/Intro.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/Intro.v Fri Jul 27 16:47:28 2012 -0400 @@ -211,7 +211,9 @@ The extra arguments demonstrated here are the proper choices for working with the code for this book. The ellipses stand for other Emacs customization settings you may already have. It can be helpful to save several alternate sets of flags in your <<.emacs>> file, with all but one commented out within the <<custom-set-variables>> block at any given time. Alternatively, Proof General configuration can be set on a per-directory basis, using a %\index{.dir-locals.el file@\texttt{.dir-locals.el} file}%<<.dir-locals.el>> file in the directory of the source files for which you want the settings to apply. Here is an example that could be written in such a file to enable use of the book source. Note the need to include an argument that starts Coq in Emacs support mode. -%\begin{verbatim}%#<pre>#((coq-mode . ((coq-prog-args . ("-emacs-U" "-I" "DIR/src")))))#</pre>#%\end{verbatim}% +<< +((coq-mode . ((coq-prog-args . ("-emacs-U" "-I" "DIR/src"))))) +>> #</li># #</ol>#%\end{enumerate}%
--- a/src/Large.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/Large.v Fri Jul 27 16:47:28 2012 -0400 @@ -463,7 +463,9 @@ info t. (* begin hide *) + (* begin thide *) Definition eir := eq_ind_r. + (* end thide *) (* end hide *) (** %\vspace{-.15in}%[[ @@ -591,7 +593,9 @@ debug eauto 6. (* begin hide *) + (* begin thide *) Definition deeeebug := (@eq_refl, @sym_eq). + (* end thide *) (* end hide *) (** The output is a large proof tree. The beginning of the tree is enough to reveal what is happening: @@ -755,6 +759,7 @@ (** * Build Processes *) (* begin hide *) +(* begin thide *) Module Lib. Module A. End A. @@ -769,6 +774,7 @@ Module E. End E. End Client. +(* end thide *) (* end hide *) (** 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.
--- a/src/LogicProg.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/LogicProg.v Fri Jul 27 16:47:28 2012 -0400 @@ -77,7 +77,9 @@ (* end thide *) (* begin hide *) +(* begin thide *) Definition er := @eq_refl. +(* end thide *) (* end hide *) Print four_plus_three. @@ -356,6 +358,12 @@ (** We see worrying exponential growth in running time, and the %\index{tactics!debug}%[debug] tactical helps us see where [eauto] is wasting its time, outputting a trace of every proof step that is attempted. The rule [eq_trans] applies at every node of a proof tree, and [eauto] tries all such positions. *) +(* begin hide *) +(* begin thide *) +Definition syms := (eq_sym, plus_n_O, eq_add_S, f_equal2). +(* end thide *) +(* end hide *) + debug eauto 3. (** [[ 1 depth=3 @@ -403,7 +411,7 @@ Abort. (* end thide *) -(** One simple example from before runs in the same amount of time, avoiding pollution by transivity. *) +(** One simple example from before runs in the same amount of time, avoiding pollution by transitivity. *) Example seven_minus_three_again : exists x, x + 3 = 7. (* begin thide *) @@ -510,7 +518,9 @@ (** We see that the two unification variables stand for the two elements of the list. Indeed, list length is independent of data values. Paradoxically, we can make the proof search process easier by constraining the list further, so that proof search naturally locates appropriate data elements by unification. The library predicate [Forall] will be helpful. *) (* begin hide *) +(* begin thide *) Definition Forall_c := (@Forall_nil, @Forall_cons). +(* end thide *) (* end hide *) Print Forall. @@ -532,7 +542,9 @@ (** We can see which list [eauto] found by printing the proof term. *) (* begin hide *) +(* begin thide *) Definition conj' := (conj, le_n). +(* end thide *) (* end hide *) Print length_is_2. @@ -674,7 +686,9 @@ (* end thide *) (* begin hide *) +(* begin thide *) Definition e1s := eval1'_subproof. +(* end thide *) (* end hide *) Print eval1'. @@ -812,7 +826,9 @@ Abort. (* begin hide *) +(* begin thide *) Definition boool := bool. +(* end thide *) (* end hide *) (** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove. Luckily, a simpler form suffices, by appealing to the built-in tactic %\index{tactics!congruence}%[congruence], a complete procedure for the theory of equality, uninterpreted functions, and datatype constructors. *) @@ -852,7 +868,9 @@ End forall_and. (* begin hide *) +(* begin thide *) Definition noot := (not, @eq). +(* end thide *) (* end hide *) (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
--- a/src/Match.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/Match.v Fri Jul 27 16:47:28 2012 -0400 @@ -402,7 +402,9 @@ (* EX: Write a list map function in Ltac. *) (* begin hide *) +(* begin thide *) Definition mapp := (map, list). +(* end thide *) (* end hide *) (** We can also use anonymous function expressions and local function definitions in Ltac, as this example of a standard list [map] function shows. *)
--- a/src/MoreDep.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/MoreDep.v Fri Jul 27 16:47:28 2012 -0400 @@ -234,6 +234,12 @@ | Snd _ _ e' => snd (expDenote e') end. +(* begin hide *) +(* begin thide *) +Definition sumboool := sumbool. +(* end thide *) +(* end hide *) + (** Despite the fancy type, the function definition is routine. In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype. The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case. Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type. Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns. We can implement our old favorite, a constant folding function, and prove it correct. It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so. Unsurprisingly, a first attempt leads to a type error. @@ -528,10 +534,6 @@ end. End present. -(* begin hide *) -Definition sigT' := sigT. -(* end hide *) - (** Insertion relies on two balancing operations. It will be useful to give types to these operations using a relative of the subset types from last chapter. While subset types let us pair a value with a proof about that value, here we want to pair a value with another non-proof dependently typed value. The %\index{Gallina terms!sigT}%[sigT] type fills this role. *) Locate "{ _ : _ & _ }".
--- a/src/Reflection.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/Reflection.v Fri Jul 27 16:47:28 2012 -0400 @@ -58,7 +58,9 @@ For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *) (* begin hide *) +(* begin thide *) Definition paartial := partial. +(* end thide *) (* end hide *) Print partial. @@ -161,7 +163,9 @@ Qed. (* begin hide *) +(* begin thide *) Definition tg := (and_ind, or_introl). +(* end thide *) (* end hide *) Print true_galore. @@ -560,7 +564,9 @@ Qed. (* begin hide *) +(* begin thide *) Definition nvm := (Node_vm, Empty_vm, End_idx, Left_idx, Right_idx). +(* end thide *) (* end hide *) Print mt2. @@ -624,7 +630,9 @@ Qed. (* begin hide *) +(* begin thide *) Definition fi := False_ind. +(* end thide *) (* end hide *) Print mt4'.
--- a/src/Subset.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/Subset.v Fri Jul 27 16:47:28 2012 -0400 @@ -29,10 +29,6 @@ (** Let us consider several ways of implementing the natural number predecessor function. We start by displaying the definition from the standard library: *) -(* begin hide *) -Definition foo := pred. -(* end hide *) - Print pred. (** %\vspace{-.15in}% [[ pred = fun n : nat => match n with @@ -147,7 +143,9 @@ We can reimplement our dependently typed [pred] based on%\index{subset types}% _subset types_, defined in the standard library with the type family %\index{Gallina terms!sig}%[sig]. *) (* begin hide *) -Definition bar := (sig, ex). +(* begin thide *) +Definition bar := ex. +(* end thide *) (* end hide *) Print sig. @@ -219,7 +217,9 @@ *) (* begin hide *) +(* begin thide *) Definition pred_strong := 0. +(* end thide *) (* end hide *) (** The function %\index{Gallina terms!proj1\_sig}%[proj1_sig] extracts the base value from a subset type. It turns out that we need to include an explicit [return] clause here, since Coq's heuristics are not smart enough to propagate the result type that we wrote earlier. @@ -386,10 +386,6 @@ (** There is another type in the standard library which captures the idea of program values that indicate which of two propositions is true.%\index{Gallina terms!sumbool}% *) -(* begin hide *) -Definition baz := sumbool. -(* end hide *) - Print sumbool. (** %\vspace{-.15in}% [[ Inductive sumbool (A : Prop) (B : Prop) : Set := @@ -607,10 +603,6 @@ Because we used [maybe], one valid implementation of the type we gave [pred_strong7] would return [??] in every case. We can strengthen the type to rule out such vacuous implementations, and the type family %\index{Gallina terms!sumor}%[sumor] from the standard library provides the easiest starting point. For type [A] and proposition [B], [A + {B}] desugars to [sumor A B], whose values are either values of [A] or proofs of [B]. *) -(* begin hide *) -Definition sumor' := sumor. -(* end hide *) - Print sumor. (** %\vspace{-.15in}% [[ Inductive sumor (A : Type) (B : Prop) : Type :=
--- a/src/Universes.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/Universes.v Fri Jul 27 16:47:28 2012 -0400 @@ -272,8 +272,10 @@ 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. *) (* begin hide *) +(* begin thide *) Inductive prod := pair. Reset prod. +(* end thide *) (* end hide *) (** [[ @@ -477,7 +479,9 @@ end. (* begin hide *) +(* begin thide *) Definition projE := O. +(* end thide *) (* end hide *) (** We run into trouble with a version that has been changed to work with [ex]. @@ -777,7 +781,9 @@ Qed. (* begin hide *) +(* begin thide *) Require Eqdep_dec. +(* end thide *) (* end hide *) (** These corollaries are special cases of proof irrelevance. In developments that only need proof irrelevance for equality, there is no need to assert full irrelevance. @@ -849,7 +855,9 @@ This axiom lets us convert a relational specification [R] into a function implementing that specification. We need only prove that [R] is truly a function. An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs. We also simplify the statement of the theorem by considering only non-dependent function types. *) (* begin hide *) +(* begin thide *) Require RelationalChoice. +(* end thide *) (* end hide *) Require Import ClassicalChoice. @@ -967,7 +975,9 @@ (* begin hide *) Require Import JMeq. +(* begin thide *) Definition jme := (JMeq, JMeq_eq). +(* end thide *) (* end hide *) Print Assumptions fin_cases. @@ -1088,7 +1098,9 @@ injection H1; intros. (* begin hide *) +(* begin thide *) Definition existT' := existT. +(* end thide *) (* end hide *) (** Unfortunately, the "equality" that we expected between [p] and [p0] comes in a strange form: