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