# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1220898535 14400
# Node ID 8788249c7d3a77e7b38a26e7c466d71a9d8cd3a0
# Parent  65314ca099ed3f575e193619b9c3e34e3f3ad2ed
bool

diff -r 65314ca099ed -r 8788249c7d3a src/InductiveTypes.v
--- 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
+]] *)