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: Pnat.v,v 1.3.2.1 2004/07/16 19:31:07 herbelin Exp $ i*)
35 include "NArith/BinPos.ma".
37 (*#*********************************************************************)
39 (*#* Properties of the injection from binary positive numbers to Peano
42 (*#* Original development by Pierre Cr\233\gut, CNET, Lannion, France *)
44 include "Arith/Le.ma".
46 include "Arith/Lt.ma".
48 include "Arith/Gt.ma".
50 include "Arith/Plus.ma".
52 include "Arith/Mult.ma".
54 include "Arith/Minus.ma".
56 (*#* [nat_of_P] is a morphism for addition *)
58 inline procedural "cic:/Coq/NArith/Pnat/Pmult_nat_succ_morphism.con" as lemma.
60 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_succ_morphism.con" as lemma.
62 inline procedural "cic:/Coq/NArith/Pnat/Pmult_nat_plus_carry_morphism.con" as theorem.
64 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_plus_carry_morphism.con" as theorem.
66 inline procedural "cic:/Coq/NArith/Pnat/Pmult_nat_l_plus_morphism.con" as theorem.
68 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_plus_morphism.con" as theorem.
70 (*#* [Pmult_nat] is a morphism for addition *)
72 inline procedural "cic:/Coq/NArith/Pnat/Pmult_nat_r_plus_morphism.con" as lemma.
74 inline procedural "cic:/Coq/NArith/Pnat/ZL6.con" as lemma.
76 (*#* [nat_of_P] is a morphism for multiplication *)
78 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_mult_morphism.con" as theorem.
80 (*#* [nat_of_P] maps to the strictly positive subset of [nat] *)
82 inline procedural "cic:/Coq/NArith/Pnat/ZL4.con" as lemma.
84 (*#* Extra lemmas on [lt] on Peano natural numbers *)
86 inline procedural "cic:/Coq/NArith/Pnat/ZL7.con" as lemma.
88 inline procedural "cic:/Coq/NArith/Pnat/ZL8.con" as lemma.
90 (*#* [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
91 from [compare] on [positive])
93 Part 1: [lt] on [positive] is finer than [lt] on [nat]
96 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_lt_Lt_compare_morphism.con" as lemma.
98 (*#* [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
99 from [compare] on [positive])
101 Part 1: [gt] on [positive] is finer than [gt] on [nat]
104 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_gt_Gt_compare_morphism.con" as lemma.
106 (*#* [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
107 from [compare] on [positive])
109 Part 2: [lt] on [nat] is finer than [lt] on [positive]
112 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_lt_Lt_compare_complement_morphism.con" as lemma.
114 (*#* [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
115 from [compare] on [positive])
117 Part 2: [gt] on [nat] is finer than [gt] on [positive]
120 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_gt_Gt_compare_complement_morphism.con" as lemma.
122 (*#* [nat_of_P] is strictly positive *)
124 inline procedural "cic:/Coq/NArith/Pnat/le_Pmult_nat.con" as lemma.
126 inline procedural "cic:/Coq/NArith/Pnat/lt_O_nat_of_P.con" as lemma.
128 (*#* Pmult_nat permutes with multiplication *)
130 inline procedural "cic:/Coq/NArith/Pnat/Pmult_nat_mult_permute.con" as lemma.
132 inline procedural "cic:/Coq/NArith/Pnat/Pmult_nat_2_mult_2_permute.con" as lemma.
134 inline procedural "cic:/Coq/NArith/Pnat/Pmult_nat_4_mult_2_permute.con" as lemma.
136 (*#* Mapping of xH, xO and xI through [nat_of_P] *)
138 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_xH.con" as lemma.
140 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_xO.con" as lemma.
142 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_xI.con" as lemma.
144 (*#*********************************************************************)
146 (*#* Properties of the shifted injection from Peano natural numbers to
147 binary positive numbers *)
149 (*#* Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *)
151 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_o_P_of_succ_nat_eq_succ.con" as theorem.
153 (*#* Miscellaneous lemmas on [P_of_succ_nat] *)
155 inline procedural "cic:/Coq/NArith/Pnat/ZL3.con" as lemma.
157 inline procedural "cic:/Coq/NArith/Pnat/ZL5.con" as lemma.
159 (*#* Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *)
161 inline procedural "cic:/Coq/NArith/Pnat/P_of_succ_nat_o_nat_of_P_eq_succ.con" as theorem.
163 (*#* Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity
166 inline procedural "cic:/Coq/NArith/Pnat/pred_o_P_of_succ_nat_o_nat_of_P_eq_id.con" as theorem.
168 (*#*********************************************************************)
170 (*#* Extra properties of the injection from binary positive numbers to Peano
173 (*#* [nat_of_P] is a morphism for subtraction on positive numbers *)
175 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_minus_morphism.con" as theorem.
177 (*#* [nat_of_P] is injective *)
179 inline procedural "cic:/Coq/NArith/Pnat/nat_of_P_inj.con" as lemma.
181 inline procedural "cic:/Coq/NArith/Pnat/ZL16.con" as lemma.
183 inline procedural "cic:/Coq/NArith/Pnat/ZL17.con" as lemma.
185 (*#* Comparison and subtraction *)
187 inline procedural "cic:/Coq/NArith/Pnat/Pcompare_minus_r.con" as lemma.
189 inline procedural "cic:/Coq/NArith/Pnat/Pcompare_minus_l.con" as lemma.
191 (*#* Distributivity of multiplication over subtraction *)
193 inline procedural "cic:/Coq/NArith/Pnat/Pmult_minus_distr_l.con" as theorem.