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: BinPos.v,v 1.7.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
37 (*#*********************************************************************)
39 (*#* Binary positive numbers *)
41 (*#* Original development by Pierre Cr\233\gut, CNET, Lannion, France *)
43 inline procedural "cic:/Coq/NArith/BinPos/positive.ind".
45 (*#* Declare binding key for scope positive_scope *)
48 Delimit Scope positive_scope with positive.
51 (*#* Automatically open scope positive_scope for type positive, xO and xI *)
54 Bind Scope positive_scope with positive.
58 Arguments Scope xO [positive_scope].
62 Arguments Scope xI [positive_scope].
67 inline procedural "cic:/Coq/NArith/BinPos/Psucc.con" as definition.
71 inline procedural "cic:/Coq/NArith/BinPos/Pplus.con" as definition.
74 Infix "+" := Pplus : positive_scope.
78 Open Local Scope positive_scope.
81 (*#* From binary positive numbers to Peano natural numbers *)
83 inline procedural "cic:/Coq/NArith/BinPos/Pmult_nat.con" as definition.
85 inline procedural "cic:/Coq/NArith/BinPos/nat_of_P.con" as definition.
87 (*#* From Peano natural numbers to binary positive numbers *)
89 inline procedural "cic:/Coq/NArith/BinPos/P_of_succ_nat.con" as definition.
91 (*#* Operation x -> 2*x-1 *)
93 inline procedural "cic:/Coq/NArith/BinPos/Pdouble_minus_one.con" as definition.
97 inline procedural "cic:/Coq/NArith/BinPos/Ppred.con" as definition.
99 (*#* An auxiliary type for subtraction *)
101 inline procedural "cic:/Coq/NArith/BinPos/positive_mask.ind".
103 (*#* Operation x -> 2*x+1 *)
105 inline procedural "cic:/Coq/NArith/BinPos/Pdouble_plus_one_mask.con" as definition.
107 (*#* Operation x -> 2*x *)
109 inline procedural "cic:/Coq/NArith/BinPos/Pdouble_mask.con" as definition.
111 (*#* Operation x -> 2*x-2 *)
113 inline procedural "cic:/Coq/NArith/BinPos/Pdouble_minus_two.con" as definition.
115 (*#* Subtraction of binary positive numbers into a positive numbers mask *)
117 inline procedural "cic:/Coq/NArith/BinPos/Pminus_mask.con" as definition.
119 (*#* Subtraction of binary positive numbers x and y, returns 1 if x<=y *)
121 inline procedural "cic:/Coq/NArith/BinPos/Pminus.con" as definition.
124 Infix "-" := Pminus : positive_scope.
127 (*#* Multiplication on binary positive numbers *)
129 inline procedural "cic:/Coq/NArith/BinPos/Pmult.con" as definition.
132 Infix "*" := Pmult : positive_scope.
135 (*#* Division by 2 rounded below but for 1 *)
137 inline procedural "cic:/Coq/NArith/BinPos/Pdiv2.con" as definition.
140 Infix "/" := Pdiv2 : positive_scope.
143 (*#* Comparison on binary positive numbers *)
145 inline procedural "cic:/Coq/NArith/BinPos/Pcompare.con" as definition.
148 Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
151 (*#*********************************************************************)
153 (*#* Miscellaneous properties of binary positive numbers *)
155 inline procedural "cic:/Coq/NArith/BinPos/ZL11.con" as lemma.
157 (*#*********************************************************************)
159 (*#* Properties of successor on binary positive numbers *)
161 (*#* Specification of [xI] in term of [Psucc] and [xO] *)
163 inline procedural "cic:/Coq/NArith/BinPos/xI_succ_xO.con" as lemma.
165 inline procedural "cic:/Coq/NArith/BinPos/Psucc_discr.con" as lemma.
167 (*#* Successor and double *)
169 inline procedural "cic:/Coq/NArith/BinPos/Psucc_o_double_minus_one_eq_xO.con" as lemma.
171 inline procedural "cic:/Coq/NArith/BinPos/Pdouble_minus_one_o_succ_eq_xI.con" as lemma.
173 inline procedural "cic:/Coq/NArith/BinPos/xO_succ_permute.con" as lemma.
175 inline procedural "cic:/Coq/NArith/BinPos/double_moins_un_xO_discr.con" as lemma.
177 (*#* Successor and predecessor *)
179 inline procedural "cic:/Coq/NArith/BinPos/Psucc_not_one.con" as lemma.
181 inline procedural "cic:/Coq/NArith/BinPos/Ppred_succ.con" as lemma.
183 inline procedural "cic:/Coq/NArith/BinPos/Psucc_pred.con" as lemma.
185 (*#* Injectivity of successor *)
187 inline procedural "cic:/Coq/NArith/BinPos/Psucc_inj.con" as lemma.
189 (*#*********************************************************************)
191 (*#* Properties of addition on binary positive numbers *)
193 (*#* Specification of [Psucc] in term of [Pplus] *)
195 inline procedural "cic:/Coq/NArith/BinPos/Pplus_one_succ_r.con" as lemma.
197 inline procedural "cic:/Coq/NArith/BinPos/Pplus_one_succ_l.con" as lemma.
199 (*#* Specification of [Pplus_carry] *)
201 inline procedural "cic:/Coq/NArith/BinPos/Pplus_carry_spec.con" as theorem.
203 (*#* Commutativity *)
205 inline procedural "cic:/Coq/NArith/BinPos/Pplus_comm.con" as theorem.
207 (*#* Permutation of [Pplus] and [Psucc] *)
209 inline procedural "cic:/Coq/NArith/BinPos/Pplus_succ_permute_r.con" as theorem.
211 inline procedural "cic:/Coq/NArith/BinPos/Pplus_succ_permute_l.con" as theorem.
213 inline procedural "cic:/Coq/NArith/BinPos/Pplus_carry_pred_eq_plus.con" as theorem.
215 (*#* No neutral for addition on strictly positive numbers *)
217 inline procedural "cic:/Coq/NArith/BinPos/Pplus_no_neutral.con" as lemma.
219 inline procedural "cic:/Coq/NArith/BinPos/Pplus_carry_no_neutral.con" as lemma.
221 (*#* Simplification *)
223 inline procedural "cic:/Coq/NArith/BinPos/Pplus_carry_plus.con" as lemma.
225 inline procedural "cic:/Coq/NArith/BinPos/Pplus_reg_r.con" as lemma.
227 inline procedural "cic:/Coq/NArith/BinPos/Pplus_reg_l.con" as lemma.
229 inline procedural "cic:/Coq/NArith/BinPos/Pplus_carry_reg_r.con" as lemma.
231 inline procedural "cic:/Coq/NArith/BinPos/Pplus_carry_reg_l.con" as lemma.
233 (*#* Addition on positive is associative *)
235 inline procedural "cic:/Coq/NArith/BinPos/Pplus_assoc.con" as theorem.
237 (*#* Commutation of addition with the double of a positive number *)
239 inline procedural "cic:/Coq/NArith/BinPos/Pplus_xI_double_minus_one.con" as lemma.
241 inline procedural "cic:/Coq/NArith/BinPos/Pplus_xO_double_minus_one.con" as lemma.
245 inline procedural "cic:/Coq/NArith/BinPos/Pplus_diag.con" as lemma.
247 (*#*********************************************************************)
249 (*#* Peano induction on binary positive positive numbers *)
251 inline procedural "cic:/Coq/NArith/BinPos/plus_iter.con" as definition.
253 inline procedural "cic:/Coq/NArith/BinPos/plus_iter_eq_plus.con" as lemma.
255 inline procedural "cic:/Coq/NArith/BinPos/plus_iter_xO.con" as lemma.
257 inline procedural "cic:/Coq/NArith/BinPos/plus_iter_xI.con" as lemma.
259 inline procedural "cic:/Coq/NArith/BinPos/iterate_add.con" as lemma.
261 (*#* Peano induction *)
263 inline procedural "cic:/Coq/NArith/BinPos/Pind.con" as theorem.
265 (*#* Peano recursion *)
267 inline procedural "cic:/Coq/NArith/BinPos/Prec.con" as definition.
269 (*#* Peano case analysis *)
271 inline procedural "cic:/Coq/NArith/BinPos/Pcase.con" as theorem.
275 (let fact := Prec positive xH (fun p r => Psucc p * r) in
276 let seven := xI (xI xH) in
277 let five_thousand_forty :=
278 xO (xO (xO (xO (xI (xI (xO (xI (xI (xI (xO (xO xH))))))))))) in
279 refl_equal _:fact seven = five_thousand_forty).
282 (*#*********************************************************************)
284 (*#* Properties of multiplication on binary positive numbers *)
286 (*#* One is right neutral for multiplication *)
288 inline procedural "cic:/Coq/NArith/BinPos/Pmult_1_r.con" as lemma.
290 (*#* Right reduction properties for multiplication *)
292 inline procedural "cic:/Coq/NArith/BinPos/Pmult_xO_permute_r.con" as lemma.
294 inline procedural "cic:/Coq/NArith/BinPos/Pmult_xI_permute_r.con" as lemma.
296 (*#* Commutativity of multiplication *)
298 inline procedural "cic:/Coq/NArith/BinPos/Pmult_comm.con" as theorem.
300 (*#* Distributivity of multiplication over addition *)
302 inline procedural "cic:/Coq/NArith/BinPos/Pmult_plus_distr_l.con" as theorem.
304 inline procedural "cic:/Coq/NArith/BinPos/Pmult_plus_distr_r.con" as theorem.
306 (*#* Associativity of multiplication *)
308 inline procedural "cic:/Coq/NArith/BinPos/Pmult_assoc.con" as theorem.
310 (*#* Parity properties of multiplication *)
312 inline procedural "cic:/Coq/NArith/BinPos/Pmult_xI_mult_xO_discr.con" as lemma.
314 inline procedural "cic:/Coq/NArith/BinPos/Pmult_xO_discr.con" as lemma.
316 (*#* Simplification properties of multiplication *)
318 inline procedural "cic:/Coq/NArith/BinPos/Pmult_reg_r.con" as theorem.
320 inline procedural "cic:/Coq/NArith/BinPos/Pmult_reg_l.con" as theorem.
322 (*#* Inversion of multiplication *)
324 inline procedural "cic:/Coq/NArith/BinPos/Pmult_1_inversion_l.con" as lemma.
326 (*#*********************************************************************)
328 (*#* Properties of comparison on binary positive numbers *)
330 inline procedural "cic:/Coq/NArith/BinPos/Pcompare_not_Eq.con" as theorem.
332 inline procedural "cic:/Coq/NArith/BinPos/Pcompare_Eq_eq.con" as theorem.
334 inline procedural "cic:/Coq/NArith/BinPos/Pcompare_Gt_Lt.con" as lemma.
336 inline procedural "cic:/Coq/NArith/BinPos/Pcompare_Lt_Gt.con" as lemma.
338 inline procedural "cic:/Coq/NArith/BinPos/Pcompare_Lt_Lt.con" as lemma.
340 inline procedural "cic:/Coq/NArith/BinPos/Pcompare_Gt_Gt.con" as lemma.
342 inline procedural "cic:/Coq/NArith/BinPos/Dcompare.con" as lemma.
345 Ltac ElimPcompare c1 c2 :=
346 elim (Dcompare ((c1 ?= c2) Eq));
347 [ idtac | let x := fresh "H" in
348 (intro x; case x; clear x) ].
351 inline procedural "cic:/Coq/NArith/BinPos/Pcompare_refl.con" as theorem.
353 inline procedural "cic:/Coq/NArith/BinPos/Pcompare_antisym.con" as lemma.
355 inline procedural "cic:/Coq/NArith/BinPos/ZC1.con" as lemma.
357 inline procedural "cic:/Coq/NArith/BinPos/ZC2.con" as lemma.
359 inline procedural "cic:/Coq/NArith/BinPos/ZC3.con" as lemma.
361 inline procedural "cic:/Coq/NArith/BinPos/ZC4.con" as lemma.
363 (*#*********************************************************************)
365 (*#* Properties of subtraction on binary positive numbers *)
367 inline procedural "cic:/Coq/NArith/BinPos/double_eq_zero_inversion.con" as lemma.
369 inline procedural "cic:/Coq/NArith/BinPos/double_plus_one_zero_discr.con" as lemma.
371 inline procedural "cic:/Coq/NArith/BinPos/double_plus_one_eq_one_inversion.con" as lemma.
373 inline procedural "cic:/Coq/NArith/BinPos/double_eq_one_discr.con" as lemma.
375 inline procedural "cic:/Coq/NArith/BinPos/Pminus_mask_diag.con" as theorem.
377 inline procedural "cic:/Coq/NArith/BinPos/ZL10.con" as lemma.
379 (*#* Properties of subtraction valid only for x>y *)
381 inline procedural "cic:/Coq/NArith/BinPos/Pminus_mask_Gt.con" as lemma.
383 inline procedural "cic:/Coq/NArith/BinPos/Pplus_minus.con" as theorem.