Mercurial > cpdt > repo
comparison src/Predicates.v @ 67:55199444e5e7
Finish Coinductive chapter
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Wed, 01 Oct 2008 09:56:32 -0400 |
| parents | b581446229fd |
| children | 8caa3b3f8fc0 |
comparison
equal
deleted
inserted
replaced
| 66:b52204928c7d | 67:55199444e5e7 |
|---|---|
| 356 | 356 |
| 357 (** [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s. We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x]. As usual, there are tactics that save us from worrying about the low-level details most of the time. *) | 357 (** [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s. We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x]. As usual, there are tactics that save us from worrying about the low-level details most of the time. *) |
| 358 | 358 |
| 359 Theorem exist1 : exists x : nat, x + 1 = 2. | 359 Theorem exist1 : exists x : nat, x + 1 = 2. |
| 360 (* begin thide *) | 360 (* begin thide *) |
| 361 (** remove printing exists*) | 361 (** remove printing exists *) |
| 362 (** We can start this proof with a tactic [exists], which should not be confused with the formula constructor shorthand of the same name. (In the PDF version of this document, the reverse 'E' appears instead of the text "exists" in formulas.) *) | 362 (** We can start this proof with a tactic [exists], which should not be confused with the formula constructor shorthand of the same name. (In the PDF version of this document, the reverse 'E' appears instead of the text "exists" in formulas.) *) |
| 363 exists 1. | 363 exists 1. |
| 364 | 364 |
| 365 (** The conclusion is replaced with a version using the existential witness that we announced. *) | 365 (** The conclusion is replaced with a version using the existential witness that we announced. *) |
| 366 | 366 |