Mercurial > cpdt > repo

comparison src/Predicates.v @ 469:b36876d4611e

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 Wed, 26 Sep 2012 16:35:35 -0400
parents 79190c225f1a
children 0df6dde807ab
comparison
equal deleted inserted replaced
468:62475ab7570b 469:b36876d4611e
371 (** %\vspace{-.15in}%[[ 371 (** %\vspace{-.15in}%[[
372 Inductive ex (A : Type) (P : A -> Prop) : Prop := 372 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
373 ex_intro : forall x : A, P x -> ex P 373 ex_intro : forall x : A, P x -> ex P
374 ]] 374 ]]
375 375
376 (Note that here, as always, each [forall] quantifier has the largest possible scope, so that the type of [ex_intro] could also be written [forall x : A, (P x -> ex P)].)
377
376 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. *)
377 379
378 Theorem exist1 : exists x : nat, x + 1 = 2. 380 Theorem exist1 : exists x : nat, x + 1 = 2.
379 (* begin thide *) 381 (* begin thide *)
380 (** remove printing exists *) 382 (** remove printing exists *)
517 ============================ 519 ============================
518 1 + 1 = 4 520 1 + 1 = 4
519 521
520 ]] 522 ]]
521 523
522 What on earth happened here? Internally, [destruct] replaced [1] with a fresh variable, and, trying to be helpful, it also replaced the occurrence of [1] within the unary representation of each number in the goal. This has the net effect of decrementing each of these numbers. *) 524 What on earth happened here? Internally, [destruct] replaced [1] with a fresh variable, and, trying to be helpful, it also replaced the occurrence of [1] within the unary representation of each number in the goal. Then, within the [O] case of the proof, we replace the fresh variable with [O]. This has the net effect of decrementing each of these numbers. *)
523 525
524 Abort. 526 Abort.
525 527
526 (** To see more clearly what is happening, we can consider the type of [isZero]'s induction principle. *) 528 (** To see more clearly what is happening, we can consider the type of [isZero]'s induction principle. *)
527 529