Mercurial > cpdt > repo

comparison src/Predicates.v @ 470:0df6dde807ab

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Batch of changes based on proofreader feedback
author Adam Chlipala <adam@chlipala.net>
date Tue, 02 Oct 2012 11:34:40 -0400
parents b36876d4611e
children 51a8472aca68
comparison
equal deleted inserted replaced
469:b36876d4611e 470:0df6dde807ab
378 The family [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. We use the equality operator [=], which, depending on the settings in which they learned logic, different people will say either is or is not part of first-order logic. For our purposes, it is. *) 378 The family [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. We use the equality operator [=], which, depending on the settings in which they learned logic, different people will say either is or is not part of first-order logic. For our purposes, it is. *)
379 379
380 Theorem exist1 : exists x : nat, x + 1 = 2. 380 Theorem exist1 : exists x : nat, x + 1 = 2.
381 (* begin thide *) 381 (* begin thide *)
382 (** remove printing exists *) 382 (** remove printing exists *)
383 (** We can start this proof with a tactic %\index{tactics!exists}%[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.) *) 383 (** We can start this proof with a tactic %\index{tactics!exists}%[exists], which should not be confused with the formula constructor shorthand of the same name. %In the version of this document that you are reading, the reverse ``E'' appears instead of the text ``exists'' in formulas.% *)
384 384
385 exists 1. 385 exists 1.
386 386
387 (** The conclusion is replaced with a version using the existential witness that we announced. 387 (** The conclusion is replaced with a version using the existential witness that we announced.
388 388