Mercurial > cpdt > repo
changeset 27:8788249c7d3a
bool
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 08 Sep 2008 14:28:55 -0400 |
parents | 65314ca099ed |
children | 0543bbd62843 |
files | src/InductiveTypes.v |
diffstat | 1 files changed, 21 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/src/InductiveTypes.v Mon Sep 08 14:19:50 2008 -0400 +++ b/src/InductiveTypes.v Mon Sep 08 14:28:55 2008 -0400 @@ -121,6 +121,11 @@ | false => true end. +(** An alternative definition desugars to the above: *) + +Definition not' (b : bool) : bool := + if b then false else true. + (** We might want to prove that [not] is its own inverse operation. *) Theorem not_inverse : forall b : bool, not (not b) = b. @@ -150,3 +155,19 @@ Restart. destruct b; reflexivity. Qed. + +(** Another theorem about booleans illustrates another useful tactic. *) + +Theorem not_ineq : forall b : bool, not b <> b. + destruct b; discriminate. +Qed. + +(** [discriminate] is used to prove that two values of an inductive type are not equal, whenever the values are formed with different constructors. In this case, the different constructors are [true] and [false]. + +At this point, it is probably not hard to guess what the underlying induction principle for [bool] is. *) + +Check bool_ind. +(** [[ + +bool_ind : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b +]] *)