1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#**********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
25 (* \VV/ *************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#**********************************************************************)
33 (*i $Id: Bool.v,v 1.29 2004/02/12 16:03:01 herbelin Exp $ i*)
37 (*#* The type [bool] is defined in the prelude as
38 [Inductive bool : Set := true : bool | false : bool] *)
40 (*#* Interpretation of booleans as Proposition *)
42 inline procedural "cic:/Coq/Bool/Bool/Is_true.con" as definition.
45 Hint Unfold Is_true: bool.
48 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_left.con" as lemma.
50 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_right.con" as lemma.
53 Hint Immediate Is_true_eq_right Is_true_eq_left: bool.
56 (*#******************)
58 (*#* Discrimination *)
60 (*#******************)
62 inline procedural "cic:/Coq/Bool/Bool/diff_true_false.con" as lemma.
65 Hint Resolve diff_true_false: bool v62.
68 inline procedural "cic:/Coq/Bool/Bool/diff_false_true.con" as lemma.
71 Hint Resolve diff_false_true: bool v62.
74 inline procedural "cic:/Coq/Bool/Bool/eq_true_false_abs.con" as lemma.
77 Hint Resolve eq_true_false_abs: bool.
80 inline procedural "cic:/Coq/Bool/Bool/not_true_is_false.con" as lemma.
82 inline procedural "cic:/Coq/Bool/Bool/not_false_is_true.con" as lemma.
84 (*#*********************)
86 (*#* Order on booleans *)
88 (*#*********************)
90 inline procedural "cic:/Coq/Bool/Bool/leb.con" as definition.
93 Hint Unfold leb: bool v62.
102 inline procedural "cic:/Coq/Bool/Bool/eqb.con" as definition.
104 inline procedural "cic:/Coq/Bool/Bool/eqb_refl.con" as lemma.
106 inline procedural "cic:/Coq/Bool/Bool/eqb_eq.con" as lemma.
108 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_true.con" as lemma.
110 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_true2.con" as lemma.
112 inline procedural "cic:/Coq/Bool/Bool/eqb_subst.con" as lemma.
114 inline procedural "cic:/Coq/Bool/Bool/eqb_reflx.con" as lemma.
116 inline procedural "cic:/Coq/Bool/Bool/eqb_prop.con" as lemma.
118 (*#***********************)
120 (*#* Logical combinators *)
122 (*#***********************)
124 inline procedural "cic:/Coq/Bool/Bool/ifb.con" as definition.
126 inline procedural "cic:/Coq/Bool/Bool/andb.con" as definition.
128 inline procedural "cic:/Coq/Bool/Bool/orb.con" as definition.
130 inline procedural "cic:/Coq/Bool/Bool/implb.con" as definition.
132 inline procedural "cic:/Coq/Bool/Bool/xorb.con" as definition.
134 inline procedural "cic:/Coq/Bool/Bool/negb.con" as definition.
137 Infix "||" := orb (at level 50, left associativity) : bool_scope.
141 Infix "&&" := andb (at level 40, left associativity) : bool_scope.
145 Open Scope bool_scope.
149 Delimit Scope bool_scope with bool.
153 Bind Scope bool_scope with bool.
156 (*#*************************)
158 (*#* Lemmas about [negb] *)
160 (*#*************************)
162 inline procedural "cic:/Coq/Bool/Bool/negb_intro.con" as lemma.
164 inline procedural "cic:/Coq/Bool/Bool/negb_elim.con" as lemma.
166 inline procedural "cic:/Coq/Bool/Bool/negb_orb.con" as lemma.
168 inline procedural "cic:/Coq/Bool/Bool/negb_andb.con" as lemma.
170 inline procedural "cic:/Coq/Bool/Bool/negb_sym.con" as lemma.
172 inline procedural "cic:/Coq/Bool/Bool/no_fixpoint_negb.con" as lemma.
174 inline procedural "cic:/Coq/Bool/Bool/eqb_negb1.con" as lemma.
176 inline procedural "cic:/Coq/Bool/Bool/eqb_negb2.con" as lemma.
178 inline procedural "cic:/Coq/Bool/Bool/if_negb.con" as lemma.
180 (*#***************************)
182 (*#* A few lemmas about [or] *)
184 (*#***************************)
186 inline procedural "cic:/Coq/Bool/Bool/orb_prop.con" as lemma.
188 inline procedural "cic:/Coq/Bool/Bool/orb_prop2.con" as lemma.
190 inline procedural "cic:/Coq/Bool/Bool/orb_true_intro.con" as lemma.
193 Hint Resolve orb_true_intro: bool v62.
196 inline procedural "cic:/Coq/Bool/Bool/orb_b_true.con" as lemma.
199 Hint Resolve orb_b_true: bool v62.
202 inline procedural "cic:/Coq/Bool/Bool/orb_true_b.con" as lemma.
204 inline procedural "cic:/Coq/Bool/Bool/orb_true_elim.con" as definition.
206 inline procedural "cic:/Coq/Bool/Bool/orb_false_intro.con" as lemma.
209 Hint Resolve orb_false_intro: bool v62.
212 inline procedural "cic:/Coq/Bool/Bool/orb_b_false.con" as lemma.
215 Hint Resolve orb_b_false: bool v62.
218 inline procedural "cic:/Coq/Bool/Bool/orb_false_b.con" as lemma.
221 Hint Resolve orb_false_b: bool v62.
224 inline procedural "cic:/Coq/Bool/Bool/orb_false_elim.con" as lemma.
226 inline procedural "cic:/Coq/Bool/Bool/orb_neg_b.con" as lemma.
229 Hint Resolve orb_neg_b: bool v62.
232 inline procedural "cic:/Coq/Bool/Bool/orb_comm.con" as lemma.
234 inline procedural "cic:/Coq/Bool/Bool/orb_assoc.con" as lemma.
237 Hint Resolve orb_comm orb_assoc orb_b_false orb_false_b: bool v62.
240 (*#****************************)
242 (*#* A few lemmas about [and] *)
244 (*#****************************)
246 inline procedural "cic:/Coq/Bool/Bool/andb_prop.con" as lemma.
249 Hint Resolve andb_prop: bool v62.
252 inline procedural "cic:/Coq/Bool/Bool/andb_true_eq.con" as definition.
254 inline procedural "cic:/Coq/Bool/Bool/andb_prop2.con" as lemma.
257 Hint Resolve andb_prop2: bool v62.
260 inline procedural "cic:/Coq/Bool/Bool/andb_true_intro.con" as lemma.
263 Hint Resolve andb_true_intro: bool v62.
266 inline procedural "cic:/Coq/Bool/Bool/andb_true_intro2.con" as lemma.
269 Hint Resolve andb_true_intro2: bool v62.
272 inline procedural "cic:/Coq/Bool/Bool/andb_false_intro1.con" as lemma.
274 inline procedural "cic:/Coq/Bool/Bool/andb_false_intro2.con" as lemma.
276 inline procedural "cic:/Coq/Bool/Bool/andb_b_false.con" as lemma.
278 inline procedural "cic:/Coq/Bool/Bool/andb_false_b.con" as lemma.
280 inline procedural "cic:/Coq/Bool/Bool/andb_b_true.con" as lemma.
282 inline procedural "cic:/Coq/Bool/Bool/andb_true_b.con" as lemma.
284 inline procedural "cic:/Coq/Bool/Bool/andb_false_elim.con" as definition.
287 Hint Resolve andb_false_elim: bool v62.
290 inline procedural "cic:/Coq/Bool/Bool/andb_neg_b.con" as lemma.
293 Hint Resolve andb_neg_b: bool v62.
296 inline procedural "cic:/Coq/Bool/Bool/andb_comm.con" as lemma.
298 inline procedural "cic:/Coq/Bool/Bool/andb_assoc.con" as lemma.
301 Hint Resolve andb_comm andb_assoc: bool v62.
304 (*#******************************)
306 (*#* Properties of [xorb] *)
308 (*#******************************)
310 inline procedural "cic:/Coq/Bool/Bool/xorb_false.con" as lemma.
312 inline procedural "cic:/Coq/Bool/Bool/false_xorb.con" as lemma.
314 inline procedural "cic:/Coq/Bool/Bool/xorb_true.con" as lemma.
316 inline procedural "cic:/Coq/Bool/Bool/true_xorb.con" as lemma.
318 inline procedural "cic:/Coq/Bool/Bool/xorb_nilpotent.con" as lemma.
320 inline procedural "cic:/Coq/Bool/Bool/xorb_comm.con" as lemma.
322 inline procedural "cic:/Coq/Bool/Bool/xorb_assoc.con" as lemma.
324 inline procedural "cic:/Coq/Bool/Bool/xorb_eq.con" as lemma.
326 inline procedural "cic:/Coq/Bool/Bool/xorb_move_l_r_1.con" as lemma.
328 inline procedural "cic:/Coq/Bool/Bool/xorb_move_l_r_2.con" as lemma.
330 inline procedural "cic:/Coq/Bool/Bool/xorb_move_r_l_1.con" as lemma.
332 inline procedural "cic:/Coq/Bool/Bool/xorb_move_r_l_2.con" as lemma.
334 (*#******************************)
336 (*#* De Morgan's law *)
338 (*#******************************)
340 inline procedural "cic:/Coq/Bool/Bool/demorgan1.con" as lemma.
342 inline procedural "cic:/Coq/Bool/Bool/demorgan2.con" as lemma.
344 inline procedural "cic:/Coq/Bool/Bool/demorgan3.con" as lemma.
346 inline procedural "cic:/Coq/Bool/Bool/demorgan4.con" as lemma.
348 inline procedural "cic:/Coq/Bool/Bool/absoption_andb.con" as lemma.
350 inline procedural "cic:/Coq/Bool/Bool/absoption_orb.con" as lemma.
352 (*#* Misc. equalities between booleans (to be used by Auto) *)
354 inline procedural "cic:/Coq/Bool/Bool/bool_1.con" as lemma.
356 inline procedural "cic:/Coq/Bool/Bool/bool_2.con" as lemma.
358 inline procedural "cic:/Coq/Bool/Bool/bool_3.con" as lemma.
360 inline procedural "cic:/Coq/Bool/Bool/bool_4.con" as lemma.
362 inline procedural "cic:/Coq/Bool/Bool/bool_5.con" as lemma.
364 inline procedural "cic:/Coq/Bool/Bool/bool_6.con" as lemma.
367 Hint Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6.