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

comparison src/Subset.v @ 440:f923024bd284

Vertical spacing pass, through end of Subset

author	Adam Chlipala <adam@chlipala.net>
date	Mon, 30 Jul 2012 16:50:02 -0400
parents	393b8ed99c2f
children	89c67796754e

comparison

equal deleted inserted replaced

-:393b8ed99c2f
+:f923024bd284
 Eval compute in pred_strong1 two_gt0.
 (** %\vspace{-.15in}% [[
 = 1
 : nat
 ]]
-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.
+%\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.
-[[
+%\vspace{-.15in}%[[
 Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=
 match n with
 | O => match zgtz pf with end
 | S n' => n'
 end.
 Print sig.
 (** %\vspace{-.15in}% [[
 Inductive sig (A : Type) (P : A -> Prop) : Type :=
 exist : forall x : A, P x -> sig P
 ]]
-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.
+%\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.
 We rewrite [pred_strong1], using some syntactic sugar for subset types. *)
 Locate "{ _ : _ | _ }".
 (** %\vspace{-.15in}% [[
 | S n' =>
 fun _ : S n' > 0 =>
 exist (fun m : nat => S n' = S m) n' (eq_refl (S n'))
 end
 : forall n : nat, n > 0 -> {m : nat | n = S m}
 ]]
-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. *)
+%\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. *)
 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}
 ]]
-A tactic modifier called %\index{tactics!abstract}%[abstract] can be helpful for producing shorter terms, by automatically abstracting subgoals into named lemmas. *)
+%\smallskip{}%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}
 ]]
-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}% *)
+%\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}% *)
 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}
 ]]
-In this case, we see that the new definition yields the same computational behavior as before. *)
+%\smallskip{}%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}% *)
 Eval compute in eq_nat_dec 2 3.
 (** %\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.
 Eval compute in In_dec eq_nat_dec 3 (1 :: 2 :: nil).
 (** %\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}}
 ]]
-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]. *)
+%\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]. *)
 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. *)
 Eval simpl in typeCheck (Plus (Nat 1) (Bool false)).
 (** %\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)}
 ]]
-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. *)
+%\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. *)

Mercurial > cpdt > repo

comparison src/Subset.v @ 440:f923024bd284