## Mercurial > cpdt > repo

### comparison src/Subset.v @ 495:b7419a10e52e

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

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} |