Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 27:8788249c7d3a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bool
author Adam Chlipala <adamc@hcoop.net>
date Mon, 08 Sep 2008 14:28:55 -0400
parents 65314ca099ed
children 0543bbd62843
comparison
equal deleted inserted replaced
26:65314ca099ed 27:8788249c7d3a
119 match b with 119 match b with
120 | true => false 120 | true => false
121 | false => true 121 | false => true
122 end. 122 end.
123 123
124 (** An alternative definition desugars to the above: *)
125
126 Definition not' (b : bool) : bool :=
127 if b then false else true.
128
124 (** We might want to prove that [not] is its own inverse operation. *) 129 (** We might want to prove that [not] is its own inverse operation. *)
125 130
126 Theorem not_inverse : forall b : bool, not (not b) = b. 131 Theorem not_inverse : forall b : bool, not (not b) = b.
127 destruct b. 132 destruct b.
128 133
148 (** Likewise for the second subgoal, so we can restart the proof and give a very compact justification. *) 153 (** Likewise for the second subgoal, so we can restart the proof and give a very compact justification. *)
149 154
150 Restart. 155 Restart.
151 destruct b; reflexivity. 156 destruct b; reflexivity.
152 Qed. 157 Qed.
158
159 (** Another theorem about booleans illustrates another useful tactic. *)
160
161 Theorem not_ineq : forall b : bool, not b <> b.
162 destruct b; discriminate.
163 Qed.
164
165 (** [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].
166
167 At this point, it is probably not hard to guess what the underlying induction principle for [bool] is. *)
168
169 Check bool_ind.
170 (** [[
171
172 bool_ind : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
173 ]] *)