Mercurial > cpdt > repo

comparison src/Subset.v @ 437:8077352044b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 393b8ed99c2f
comparison
equal deleted inserted replaced
436:5d5e44f905c7 437:8077352044b2
27 27
28 (** * Introducing Subset Types *) 28 (** * Introducing Subset Types *)
29 29
30 (** Let us consider several ways of implementing the natural number predecessor function. We start by displaying the definition from the standard library: *) 30 (** Let us consider several ways of implementing the natural number predecessor function. We start by displaying the definition from the standard library: *)
31 31
32 (* begin hide *)
33 Definition foo := pred.
34 (* end hide *)
35
36 Print pred. 32 Print pred.
37 (** %\vspace{-.15in}% [[ 33 (** %\vspace{-.15in}% [[
38 pred = fun n : nat => match n with 34 pred = fun n : nat => match n with
39 | 0 => 0 35 | 0 => 0
40 | S u => u 36 | S u => u
145 (** The proof argument has disappeared! We get exactly the OCaml code we would have written manually. This is our first demonstration of the main technically interesting feature of Coq program extraction: program components of type [Prop] are erased systematically. 141 (** The proof argument has disappeared! We get exactly the OCaml code we would have written manually. This is our first demonstration of the main technically interesting feature of Coq program extraction: program components of type [Prop] are erased systematically.
146 142
147 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]. *) 143 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]. *)
148 144
149 (* begin hide *) 145 (* begin hide *)
150 Definition bar := (sig, ex). 146 (* begin thide *)
147 Definition bar := ex.
148 (* end thide *)
151 (* end hide *) 149 (* end hide *)
152 150
153 Print sig. 151 Print sig.
154 (** %\vspace{-.15in}% [[ 152 (** %\vspace{-.15in}% [[
155 Inductive sig (A : Type) (P : A -> Prop) : Type := 153 Inductive sig (A : Type) (P : A -> Prop) : Type :=
217 : {m : nat | proj1_sig (exist (lt 0) 2 two_gt0) = S m} 215 : {m : nat | proj1_sig (exist (lt 0) 2 two_gt0) = S m}
218 ]] 216 ]]
219 *) 217 *)
220 218
221 (* begin hide *) 219 (* begin hide *)
220 (* begin thide *)
222 Definition pred_strong := 0. 221 Definition pred_strong := 0.
222 (* end thide *)
223 (* end hide *) 223 (* end hide *)
224 224
225 (** 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. 225 (** 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.
226 226
227 By now, the reader is probably ready to believe that the new [pred_strong] leads to the same OCaml code as we have seen several times so far, and Coq does not disappoint. *) 227 By now, the reader is probably ready to believe that the new [pred_strong] leads to the same OCaml code as we have seen several times so far, and Coq does not disappoint. *)
384 384
385 (** * Decidable Proposition Types *) 385 (** * Decidable Proposition Types *)
386 386
387 (** 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}% *) 387 (** 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}% *)
388 388
389 (* begin hide *)
390 Definition baz := sumbool.
391 (* end hide *)
392
393 Print sumbool. 389 Print sumbool.
394 (** %\vspace{-.15in}% [[ 390 (** %\vspace{-.15in}% [[
395 Inductive sumbool (A : Prop) (B : Prop) : Set := 391 Inductive sumbool (A : Prop) (B : Prop) : Set :=
396 left : A -> {A} + {B} | right : B -> {A} + {B} 392 left : A -> {A} + {B} | right : B -> {A} + {B}
397 ]] 393 ]]
604 = ?? 600 = ??
605 : {{m | 0 = S m}} 601 : {{m | 0 = S m}}
606 ]] 602 ]]
607 603
608 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]. *) 604 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]. *)
609
610 (* begin hide *)
611 Definition sumor' := sumor.
612 (* end hide *)
613 605
614 Print sumor. 606 Print sumor.
615 (** %\vspace{-.15in}% [[ 607 (** %\vspace{-.15in}% [[
616 Inductive sumor (A : Type) (B : Prop) : Type := 608 Inductive sumor (A : Type) (B : Prop) : Type :=
617 inleft : A -> A + {B} | inright : B -> A + {B} 609 inleft : A -> A + {B} | inright : B -> A + {B}