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 include "Init/Prelude.ma".
21 (*#***********************************************************************)
23 (* v * The Coq Proof Assistant / The Coq Development Team *)
25 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
27 (* \VV/ **************************************************************)
29 (* // * This file is distributed under the terms of the *)
31 (* * GNU Lesser General Public License Version 2.1 *)
33 (*#***********************************************************************)
35 (*i $Id: Bool.v,v 1.29.2.1 2004/07/16 19:31:01 herbelin Exp $ i*)
39 (*#* The type [bool] is defined in the prelude as
40 [Inductive bool : Set := true : bool | false : bool] *)
42 (*#* Interpretation of booleans as Proposition *)
44 inline procedural "cic:/Coq/Bool/Bool/Is_true.con" as definition.
47 Hint Unfold Is_true: bool.
50 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_left.con" as lemma.
52 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_right.con" as lemma.
55 Hint Immediate Is_true_eq_right Is_true_eq_left: bool.
58 (*#******************)
60 (*#* Discrimination *)
62 (*#******************)
64 inline procedural "cic:/Coq/Bool/Bool/diff_true_false.con" as lemma.
67 Hint Resolve diff_true_false: bool v62.
70 inline procedural "cic:/Coq/Bool/Bool/diff_false_true.con" as lemma.
73 Hint Resolve diff_false_true: bool v62.
76 inline procedural "cic:/Coq/Bool/Bool/eq_true_false_abs.con" as lemma.
79 Hint Resolve eq_true_false_abs: bool.
82 inline procedural "cic:/Coq/Bool/Bool/not_true_is_false.con" as lemma.
84 inline procedural "cic:/Coq/Bool/Bool/not_false_is_true.con" as lemma.
86 (*#*********************)
88 (*#* Order on booleans *)
90 (*#*********************)
92 inline procedural "cic:/Coq/Bool/Bool/leb.con" as definition.
95 Hint Unfold leb: bool v62.
104 inline procedural "cic:/Coq/Bool/Bool/eqb.con" as definition.
106 inline procedural "cic:/Coq/Bool/Bool/eqb_refl.con" as lemma.
108 inline procedural "cic:/Coq/Bool/Bool/eqb_eq.con" as lemma.
110 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_true.con" as lemma.
112 inline procedural "cic:/Coq/Bool/Bool/Is_true_eq_true2.con" as lemma.
114 inline procedural "cic:/Coq/Bool/Bool/eqb_subst.con" as lemma.
116 inline procedural "cic:/Coq/Bool/Bool/eqb_reflx.con" as lemma.
118 inline procedural "cic:/Coq/Bool/Bool/eqb_prop.con" as lemma.
120 (*#***********************)
122 (*#* Logical combinators *)
124 (*#***********************)
126 inline procedural "cic:/Coq/Bool/Bool/ifb.con" as definition.
128 inline procedural "cic:/Coq/Bool/Bool/andb.con" as definition.
130 inline procedural "cic:/Coq/Bool/Bool/orb.con" as definition.
132 inline procedural "cic:/Coq/Bool/Bool/implb.con" as definition.
134 inline procedural "cic:/Coq/Bool/Bool/xorb.con" as definition.
136 inline procedural "cic:/Coq/Bool/Bool/negb.con" as definition.
139 Infix "||" := orb (at level 50, left associativity) : bool_scope.
143 Infix "&&" := andb (at level 40, left associativity) : bool_scope.
147 Open Scope bool_scope.
151 Delimit Scope bool_scope with bool.
155 Bind Scope bool_scope with bool.
158 (*#*************************)
160 (*#* Lemmas about [negb] *)
162 (*#*************************)
164 inline procedural "cic:/Coq/Bool/Bool/negb_intro.con" as lemma.
166 inline procedural "cic:/Coq/Bool/Bool/negb_elim.con" as lemma.
168 inline procedural "cic:/Coq/Bool/Bool/negb_orb.con" as lemma.
170 inline procedural "cic:/Coq/Bool/Bool/negb_andb.con" as lemma.
172 inline procedural "cic:/Coq/Bool/Bool/negb_sym.con" as lemma.
174 inline procedural "cic:/Coq/Bool/Bool/no_fixpoint_negb.con" as lemma.
176 inline procedural "cic:/Coq/Bool/Bool/eqb_negb1.con" as lemma.
178 inline procedural "cic:/Coq/Bool/Bool/eqb_negb2.con" as lemma.
180 inline procedural "cic:/Coq/Bool/Bool/if_negb.con" as lemma.
182 (*#***************************)
184 (*#* A few lemmas about [or] *)
186 (*#***************************)
188 inline procedural "cic:/Coq/Bool/Bool/orb_prop.con" as lemma.
190 inline procedural "cic:/Coq/Bool/Bool/orb_prop2.con" as lemma.
192 inline procedural "cic:/Coq/Bool/Bool/orb_true_intro.con" as lemma.
195 Hint Resolve orb_true_intro: bool v62.
198 inline procedural "cic:/Coq/Bool/Bool/orb_b_true.con" as lemma.
201 Hint Resolve orb_b_true: bool v62.
204 inline procedural "cic:/Coq/Bool/Bool/orb_true_b.con" as lemma.
206 inline procedural "cic:/Coq/Bool/Bool/orb_true_elim.con" as definition.
208 inline procedural "cic:/Coq/Bool/Bool/orb_false_intro.con" as lemma.
211 Hint Resolve orb_false_intro: bool v62.
214 inline procedural "cic:/Coq/Bool/Bool/orb_b_false.con" as lemma.
217 Hint Resolve orb_b_false: bool v62.
220 inline procedural "cic:/Coq/Bool/Bool/orb_false_b.con" as lemma.
223 Hint Resolve orb_false_b: bool v62.
226 inline procedural "cic:/Coq/Bool/Bool/orb_false_elim.con" as lemma.
228 inline procedural "cic:/Coq/Bool/Bool/orb_neg_b.con" as lemma.
231 Hint Resolve orb_neg_b: bool v62.
234 inline procedural "cic:/Coq/Bool/Bool/orb_comm.con" as lemma.
236 inline procedural "cic:/Coq/Bool/Bool/orb_assoc.con" as lemma.
239 Hint Resolve orb_comm orb_assoc orb_b_false orb_false_b: bool v62.
242 (*#****************************)
244 (*#* A few lemmas about [and] *)
246 (*#****************************)
248 inline procedural "cic:/Coq/Bool/Bool/andb_prop.con" as lemma.
251 Hint Resolve andb_prop: bool v62.
254 inline procedural "cic:/Coq/Bool/Bool/andb_true_eq.con" as definition.
256 inline procedural "cic:/Coq/Bool/Bool/andb_prop2.con" as lemma.
259 Hint Resolve andb_prop2: bool v62.
262 inline procedural "cic:/Coq/Bool/Bool/andb_true_intro.con" as lemma.
265 Hint Resolve andb_true_intro: bool v62.
268 inline procedural "cic:/Coq/Bool/Bool/andb_true_intro2.con" as lemma.
271 Hint Resolve andb_true_intro2: bool v62.
274 inline procedural "cic:/Coq/Bool/Bool/andb_false_intro1.con" as lemma.
276 inline procedural "cic:/Coq/Bool/Bool/andb_false_intro2.con" as lemma.
278 inline procedural "cic:/Coq/Bool/Bool/andb_b_false.con" as lemma.
280 inline procedural "cic:/Coq/Bool/Bool/andb_false_b.con" as lemma.
282 inline procedural "cic:/Coq/Bool/Bool/andb_b_true.con" as lemma.
284 inline procedural "cic:/Coq/Bool/Bool/andb_true_b.con" as lemma.
286 inline procedural "cic:/Coq/Bool/Bool/andb_false_elim.con" as definition.
289 Hint Resolve andb_false_elim: bool v62.
292 inline procedural "cic:/Coq/Bool/Bool/andb_neg_b.con" as lemma.
295 Hint Resolve andb_neg_b: bool v62.
298 inline procedural "cic:/Coq/Bool/Bool/andb_comm.con" as lemma.
300 inline procedural "cic:/Coq/Bool/Bool/andb_assoc.con" as lemma.
303 Hint Resolve andb_comm andb_assoc: bool v62.
306 (*#******************************)
308 (*#* Properties of [xorb] *)
310 (*#******************************)
312 inline procedural "cic:/Coq/Bool/Bool/xorb_false.con" as lemma.
314 inline procedural "cic:/Coq/Bool/Bool/false_xorb.con" as lemma.
316 inline procedural "cic:/Coq/Bool/Bool/xorb_true.con" as lemma.
318 inline procedural "cic:/Coq/Bool/Bool/true_xorb.con" as lemma.
320 inline procedural "cic:/Coq/Bool/Bool/xorb_nilpotent.con" as lemma.
322 inline procedural "cic:/Coq/Bool/Bool/xorb_comm.con" as lemma.
324 inline procedural "cic:/Coq/Bool/Bool/xorb_assoc.con" as lemma.
326 inline procedural "cic:/Coq/Bool/Bool/xorb_eq.con" as lemma.
328 inline procedural "cic:/Coq/Bool/Bool/xorb_move_l_r_1.con" as lemma.
330 inline procedural "cic:/Coq/Bool/Bool/xorb_move_l_r_2.con" as lemma.
332 inline procedural "cic:/Coq/Bool/Bool/xorb_move_r_l_1.con" as lemma.
334 inline procedural "cic:/Coq/Bool/Bool/xorb_move_r_l_2.con" as lemma.
336 (*#******************************)
338 (*#* De Morgan's law *)
340 (*#******************************)
342 inline procedural "cic:/Coq/Bool/Bool/demorgan1.con" as lemma.
344 inline procedural "cic:/Coq/Bool/Bool/demorgan2.con" as lemma.
346 inline procedural "cic:/Coq/Bool/Bool/demorgan3.con" as lemma.
348 inline procedural "cic:/Coq/Bool/Bool/demorgan4.con" as lemma.
350 inline procedural "cic:/Coq/Bool/Bool/absoption_andb.con" as lemma.
352 inline procedural "cic:/Coq/Bool/Bool/absoption_orb.con" as lemma.
354 (*#* Misc. equalities between booleans (to be used by Auto) *)
356 inline procedural "cic:/Coq/Bool/Bool/bool_1.con" as lemma.
358 inline procedural "cic:/Coq/Bool/Bool/bool_2.con" as lemma.
360 inline procedural "cic:/Coq/Bool/Bool/bool_3.con" as lemma.
362 inline procedural "cic:/Coq/Bool/Bool/bool_4.con" as lemma.
364 inline procedural "cic:/Coq/Bool/Bool/bool_5.con" as lemma.
366 inline procedural "cic:/Coq/Bool/Bool/bool_6.con" as lemma.
369 Hint Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6.