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___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
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: BinInt.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ i*)
35 (*#**********************************************************)
37 (*#* Binary Integers (Pierre Cr\233\gut, CNET, Lannion, France) *)
39 (*#**********************************************************)
41 include "NArith/BinPos.ma".
43 include "NArith/Pnat.ma".
45 include "NArith/BinNat.ma".
47 include "Arith/Plus.ma".
49 include "Arith/Mult.ma".
51 (*#*********************************************************************)
53 (*#* Binary integer numbers *)
55 inline procedural "cic:/Coq/ZArith/BinInt/Z.ind".
57 (*#* Declare Scope Z_scope with Key Z *)
60 Delimit Scope Z_scope with Z.
63 (*#* Automatically open scope positive_scope for the constructors of Z *)
66 Bind Scope Z_scope with Z.
70 Arguments Scope Zpos [positive_scope].
74 Arguments Scope Zneg [positive_scope].
77 (*#* Subtraction of positive into Z *)
79 inline procedural "cic:/Coq/ZArith/BinInt/Zdouble_plus_one.con" as definition.
81 inline procedural "cic:/Coq/ZArith/BinInt/Zdouble_minus_one.con" as definition.
83 inline procedural "cic:/Coq/ZArith/BinInt/Zdouble.con" as definition.
85 inline procedural "cic:/Coq/ZArith/BinInt/ZPminus.con" as definition.
87 (*#* Addition on integers *)
89 inline procedural "cic:/Coq/ZArith/BinInt/Zplus.con" as definition.
92 Infix "+" := Zplus : Z_scope.
97 inline procedural "cic:/Coq/ZArith/BinInt/Zopp.con" as definition.
100 Notation "- x" := (Zopp x) : Z_scope.
103 (*#* Successor on integers *)
105 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc.con" as definition.
107 (*#* Predecessor on integers *)
109 inline procedural "cic:/Coq/ZArith/BinInt/Zpred.con" as definition.
111 (*#* Subtraction on integers *)
113 inline procedural "cic:/Coq/ZArith/BinInt/Zminus.con" as definition.
116 Infix "-" := Zminus : Z_scope.
119 (*#* Multiplication on integers *)
121 inline procedural "cic:/Coq/ZArith/BinInt/Zmult.con" as definition.
124 Infix "*" := Zmult : Z_scope.
127 (*#* Comparison of integers *)
129 inline procedural "cic:/Coq/ZArith/BinInt/Zcompare.con" as definition.
132 Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.
136 Ltac elim_compare com1 com2 :=
137 case (Dcompare (com1 ?= com2)%Z);
138 [ idtac | let x := fresh "H" in
139 (intro x; case x; clear x) ].
142 (*#* Sign function *)
144 inline procedural "cic:/Coq/ZArith/BinInt/Zsgn.con" as definition.
146 (*#* Direct, easier to handle variants of successor and addition *)
148 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc'.con" as definition.
150 inline procedural "cic:/Coq/ZArith/BinInt/Zpred'.con" as definition.
152 inline procedural "cic:/Coq/ZArith/BinInt/Zplus'.con" as definition.
155 Open Local Scope Z_scope.
158 (*#*********************************************************************)
160 (*#* Inductive specification of Z *)
162 inline procedural "cic:/Coq/ZArith/BinInt/Zind.con" as theorem.
164 (*#*********************************************************************)
166 (*#* Properties of opposite on binary integer numbers *)
168 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_neg.con" as theorem.
170 (*#* [opp] is involutive *)
172 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_involutive.con" as theorem.
174 (*#* Injectivity of the opposite *)
176 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_inj.con" as theorem.
178 (*#*********************************************************************)
180 (* Properties of the direct definition of successor and predecessor *)
182 inline procedural "cic:/Coq/ZArith/BinInt/Zpred'_succ'.con" as lemma.
184 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc'_discr.con" as lemma.
186 (*#*********************************************************************)
188 (*#* Other properties of binary integer numbers *)
190 inline procedural "cic:/Coq/ZArith/BinInt/ZL0.con" as lemma.
192 (*#*********************************************************************)
194 (*#* Properties of the addition on integers *)
196 (*#* zero is left neutral for addition *)
198 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_0_l.con" as theorem.
200 (*#* zero is right neutral for addition *)
202 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_0_r.con" as theorem.
204 (*#* addition is commutative *)
206 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_comm.con" as theorem.
208 (*#* opposite distributes over addition *)
210 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_plus_distr.con" as theorem.
212 (*#* opposite is inverse for addition *)
214 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_opp_r.con" as theorem.
216 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_opp_l.con" as theorem.
219 Hint Local Resolve Zplus_0_l Zplus_0_r.
222 (*#* addition is associative *)
224 inline procedural "cic:/Coq/ZArith/BinInt/weak_assoc.con" as lemma.
227 Hint Local Resolve weak_assoc.
230 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_assoc.con" as theorem.
232 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_assoc_reverse.con" as lemma.
234 (*#* Associativity mixed with commutativity *)
236 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_permute.con" as theorem.
238 (*#* addition simplifies *)
240 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_reg_l.con" as theorem.
242 (*#* addition and successor permutes *)
244 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_succ_l.con" as lemma.
246 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_succ_r.con" as lemma.
248 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_succ_comm.con" as lemma.
250 (*#* Misc properties, usually redundant or non natural *)
252 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_0_r_reverse.con" as lemma.
254 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_0_simpl_l.con" as lemma.
256 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_0_simpl_l_reverse.con" as lemma.
258 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_eq_compat.con" as lemma.
260 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_opp_expand.con" as lemma.
262 (*#*********************************************************************)
264 (*#* Properties of successor and predecessor on binary integer numbers *)
266 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc_discr.con" as theorem.
268 inline procedural "cic:/Coq/ZArith/BinInt/Zpos_succ_morphism.con" as theorem.
270 (*#* successor and predecessor are inverse functions *)
272 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc_pred.con" as theorem.
275 Hint Immediate Zsucc_pred: zarith.
278 inline procedural "cic:/Coq/ZArith/BinInt/Zpred_succ.con" as theorem.
280 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc_inj.con" as theorem.
282 (*#* Misc properties, usually redundant or non natural *)
284 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc_eq_compat.con" as lemma.
286 inline procedural "cic:/Coq/ZArith/BinInt/Zsucc_inj_contrapositive.con" as lemma.
288 (*#*********************************************************************)
290 (*#* Properties of subtraction on binary integer numbers *)
292 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_0_r.con" as lemma.
294 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_0_l_reverse.con" as lemma.
296 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_diag.con" as lemma.
298 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_diag_reverse.con" as lemma.
300 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_minus_eq.con" as lemma.
302 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_plus.con" as lemma.
304 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_minus.con" as lemma.
306 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_succ_l.con" as lemma.
308 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_plus_simpl_l.con" as lemma.
310 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_plus_simpl_l_reverse.con" as lemma.
312 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_plus_simpl_r.con" as lemma.
314 (*#* Misc redundant properties *)
316 inline procedural "cic:/Coq/ZArith/BinInt/Zeq_minus.con" as lemma.
318 inline procedural "cic:/Coq/ZArith/BinInt/Zminus_eq.con" as lemma.
320 (*#*********************************************************************)
322 (*#* Properties of multiplication on binary integer numbers *)
324 (*#* One is neutral for multiplication *)
326 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_1_l.con" as theorem.
328 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_1_r.con" as theorem.
330 (*#* Zero property of multiplication *)
332 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_0_l.con" as theorem.
334 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_0_r.con" as theorem.
337 Hint Local Resolve Zmult_0_l Zmult_0_r.
340 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_0_r_reverse.con" as lemma.
342 (*#* Commutativity of multiplication *)
344 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_comm.con" as theorem.
346 (*#* Associativity of multiplication *)
348 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_assoc.con" as theorem.
350 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_assoc_reverse.con" as lemma.
352 (*#* Associativity mixed with commutativity *)
354 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_permute.con" as theorem.
356 (*#* Z is integral *)
358 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_integral_l.con" as theorem.
360 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_integral.con" as theorem.
362 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_1_inversion_l.con" as lemma.
364 (*#* Multiplication and Opposite *)
366 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_mult_distr_l.con" as theorem.
368 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_mult_distr_r.con" as theorem.
370 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_mult_distr_l_reverse.con" as lemma.
372 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_opp_comm.con" as theorem.
374 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_opp_opp.con" as theorem.
376 inline procedural "cic:/Coq/ZArith/BinInt/Zopp_eq_mult_neg_1.con" as theorem.
378 (*#* Distributivity of multiplication over addition *)
380 inline procedural "cic:/Coq/ZArith/BinInt/weak_Zmult_plus_distr_r.con" as lemma.
382 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_plus_distr_r.con" as theorem.
384 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_plus_distr_l.con" as theorem.
386 (*#* Distributivity of multiplication over subtraction *)
388 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_minus_distr_r.con" as lemma.
390 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_minus_distr_l.con" as lemma.
392 (*#* Simplification of multiplication for non-zero integers *)
394 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_reg_l.con" as lemma.
396 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_reg_r.con" as lemma.
398 (*#* Addition and multiplication by 2 *)
400 inline procedural "cic:/Coq/ZArith/BinInt/Zplus_diag_eq_mult_2.con" as lemma.
402 (*#* Multiplication and successor *)
404 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_succ_r.con" as lemma.
406 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_succ_r_reverse.con" as lemma.
408 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_succ_l.con" as lemma.
410 inline procedural "cic:/Coq/ZArith/BinInt/Zmult_succ_l_reverse.con" as lemma.
412 (*#* Misc redundant properties *)
414 inline procedural "cic:/Coq/ZArith/BinInt/Z_eq_mult.con" as lemma.
416 (*#*********************************************************************)
418 (*#* Relating binary positive numbers and binary integers *)
420 inline procedural "cic:/Coq/ZArith/BinInt/Zpos_xI.con" as lemma.
422 inline procedural "cic:/Coq/ZArith/BinInt/Zpos_xO.con" as lemma.
424 inline procedural "cic:/Coq/ZArith/BinInt/Zneg_xI.con" as lemma.
426 inline procedural "cic:/Coq/ZArith/BinInt/Zneg_xO.con" as lemma.
428 inline procedural "cic:/Coq/ZArith/BinInt/Zpos_plus_distr.con" as lemma.
430 inline procedural "cic:/Coq/ZArith/BinInt/Zneg_plus_distr.con" as lemma.
432 (*#*********************************************************************)
434 (*#* Order relations *)
436 inline procedural "cic:/Coq/ZArith/BinInt/Zlt.con" as definition.
438 inline procedural "cic:/Coq/ZArith/BinInt/Zgt.con" as definition.
440 inline procedural "cic:/Coq/ZArith/BinInt/Zle.con" as definition.
442 inline procedural "cic:/Coq/ZArith/BinInt/Zge.con" as definition.
444 inline procedural "cic:/Coq/ZArith/BinInt/Zne.con" as definition.
447 Infix "<=" := Zle : Z_scope.
451 Infix "<" := Zlt : Z_scope.
455 Infix ">=" := Zge : Z_scope.
459 Infix ">" := Zgt : Z_scope.
463 Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
467 Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
471 Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
475 Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
478 (*#*********************************************************************)
480 (*#* Absolute value on integers *)
482 inline procedural "cic:/Coq/ZArith/BinInt/Zabs_nat.con" as definition.
484 inline procedural "cic:/Coq/ZArith/BinInt/Zabs.con" as definition.
486 (*#*********************************************************************)
488 (*#* From [nat] to [Z] *)
490 inline procedural "cic:/Coq/ZArith/BinInt/Z_of_nat.con" as definition.
492 include "NArith/BinNat.ma".
494 inline procedural "cic:/Coq/ZArith/BinInt/Zabs_N.con" as definition.
496 inline procedural "cic:/Coq/ZArith/BinInt/Z_of_N.con" as definition.