blob: 7e3fe306f6692fbcb644e8059c5bb19edd72371f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: fast_integer.v,v 1.1.2.1 2004/07/16 19:31:44 herbelin Exp $ i*)
(***********************************************************)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
(***********************************************************)
Require BinPos.
Require BinNat.
Require BinInt.
Require Zcompare.
Require Mult.
V7only [
(* Defs and ppties on positive, entier and Z, previously in fast_integer *)
(* For v7 compatibility *)
Notation positive := positive.
Notation xO := xO.
Notation xI := xI.
Notation xH := xH.
Notation add_un := add_un.
Notation add := add.
Notation convert := convert.
Notation convert_add_un := convert_add_un.
Notation cvt_carry := cvt_carry.
Notation convert_add := convert_add.
Notation positive_to_nat := positive_to_nat.
Notation anti_convert := anti_convert.
Notation double_moins_un := double_moins_un.
Notation sub_un := sub_un.
Notation positive_mask := positive_mask.
Notation Un_suivi_de_mask := Un_suivi_de_mask.
Notation Zero_suivi_de_mask := Zero_suivi_de_mask.
Notation double_moins_deux := double_moins_deux.
Notation sub_pos := sub_pos.
Notation true_sub := true_sub.
Notation times := times.
Notation relation := relation.
Notation SUPERIEUR := SUPERIEUR.
Notation INFERIEUR := INFERIEUR.
Notation EGAL := EGAL.
Notation Op := Op.
Notation compare := compare.
Notation compare_convert1 := compare_convert1.
Notation compare_convert_EGAL := compare_convert_EGAL.
Notation ZLSI := ZLSI.
Notation ZLIS := ZLIS.
Notation ZLII := ZLII.
Notation ZLSS := ZLSS.
Notation Dcompare := Dcompare.
Notation convert_compare_EGAL := convert_compare_EGAL.
Notation ZL0 := ZL0.
Notation ZL11 := ZL11.
Notation xI_add_un_xO := xI_add_un_xO.
Notation is_double_moins_un := is_double_moins_un.
Notation double_moins_un_add_un_xI := double_moins_un_add_un_xI.
Notation ZL1 := ZL1.
Notation add_un_not_un := add_un_not_un.
Notation sub_add_one := sub_add_one.
Notation add_sub_one := add_sub_one.
Notation add_un_inj := add_un_inj.
Notation ZL12 := ZL12.
Notation ZL12bis := ZL12bis.
Notation ZL13 := ZL13.
Notation add_sym := add_sym.
Notation ZL14 := ZL14.
Notation ZL14bis := ZL14bis.
Notation ZL15 := ZL15.
Notation add_no_neutral := add_no_neutral.
Notation add_carry_not_add_un := add_carry_not_add_un.
Notation add_carry_add := add_carry_add.
Notation simpl_add_r := simpl_add_r.
Notation simpl_add_carry_r := simpl_add_carry_r.
Notation simpl_add_l := simpl_add_l.
Notation simpl_add_carry_l := simpl_add_carry_l.
Notation add_assoc := add_assoc.
Notation add_xI_double_moins_un := add_xI_double_moins_un.
Notation add_x_x := add_x_x.
Notation ZS := ZS.
Notation US := US.
Notation USH := USH.
Notation ZSH := ZSH.
Notation sub_pos_x_x := sub_pos_x_x.
Notation ZL10 := ZL10.
Notation sub_pos_SUPERIEUR := sub_pos_SUPERIEUR.
Notation sub_add := sub_add.
Notation convert_add_carry := convert_add_carry.
Notation add_verif := add_verif.
Notation ZL2 := ZL2.
Notation ZL6 := ZL6.
Notation positive_to_nat_mult := positive_to_nat_mult.
Notation times_convert := times_convert.
Notation compare_positive_to_nat_O := compare_positive_to_nat_O.
Notation compare_convert_O := compare_convert_O.
Notation convert_xH := convert_xH.
Notation convert_xO := convert_xO.
Notation convert_xI := convert_xI.
Notation bij1 := bij1.
Notation ZL3 := ZL3.
Notation ZL4 := ZL4.
Notation ZL5 := ZL5.
Notation bij2 := bij2.
Notation bij3 := bij3.
Notation ZL7 := ZL7.
Notation ZL8 := ZL8.
Notation compare_convert_INFERIEUR := compare_convert_INFERIEUR.
Notation compare_convert_SUPERIEUR := compare_convert_SUPERIEUR.
Notation convert_compare_INFERIEUR := convert_compare_INFERIEUR.
Notation convert_compare_SUPERIEUR := convert_compare_SUPERIEUR.
Notation ZC1 := ZC1.
Notation ZC2 := ZC2.
Notation ZC3 := ZC3.
Notation ZC4 := ZC4.
Notation true_sub_convert := true_sub_convert.
Notation convert_intro := convert_intro.
Notation ZL16 := ZL16.
Notation ZL17 := ZL17.
Notation compare_true_sub_right := compare_true_sub_right.
Notation compare_true_sub_left := compare_true_sub_left.
Notation times_x_ := times_x_1.
Notation times_x_double := times_x_double.
Notation times_x_double_plus_one := times_x_double_plus_one.
Notation times_sym := times_sym.
Notation times_add_distr := times_add_distr.
Notation times_add_distr_l := times_add_distr_l.
Notation times_assoc := times_assoc.
Notation times_true_sub_distr := times_true_sub_distr.
Notation times_discr_xO_xI := times_discr_xO_xI.
Notation times_discr_xO := times_discr_xO.
Notation simpl_times_r := simpl_times_r.
Notation simpl_times_l := simpl_times_l.
Notation iterate_add := iterate_add.
Notation entier := entier.
Notation Nul := Nul.
Notation Pos := Pos.
Notation Un_suivi_de := Un_suivi_de.
Notation Zero_suivi_de := Zero_suivi_de.
Notation times1 :=
[x:positive;_:positive->positive;y:positive](times x y).
Notation times1_convert :=
[x,y:positive;_:positive->positive](times_convert x y).
Notation Z := Z.
Notation POS := POS.
Notation NEG := NEG.
Notation ZERO := ZERO.
Notation Zero_left := Zero_left.
Notation Zopp_Zopp := Zopp_Zopp.
Notation Zero_right := Zero_right.
Notation Zplus_inverse_r := Zplus_inverse_r.
Notation Zopp_Zplus := Zopp_Zplus.
Notation Zplus_sym := Zplus_sym.
Notation Zplus_inverse_l := Zplus_inverse_l.
Notation Zopp_intro := Zopp_intro.
Notation Zopp_NEG := Zopp_NEG.
Notation weak_assoc := weak_assoc.
Notation Zplus_assoc := Zplus_assoc.
Notation Zplus_simpl := Zplus_simpl.
Notation Zmult_sym := Zmult_sym.
Notation Zmult_assoc := Zmult_assoc.
Notation Zmult_one := Zmult_one.
Notation lt_mult_left := lt_mult_left. (* Mult*)
Notation Zero_mult_left := Zero_mult_left.
Notation Zero_mult_right := Zero_mult_right.
Notation Zopp_Zmult := Zopp_Zmult.
Notation Zmult_Zopp_Zopp := Zmult_Zopp_Zopp.
Notation weak_Zmult_plus_distr_r := weak_Zmult_plus_distr_r.
Notation Zmult_plus_distr_r := Zmult_plus_distr_r.
Notation Zcompare_EGAL := Zcompare_EGAL.
Notation Zcompare_ANTISYM := Zcompare_ANTISYM.
Notation le_minus := le_minus.
Notation Zcompare_Zopp := Zcompare_Zopp.
Notation weaken_Zcompare_Zplus_compatible := weaken_Zcompare_Zplus_compatible.
Notation weak_Zcompare_Zplus_compatible := weak_Zcompare_Zplus_compatible.
Notation Zcompare_Zplus_compatible := Zcompare_Zplus_compatible.
Notation Zcompare_trans_SUPERIEUR := Zcompare_trans_SUPERIEUR.
Notation SUPERIEUR_POS := SUPERIEUR_POS.
Export Datatypes.
Export BinPos.
Export BinNat.
Export BinInt.
Export Zcompare.
Export Mult.
].
|
