Mercurial > cpdt > repo
comparison src/Subset.v @ 426:5f25705a10ea
Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 25 Jul 2012 18:10:26 -0400 |
| parents | d3a40c044ab4 |
| children | 5d5e44f905c7 |
comparison
equal
deleted
inserted
replaced
| 425:6ed5ee4845e4 | 426:5f25705a10ea |
|---|---|
| 206 We can continue on in the process of refining [pred]'s type. Let us change its result type to capture that the output is really the predecessor of the input. *) | 206 We can continue on in the process of refining [pred]'s type. Let us change its result type to capture that the output is really the predecessor of the input. *) |
| 207 | 207 |
| 208 Definition pred_strong3 (s : {n : nat | n > 0}) : {m : nat | proj1_sig s = S m} := | 208 Definition pred_strong3 (s : {n : nat | n > 0}) : {m : nat | proj1_sig s = S m} := |
| 209 match s return {m : nat | proj1_sig s = S m} with | 209 match s return {m : nat | proj1_sig s = S m} with |
| 210 | exist 0 pf => match zgtz pf with end | 210 | exist 0 pf => match zgtz pf with end |
| 211 | exist (S n') pf => exist _ n' (refl_equal _) | 211 | exist (S n') pf => exist _ n' (eq_refl _) |
| 212 end. | 212 end. |
| 213 | 213 |
| 214 Eval compute in pred_strong3 (exist _ 2 two_gt0). | 214 Eval compute in pred_strong3 (exist _ 2 two_gt0). |
| 215 (** %\vspace{-.15in}% [[ | 215 (** %\vspace{-.15in}% [[ |
| 216 = exist (fun m : nat => 2 = S m) 1 (refl_equal 2) | 216 = exist (fun m : nat => 2 = S m) 1 (eq_refl 2) |
| 217 : {m : nat | proj1_sig (exist (lt 0) 2 two_gt0) = S m} | 217 : {m : nat | proj1_sig (exist (lt 0) 2 two_gt0) = S m} |
| 218 ]] | 218 ]] |
| 219 *) | 219 *) |
| 220 | 220 |
| 221 (* begin hide *) | 221 (* begin hide *) |
| 296 (Bool.absurd_eq_true false | 296 (Bool.absurd_eq_true false |
| 297 (Bool.diff_false_true | 297 (Bool.diff_false_true |
| 298 (Bool.absurd_eq_true false (pred_strong4_subproof n _))))) | 298 (Bool.absurd_eq_true false (pred_strong4_subproof n _))))) |
| 299 | S n' => | 299 | S n' => |
| 300 fun _ : S n' > 0 => | 300 fun _ : S n' > 0 => |
| 301 exist (fun m : nat => S n' = S m) n' (refl_equal (S n')) | 301 exist (fun m : nat => S n' = S m) n' (eq_refl (S n')) |
| 302 end | 302 end |
| 303 : forall n : nat, n > 0 -> {m : nat | n = S m} | 303 : forall n : nat, n > 0 -> {m : nat | n = S m} |
| 304 | 304 |
| 305 ]] | 305 ]] |
| 306 | 306 |
| 307 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. *) | 307 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. *) |
| 308 | 308 |
| 309 Eval compute in pred_strong4 two_gt0. | 309 Eval compute in pred_strong4 two_gt0. |
| 310 (** %\vspace{-.15in}% [[ | 310 (** %\vspace{-.15in}% [[ |
| 311 = exist (fun m : nat => 2 = S m) 1 (refl_equal 2) | 311 = exist (fun m : nat => 2 = S m) 1 (eq_refl 2) |
| 312 : {m : nat | 2 = S m} | 312 : {m : nat | 2 = S m} |
| 313 ]] | 313 ]] |
| 314 | 314 |
| 315 A tactic modifier called %\index{tactics!abstract}%[abstract] can be helpful for producing shorter terms, by automatically abstracting subgoals into named lemmas. *) | 315 A tactic modifier called %\index{tactics!abstract}%[abstract] can be helpful for producing shorter terms, by automatically abstracting subgoals into named lemmas. *) |
| 316 | 316 |