Certified Programming with Dependent Types: src/Subset.v comparison

comparison src/Subset.v @ 442:89c67796754e

Undo some overzealous vspace tweaks

author	Adam Chlipala <adam@chlipala.net>
date	Wed, 01 Aug 2012 16:09:37 -0400
parents	f923024bd284
children	2740b8a23cce

comparison

equal deleted inserted replaced

-:cbfd23b4364d
+:89c67796754e
 (** %\vspace{-.15in}% [[
 = 1
 : nat
 ]]
-%\smallskip{}%One aspect in particular of the definition of [pred_strong1] may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.
+One aspect in particular of the definition of [pred_strong1] may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.
 %\vspace{-.15in}%[[
 Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=
 match n with
 | O => match zgtz pf with end
 (** %\vspace{-.15in}% [[
 Inductive sig (A : Type) (P : A -> Prop) : Type :=
 exist : forall x : A, P x -> sig P
 ]]
-%\smallskip{}%The family [sig] is a Curry-Howard twin of [ex], except that [sig] is in [Type], while [ex] is in [Prop].  That means that [sig] values can survive extraction, while [ex] proofs will always be erased.  The actual details of extraction of [sig]s are more subtle, as we will see shortly.
+The family [sig] is a Curry-Howard twin of [ex], except that [sig] is in [Type], while [ex] is in [Prop].  That means that [sig] values can survive extraction, while [ex] proofs will always be erased.  The actual details of extraction of [sig]s are more subtle, as we will see shortly.
 We rewrite [pred_strong1], using some syntactic sugar for subset types. *)
 Locate "{ _ : _ | _ }".
 (** %\vspace{-.15in}% [[
 exist (fun m : nat => S n' = S m) n' (eq_refl (S n'))
 end
 : forall n : nat, n > 0 -> {m : nat | n = S m}
 ]]
-%\smallskip{}%We see the code we entered, with some proofs filled in.  The first proof obligation, the second argument to [False_rec], is filled in with a nasty-looking proof term that we can be glad we did not enter by hand.  The second proof obligation is a simple reflexivity proof. *)
+We see the code we entered, with some proofs filled in.  The first proof obligation, the second argument to [False_rec], is filled in with a nasty-looking proof term that we can be glad we did not enter by hand.  The second proof obligation is a simple reflexivity proof. *)
 Eval compute in pred_strong4 two_gt0.
 (** %\vspace{-.15in}% [[
 = exist (fun m : nat => 2 = S m) 1 (eq_refl 2)
 : {m : nat | 2 = S m}
 ]]
-%\smallskip{}%A tactic modifier called %\index{tactics!abstract}%[abstract] can be helpful for producing shorter terms, by automatically abstracting subgoals into named lemmas. *)
+A tactic modifier called %\index{tactics!abstract}%[abstract] can be helpful for producing shorter terms, by automatically abstracting subgoals into named lemmas. *)
 (* begin thide *)
 Definition pred_strong4' : forall n : nat, n > 0 -> {m : nat | n = S m}.
 refine (fun n =>
 match n with
 (** %\vspace{-.15in}% [[
 = [1]
 : {m : nat | 2 = S m}
 ]]
-%\smallskip{}%One other alternative is worth demonstrating.  Recent Coq versions include a facility called %\index{Program}%[Program] that streamlines this style of definition.  Here is a complete implementation using [Program].%\index{Vernacular commands!Obligation Tactic}\index{Vernacular commands!Program Definition}% *)
+One other alternative is worth demonstrating.  Recent Coq versions include a facility called %\index{Program}%[Program] that streamlines this style of definition.  Here is a complete implementation using [Program].%\index{Vernacular commands!Obligation Tactic}\index{Vernacular commands!Program Definition}% *)
 Obligation Tactic := crush.
 Program Definition pred_strong6 (n : nat) (_ : n > 0) : {m : nat | n = S m} :=
 match n with
 (** %\vspace{-.15in}% [[
 = [1]
 : {m : nat | 2 = S m}
 ]]
-%\smallskip{}%In this case, we see that the new definition yields the same computational behavior as before. *)
+In this case, we see that the new definition yields the same computational behavior as before. *)
 (** * Decidable Proposition Types *)
 (** 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}% *)
 (** %\vspace{-.15in}% [[
 = No
 : {2 = 3} + {2 <> 3}
 ]]
-%\smallskip{}%Note that the %\coqdocnotation{%#<tt>#Yes#</tt>#%}% and %\coqdocnotation{%#<tt>#No#</tt>#%}% notations are hiding proofs establishing the correctness of the outputs.
+Note that the %\coqdocnotation{%#<tt>#Yes#</tt>#%}% and %\coqdocnotation{%#<tt>#No#</tt>#%}% notations are hiding proofs establishing the correctness of the outputs.
 Our definition extracts to reasonable OCaml code. *)
 Extraction eq_nat_dec.
 (** %\vspace{-.15in}% [[
 = No
 : {In 3 (1 :: 2 :: nil)} + {~ In 3 (1 :: 2 :: nil)}
 ]]
-%\smallskip{}%[In_dec] has a reasonable extraction to OCaml. *)
+[In_dec] has a reasonable extraction to OCaml. *)
 Extraction In_dec.
 (* end thide *)
 (** %\begin{verbatim}
 (** %\vspace{-.15in}% [[
 = ??
 : {{m | 0 = S m}}
 ]]
-%\smallskip{}%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]. *)
+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]. *)
 Print sumor.
 (** %\vspace{-.15in}% [[
 Inductive sumor (A : Type) (B : Prop) : Type :=
 inleft : A -> A + {B} | inright : B -> A + {B}
 ]]
-%\smallskip{}%We add notations for easy use of the [sumor] constructors.  The second notation is specialized to [sumor]s whose [A] parameters are instantiated with regular subset types, since this is how we will use [sumor] below. *)
+We add notations for easy use of the [sumor] constructors.  The second notation is specialized to [sumor]s whose [A] parameters are instantiated with regular subset types, since this is how we will use [sumor] below. *)
 Notation "!!" := (inright _ _).
 Notation "[|| x ||]" := (inleft _ [x]).
 (** Now we are ready to give the final version of possibly failing predecessor.  The [sumor]-based type that we use is maximally expressive; any implementation of the type has the same input-output behavior. *)
 (** %\vspace{-.15in}% [[
 = ??
 : {{t | hasType (Plus (Nat 1) (Bool false)) t}}
 ]]
-%\smallskip{}%The type checker also extracts to some reasonable OCaml code. *)
+The type checker also extracts to some reasonable OCaml code. *)
 Extraction typeCheck.
 (** %\begin{verbatim}
 (** val typeCheck : exp -> type0 maybe **)
 = !!
 : {t : type | hasType (Plus (Nat 1) (Bool false)) t} +
 {(forall t : type, ~ hasType (Plus (Nat 1) (Bool false)) t)}
 ]]
-%\smallskip{}%The results of simplifying calls to [typeCheck'] look deceptively similar to the results for [typeCheck], but now the types of the results provide more information. *)
+The results of simplifying calls to [typeCheck'] look deceptively similar to the results for [typeCheck], but now the types of the results provide more information. *)

Mercurial > cpdt > repo

comparison src/Subset.v @ 442:89c67796754e