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
494:07f2fb4d9b36 495:b7419a10e52e
159 159
160 We rewrite [pred_strong1], using some syntactic sugar for subset types. *) 160 We rewrite [pred_strong1], using some syntactic sugar for subset types. *)
161 161
162 Locate "{ _ : _ | _ }". 162 Locate "{ _ : _ | _ }".
163 (** %\vspace{-.15in}% [[ 163 (** %\vspace{-.15in}% [[
164 Notation 164 Notation
165 "{ x : A | P }" := sig (fun x : A => P) 165 "{ x : A | P }" := sig (fun x : A => P)
166 ]] 166 ]]
167 *) 167 *)
168 168
169 Definition pred_strong2 (s : {n : nat | n > 0}) : nat := 169 Definition pred_strong2 (s : {n : nat | n > 0}) : nat :=
170 match s with 170 match s with
171 | exist O pf => match zgtz pf with end 171 | exist O pf => match zgtz pf with end
206 Definition pred_strong3 (s : {n : nat | n > 0}) : {m : nat | proj1_sig s = S m} := 206 Definition pred_strong3 (s : {n : nat | n > 0}) : {m : nat | proj1_sig s = S m} :=
207 match s return {m : nat | proj1_sig s = S m} with 207 match s return {m : nat | proj1_sig s = S m} with
208 | exist 0 pf => match zgtz pf with end 208 | exist 0 pf => match zgtz pf with end
209 | exist (S n') pf => exist _ n' (eq_refl _) 209 | exist (S n') pf => exist _ n' (eq_refl _)
210 end. 210 end.
211
212 (* begin hide *)
213 (* begin thide *)
214 Definition ugh := lt.
215 (* end thide *)
216 (* end hide *)
211 217
212 Eval compute in pred_strong3 (exist _ 2 two_gt0). 218 Eval compute in pred_strong3 (exist _ 2 two_gt0).
213 (** %\vspace{-.15in}% [[ 219 (** %\vspace{-.15in}% [[
214 = exist (fun m : nat => 2 = S m) 1 (eq_refl 2) 220 = exist (fun m : nat => 2 = S m) 1 (eq_refl 2)
215 : {m : nat | proj1_sig (exist (lt 0) 2 two_gt0) = S m} 221 : {m : nat | proj1_sig (exist (lt 0) 2 two_gt0) = S m}
368 match n with 374 match n with
369 | O => _ 375 | O => _
370 | S n' => n' 376 | S n' => n'
371 end. 377 end.
372 378
373 (** 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. *) 379 (** 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. *)
374 380
375 Eval compute in pred_strong6 two_gt0. 381 Eval compute in pred_strong6 two_gt0.
376 (** %\vspace{-.15in}% [[ 382 (** %\vspace{-.15in}% [[
377 = [1] 383 = [1]
378 : {m : nat | 2 = S m} 384 : {m : nat | 2 = S m}
381 In this case, we see that the new definition yields the same computational behavior as before. *) 387 In this case, we see that the new definition yields the same computational behavior as before. *)
382 388
383 389
384 (** * Decidable Proposition Types *) 390 (** * Decidable Proposition Types *)
385 391
386 (** 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}% *) 392 (** 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}% *)
387 393
388 Print sumbool. 394 Print sumbool.
389 (** %\vspace{-.15in}% [[ 395 (** %\vspace{-.15in}% [[
390 Inductive sumbool (A : Prop) (B : Prop) : Set := 396 Inductive sumbool (A : Prop) (B : Prop) : Set :=
391 left : A -> {A} + {B} | right : B -> {A} + {B} 397 left : A -> {A} + {B} | right : B -> {A} + {B}