Mercurial > cpdt > repo

changeset 445:0650420c127b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finished vertical spacing
author Adam Chlipala <adam@chlipala.net>
date Wed, 01 Aug 2012 17:31:56 -0400
parents 0d66f1a710b8
children a0c604da96d3
files src/Large.v src/LogicProg.v src/Match.v src/Reflection.v staging/updates.rss
diffstat 5 files changed, 14 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/src/Large.v	Wed Aug 01 17:03:39 2012 -0400
+++ b/src/Large.v	Wed Aug 01 17:31:56 2012 -0400
@@ -193,7 +193,6 @@
 Error: Expects a disjunctive pattern with 3 branches.
 >>
   *)
-
 Abort.
 
 (** Unsurprisingly, the old proof fails, because it explicitly says that there are two inductive cases.  To update the script, we must, at a minimum, remember the order in which the inductive cases are generated, so that we can insert the new case in the appropriate place.  Even then, it will be painful to add the case, because we cannot walk through proof steps interactively when they occur inside an explicit set of cases. *)
@@ -562,8 +561,7 @@
     (** <<
 Finished transaction in 2. secs (1.264079u,0.s)
       >>
-
-      Why has the search time gone up so much?  The [info] command is not much help, since it only shows the result of search, not all of the paths that turned out to be worthless. *)
+      %\vspace{-.15in}%Why has the search time gone up so much?  The [info] command is not much help, since it only shows the result of search, not all of the paths that turned out to be worthless. *)
 
 (* begin thide *)
     Restart.
--- a/src/LogicProg.v	Wed Aug 01 17:03:39 2012 -0400
+++ b/src/LogicProg.v	Wed Aug 01 17:31:56 2012 -0400
@@ -946,7 +946,6 @@
     Lemma f_f_f' : forall x, f (f (f x)) = f x.
       intros; autorewrite with core.
       (** [[
-
   ============================
    g (g (g x)) = g x
 
--- a/src/Match.v	Wed Aug 01 17:03:39 2012 -0400
+++ b/src/Match.v	Wed Aug 01 17:31:56 2012 -0400
@@ -267,12 +267,10 @@
 
   Theorem fo' : forall x, P x -> S x.
 (* begin thide *)
-    (** [[
+    (** %\vspace{-.25in}%[[
     completer'.
- 
     ]]
-
-    Coq loops forever at this point.  What went wrong? *)
+    %\vspace{-.15in}%Coq loops forever at this point.  What went wrong? *)
 
   Abort.
 (* end thide *)
@@ -292,7 +290,7 @@
 
 (* begin thide *)
 Theorem t1' : forall x : nat, x = x.
-(** [[
+(** %\vspace{-.25in}%[[
   match goal with
     | [ |- forall x, ?P ] => trivial
   end.
@@ -320,7 +318,6 @@
 (** Ltac supports quite convenient functional programming, with a Lisp-with-syntax kind of flavor.  However, there are a few syntactic conventions involved in getting programs to be accepted.  The Ltac syntax is optimized for tactic-writing, so one has to deal with some inconveniences in writing more standard functional programs.
 
    To illustrate, let us try to write a simple list length function.  We start out writing it just like in Gallina, simply replacing [Fixpoint] (and its annotations) with [Ltac].
-
    [[
 Ltac length ls :=
   match ls with
@@ -334,7 +331,6 @@
 >>
 
    At this point, we hopefully remember that pattern variable names must be prefixed by question marks in Ltac.
-
    [[
 Ltac length ls :=
   match ls with
@@ -356,7 +352,7 @@
     | _ :: ?ls' => constr:(S (length ls'))
   end.
 
-(** This definition is accepted.  It can be a little awkward to test Ltac definitions like this.  Here is one method. *)
+(** This definition is accepted.  It can be a little awkward to test Ltac definitions like this one.  Here is one method. *)
 
 Goal False.
   let n := length (1 :: 2 :: 3 :: nil) in
@@ -365,7 +361,6 @@
   n := S (length (2 :: 3 :: nil)) : nat
   ============================
    False
- 
    ]]
 
    We use the %\index{tactics!pose}%[pose] tactic, which extends the proof context with a new variable that is set equal to a particular term.  We could also have used [idtac n] in place of [pose n], which would have printed the result without changing the context.
@@ -889,7 +884,7 @@
 No more subgoals but non-instantiated existential variables :
 Existential 1 =
 >>
-       [[
+       %\vspace{-.35in}%[[
 ?4384 : [A : Type
          B : Type
          Q : A -> Prop
@@ -904,7 +899,6 @@
          H : Q v1
          H0 : Q v2
          H' : Q v2 -> exists u : B, P v2 u |- Q v2] 
- 
          ]]
 
          There is another similar line about a different existential variable.  Here, "existential variable" means what we have also called "unification variable."  In the course of the proof, some unification variable [?4384] was introduced but never unified.  Unification variables are just a device to structure proof search; the language of Gallina proof terms does not include them.  Thus, we cannot produce a proof term without instantiating the variable.
--- a/src/Reflection.v	Wed Aug 01 17:03:39 2012 -0400
+++ b/src/Reflection.v	Wed Aug 01 17:31:56 2012 -0400
@@ -44,7 +44,6 @@
   (Even_SS
      (Even_SS
         (Even_SS
- 
     ]]
 
     %\noindent%...and so on.  This procedure always works (at least on machines with infinite resources), but it has a serious drawback, which we see when we print the proof it generates that 256 is even.  The final proof term has length super-linear in the input value.  Coq's implicit arguments mechanism is hiding the values given for parameter [n] of [Even_SS], which is why the proof term only appears linear here.  Also, proof terms are represented internally as syntax trees, with opportunity for sharing of node representations, but in this chapter we will measure proof term size as simple textual length or as the number of nodes in the term's syntax tree, two measures that are approximately equivalent.  Sometimes apparently large proof terms have enough internal sharing that they take up less memory than we expect, but one avoids having to reason about such sharing by ensuring that the size of a sharing-free version of a term is low enough.
@@ -66,7 +65,6 @@
 Print partial.
 (** %\vspace{-.15in}% [[
 Inductive partial (P : Prop) : Set :=  Proved : P -> [P] | Uncertain : [P]
- 
     ]]
 
     A [partial P] value is an optional proof of [P]. The notation [[P]] stands for [partial P]. *)
@@ -174,7 +172,6 @@
 fun H : True /\ True =>
 and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H
      : True /\ True -> True \/ True /\ (True -> True)
- 
     ]]
 
     As we might expect, the proof that [tauto] builds contains explicit applications of natural deduction rules.  For large formulas, this can add a linear amount of proof size overhead, beyond the size of the input.
@@ -240,7 +237,6 @@
 Qed.
 
 Print true_galore'.
-
 (** %\vspace{-.15in}% [[
 true_galore' = 
 tautTrue
--- a/staging/updates.rss	Wed Aug 01 17:03:39 2012 -0400
+++ b/staging/updates.rss	Wed Aug 01 17:31:56 2012 -0400
@@ -12,6 +12,14 @@
 <docs>http://blogs.law.harvard.edu/tech/rss</docs>
 
 <item>
+        <title>Vertical spacing</title>
+        <pubDate>Wed, 1 Aug 2012 17:29:20 EDT</pubDate>
+        <link>http://adam.chlipala.net/cpdt/</link>
+        <author>adamc@csail.mit.edu</author>
+        <description>This is a mundane revision where I've normalized the vertical space separators between text sections.  Like the last release, this one won't build for LaTeX without a coqdoc patch that may not be in Coq's Subversion repos yet.  This is the home stretch; I am going to make a proofreading pass through everything, and then I'll be looking for other proofreaders to help come up with the final version to be published by MIT Press!</description>
+</item>
+
+<item>
         <title>Taking advantage of coqdoc changes</title>
         <pubDate>Fri, 27 Jul 2012 16:48:35 EDT</pubDate>
         <link>http://adam.chlipala.net/cpdt/</link>