Mercurial > cpdt > repo

comparison src/Predicates.v @ 203:71ade09024ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quibbly note on [eq] in first-order logic
author Adam Chlipala <adamc@hcoop.net>
date Sun, 04 Jan 2009 08:18:59 -0500
parents 8caa3b3f8fc0
children f05514cc6c0d
comparison
equal deleted inserted replaced
202:8caa3b3f8fc0 203:71ade09024ac
352 352
353 Inductive ex (A : Type) (P : A -> Prop) : Prop := 353 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
354 ex_intro : forall x : A, P x -> ex P 354 ex_intro : forall x : A, P x -> ex P
355 ]] *) 355 ]] *)
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. 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. *)
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.) *)