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

comparison src/Subset.v @ 495:b7419a10e52e

Pass through Chapter 6

author	Adam Chlipala <adam@chlipala.net>
date	Sun, 20 Jan 2013 06:59:34 -0500
parents	1fd4109f7b31
children	8921cfa2f503

comparison

equal deleted inserted replaced

-:07f2fb4d9b36
+:b7419a10e52e
 We rewrite [pred_strong1], using some syntactic sugar for subset types. *)
 Locate "{ _ : _ | _ }".
 (** %\vspace{-.15in}% [[
 Notation
 "{ x : A  |  P }" := sig (fun x : A => P)
 ]]
 *)
 Definition pred_strong2 (s : {n : nat | n > 0}) : nat :=
 match s with
 | exist O pf => match zgtz pf with end
 Definition pred_strong3 (s : {n : nat | n > 0}) : {m : nat | proj1_sig s = S m} :=
 match s return {m : nat | proj1_sig s = S m} with
 | exist 0 pf => match zgtz pf with end
 | exist (S n') pf => exist _ n' (eq_refl _)
 end.
+(* begin hide *)
+(* begin thide *)
+Definition ugh := lt.
+(* end thide *)
+(* end hide *)
 Eval compute in pred_strong3 (exist _ 2 two_gt0).
 (** %\vspace{-.15in}% [[
 = exist (fun m : nat => 2 = S m) 1 (eq_refl 2)
 : {m : nat | proj1_sig (exist (lt 0) 2 two_gt0) = S m}
 match n with
 | O => _
 | S n' => n'
 end.
-(** Printing the resulting definition of [pred_strong6] yields a term very similar to what we built with [refine].  [Program] can save time in writing programs that use subset types.  Nonetheless, [refine] is often just as effective, and [refine] gives you more control over the form the final term takes, which can be useful when you want to prove additional theorems about your definition.  [Program] will sometimes insert type casts that can complicate theorem proving. *)
+(** Printing the resulting definition of [pred_strong6] yields a term very similar to what we built with [refine].  [Program] can save time in writing programs that use subset types.  Nonetheless, [refine] is often just as effective, and [refine] gives more control over the form the final term takes, which can be useful when you want to prove additional theorems about your definition.  [Program] will sometimes insert type casts that can complicate theorem proving. *)
 Eval compute in pred_strong6 two_gt0.
 (** %\vspace{-.15in}% [[
 = [1]
 : {m : nat | 2 = S m}
 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}% *)
+(** There is another type in the standard library that captures the idea of program values that indicate which of two propositions is true.%\index{Gallina terms!sumbool}% *)
 Print sumbool.
 (** %\vspace{-.15in}% [[
 Inductive sumbool (A : Prop) (B : Prop) : Set :=
 left : A -> {A} + {B} | right : B -> {A} + {B}

Mercurial > cpdt > repo

comparison src/Subset.v @ 495:b7419a10e52e