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