Pow2int.v 6.37 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

Clement Fumex's avatar
Clement Fumex committed
12 13 14 15 16
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Clément Fumex's avatar
Clément Fumex committed
17 18

(* Why3 goal *)
19
Definition pow2 : Z -> Z.
Clément Fumex's avatar
Clément Fumex committed
20 21 22 23
  exact (two_p).
Defined.

(* Why3 goal *)
24
Lemma Power_0 : ((pow2 0%Z) = 1%Z).
Clément Fumex's avatar
Clément Fumex committed
25 26 27 28
  easy.
Qed.

(* Why3 goal *)
29 30
Lemma Power_s :
  forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z).
Clément Fumex's avatar
Clément Fumex committed
31 32 33 34
  apply two_p_S.
Qed.

(* Why3 goal *)
35
Lemma Power_1 : ((pow2 1%Z) = 2%Z).
Clément Fumex's avatar
Clément Fumex committed
36 37 38 39
  easy.
Qed.

(* Why3 goal *)
40
Lemma Power_sum :
41
  forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
42
  ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
Clément Fumex's avatar
Clément Fumex committed
43 44 45 46 47 48
  unfold pow2.
  intros n m [H1 H2].
  apply two_p_is_exp; easy.
Qed.

(* Why3 goal *)
49
Lemma pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z.
Clément Fumex's avatar
Clément Fumex committed
50 51 52 53 54 55 56
  intros i h1.
  Require Import Zorder.
  apply Zgt_lt.
  auto using two_p_gt_ZERO.
Qed.

(* Why3 goal *)
57
Lemma pow2_0 : ((pow2 0%Z) = 1%Z).
Clément Fumex's avatar
Clément Fumex committed
58 59 60 61
  easy.
Qed.

(* Why3 goal *)
62
Lemma pow2_1 : ((pow2 1%Z) = 2%Z).
Clément Fumex's avatar
Clément Fumex committed
63 64 65 66
  easy.
Qed.

(* Why3 goal *)
67
Lemma pow2_2 : ((pow2 2%Z) = 4%Z).
Clément Fumex's avatar
Clément Fumex committed
68 69 70 71
  easy.
Qed.

(* Why3 goal *)
72
Lemma pow2_3 : ((pow2 3%Z) = 8%Z).
Clément Fumex's avatar
Clément Fumex committed
73 74 75 76
  easy.
Qed.

(* Why3 goal *)
77
Lemma pow2_4 : ((pow2 4%Z) = 16%Z).
Clément Fumex's avatar
Clément Fumex committed
78 79 80 81
  easy.
Qed.

(* Why3 goal *)
82
Lemma pow2_5 : ((pow2 5%Z) = 32%Z).
Clément Fumex's avatar
Clément Fumex committed
83 84 85 86
  easy.
Qed.

(* Why3 goal *)
87
Lemma pow2_6 : ((pow2 6%Z) = 64%Z).
Clément Fumex's avatar
Clément Fumex committed
88 89 90 91
  easy.
Qed.

(* Why3 goal *)
92
Lemma pow2_7 : ((pow2 7%Z) = 128%Z).
Clément Fumex's avatar
Clément Fumex committed
93 94 95 96
  easy.
Qed.

(* Why3 goal *)
97
Lemma pow2_8 : ((pow2 8%Z) = 256%Z).
Clément Fumex's avatar
Clément Fumex committed
98 99 100 101
  easy.
Qed.

(* Why3 goal *)
102
Lemma pow2_9 : ((pow2 9%Z) = 512%Z).
Clément Fumex's avatar
Clément Fumex committed
103 104 105 106
  easy.
Qed.

(* Why3 goal *)
107
Lemma pow2_10 : ((pow2 10%Z) = 1024%Z).
Clément Fumex's avatar
Clément Fumex committed
108 109 110 111
  easy.
Qed.

(* Why3 goal *)
112
Lemma pow2_11 : ((pow2 11%Z) = 2048%Z).
Clément Fumex's avatar
Clément Fumex committed
113 114 115 116
  easy.
Qed.

(* Why3 goal *)
117
Lemma pow2_12 : ((pow2 12%Z) = 4096%Z).
Clément Fumex's avatar
Clément Fumex committed
118 119 120 121
  easy.
Qed.

(* Why3 goal *)
122
Lemma pow2_13 : ((pow2 13%Z) = 8192%Z).
Clément Fumex's avatar
Clément Fumex committed
123 124 125 126
  easy.
Qed.

(* Why3 goal *)
127
Lemma pow2_14 : ((pow2 14%Z) = 16384%Z).
Clément Fumex's avatar
Clément Fumex committed
128 129 130 131
  easy.
Qed.

(* Why3 goal *)
132
Lemma pow2_15 : ((pow2 15%Z) = 32768%Z).
Clément Fumex's avatar
Clément Fumex committed
133 134 135 136
  easy.
Qed.

(* Why3 goal *)
137
Lemma pow2_16 : ((pow2 16%Z) = 65536%Z).
Clément Fumex's avatar
Clément Fumex committed
138 139 140 141
  easy.
Qed.

(* Why3 goal *)
142
Lemma pow2_17 : ((pow2 17%Z) = 131072%Z).
Clément Fumex's avatar
Clément Fumex committed
143 144 145 146
  easy.
Qed.

(* Why3 goal *)
147
Lemma pow2_18 : ((pow2 18%Z) = 262144%Z).
Clément Fumex's avatar
Clément Fumex committed
148 149 150 151
  easy.
Qed.

(* Why3 goal *)
152
Lemma pow2_19 : ((pow2 19%Z) = 524288%Z).
Clément Fumex's avatar
Clément Fumex committed
153 154 155 156
  easy.
Qed.

(* Why3 goal *)
157
Lemma pow2_20 : ((pow2 20%Z) = 1048576%Z).
Clément Fumex's avatar
Clément Fumex committed
158 159 160 161
  easy.
Qed.

(* Why3 goal *)
162
Lemma pow2_21 : ((pow2 21%Z) = 2097152%Z).
Clément Fumex's avatar
Clément Fumex committed
163 164 165 166
  easy.
Qed.

(* Why3 goal *)
167
Lemma pow2_22 : ((pow2 22%Z) = 4194304%Z).
Clément Fumex's avatar
Clément Fumex committed
168 169 170 171
  easy.
Qed.

(* Why3 goal *)
172
Lemma pow2_23 : ((pow2 23%Z) = 8388608%Z).
Clément Fumex's avatar
Clément Fumex committed
173 174 175 176
  easy.
Qed.

(* Why3 goal *)
177
Lemma pow2_24 : ((pow2 24%Z) = 16777216%Z).
Clément Fumex's avatar
Clément Fumex committed
178 179 180 181
  easy.
Qed.

(* Why3 goal *)
182
Lemma pow2_25 : ((pow2 25%Z) = 33554432%Z).
Clément Fumex's avatar
Clément Fumex committed
183 184 185 186
  easy.
Qed.

(* Why3 goal *)
187
Lemma pow2_26 : ((pow2 26%Z) = 67108864%Z).
Clément Fumex's avatar
Clément Fumex committed
188 189 190 191
  easy.
Qed.

(* Why3 goal *)
192
Lemma pow2_27 : ((pow2 27%Z) = 134217728%Z).
Clément Fumex's avatar
Clément Fumex committed
193 194 195 196
  easy.
Qed.

(* Why3 goal *)
197
Lemma pow2_28 : ((pow2 28%Z) = 268435456%Z).
Clément Fumex's avatar
Clément Fumex committed
198 199 200 201
  easy.
Qed.

(* Why3 goal *)
202
Lemma pow2_29 : ((pow2 29%Z) = 536870912%Z).
Clément Fumex's avatar
Clément Fumex committed
203 204 205 206
  easy.
Qed.

(* Why3 goal *)
207
Lemma pow2_30 : ((pow2 30%Z) = 1073741824%Z).
Clément Fumex's avatar
Clément Fumex committed
208 209 210 211
  easy.
Qed.

(* Why3 goal *)
212
Lemma pow2_31 : ((pow2 31%Z) = 2147483648%Z).
Clément Fumex's avatar
Clément Fumex committed
213 214 215 216
  easy.
Qed.

(* Why3 goal *)
217
Lemma pow2_32 : ((pow2 32%Z) = 4294967296%Z).
Clément Fumex's avatar
Clément Fumex committed
218 219 220 221
  easy.
Qed.

(* Why3 goal *)
222
Lemma pow2_33 : ((pow2 33%Z) = 8589934592%Z).
Clément Fumex's avatar
Clément Fumex committed
223 224 225 226
  easy.
Qed.

(* Why3 goal *)
227
Lemma pow2_34 : ((pow2 34%Z) = 17179869184%Z).
Clément Fumex's avatar
Clément Fumex committed
228 229 230 231
  easy.
Qed.

(* Why3 goal *)
232
Lemma pow2_35 : ((pow2 35%Z) = 34359738368%Z).
Clément Fumex's avatar
Clément Fumex committed
233 234 235 236
  easy.
Qed.

(* Why3 goal *)
237
Lemma pow2_36 : ((pow2 36%Z) = 68719476736%Z).
Clément Fumex's avatar
Clément Fumex committed
238 239 240 241
  easy.
Qed.

(* Why3 goal *)
242
Lemma pow2_37 : ((pow2 37%Z) = 137438953472%Z).
Clément Fumex's avatar
Clément Fumex committed
243 244 245 246
  easy.
Qed.

(* Why3 goal *)
247
Lemma pow2_38 : ((pow2 38%Z) = 274877906944%Z).
Clément Fumex's avatar
Clément Fumex committed
248 249 250 251
  easy.
Qed.

(* Why3 goal *)
252
Lemma pow2_39 : ((pow2 39%Z) = 549755813888%Z).
Clément Fumex's avatar
Clément Fumex committed
253 254 255 256
  easy.
Qed.

(* Why3 goal *)
257
Lemma pow2_40 : ((pow2 40%Z) = 1099511627776%Z).
Clément Fumex's avatar
Clément Fumex committed
258 259 260 261
  easy.
Qed.

(* Why3 goal *)
262
Lemma pow2_41 : ((pow2 41%Z) = 2199023255552%Z).
Clément Fumex's avatar
Clément Fumex committed
263 264 265 266
  easy.
Qed.

(* Why3 goal *)
267
Lemma pow2_42 : ((pow2 42%Z) = 4398046511104%Z).
Clément Fumex's avatar
Clément Fumex committed
268 269 270 271
  easy.
Qed.

(* Why3 goal *)
272
Lemma pow2_43 : ((pow2 43%Z) = 8796093022208%Z).
Clément Fumex's avatar
Clément Fumex committed
273 274 275 276
  easy.
Qed.

(* Why3 goal *)
277
Lemma pow2_44 : ((pow2 44%Z) = 17592186044416%Z).
Clément Fumex's avatar
Clément Fumex committed
278 279 280 281
  easy.
Qed.

(* Why3 goal *)
282
Lemma pow2_45 : ((pow2 45%Z) = 35184372088832%Z).
Clément Fumex's avatar
Clément Fumex committed
283 284 285 286
  easy.
Qed.

(* Why3 goal *)
287
Lemma pow2_46 : ((pow2 46%Z) = 70368744177664%Z).
Clément Fumex's avatar
Clément Fumex committed
288 289 290 291
  easy.
Qed.

(* Why3 goal *)
292
Lemma pow2_47 : ((pow2 47%Z) = 140737488355328%Z).
Clément Fumex's avatar
Clément Fumex committed
293 294 295 296
  easy.
Qed.

(* Why3 goal *)
297
Lemma pow2_48 : ((pow2 48%Z) = 281474976710656%Z).
Clément Fumex's avatar
Clément Fumex committed
298 299 300 301
  easy.
Qed.

(* Why3 goal *)
302
Lemma pow2_49 : ((pow2 49%Z) = 562949953421312%Z).
Clément Fumex's avatar
Clément Fumex committed
303 304 305 306
  easy.
Qed.

(* Why3 goal *)
307
Lemma pow2_50 : ((pow2 50%Z) = 1125899906842624%Z).
Clément Fumex's avatar
Clément Fumex committed
308 309 310 311
  easy.
Qed.

(* Why3 goal *)
312
Lemma pow2_51 : ((pow2 51%Z) = 2251799813685248%Z).
Clément Fumex's avatar
Clément Fumex committed
313 314 315 316
  easy.
Qed.

(* Why3 goal *)
317
Lemma pow2_52 : ((pow2 52%Z) = 4503599627370496%Z).
Clément Fumex's avatar
Clément Fumex committed
318 319 320 321
  easy.
Qed.

(* Why3 goal *)
322
Lemma pow2_53 : ((pow2 53%Z) = 9007199254740992%Z).
Clément Fumex's avatar
Clément Fumex committed
323 324 325 326
  easy.
Qed.

(* Why3 goal *)
327
Lemma pow2_54 : ((pow2 54%Z) = 18014398509481984%Z).
Clément Fumex's avatar
Clément Fumex committed
328 329 330 331
  easy.
Qed.

(* Why3 goal *)
332
Lemma pow2_55 : ((pow2 55%Z) = 36028797018963968%Z).
Clément Fumex's avatar
Clément Fumex committed
333 334 335 336
  easy.
Qed.

(* Why3 goal *)
337
Lemma pow2_56 : ((pow2 56%Z) = 72057594037927936%Z).
Clément Fumex's avatar
Clément Fumex committed
338 339 340 341
  easy.
Qed.

(* Why3 goal *)
342
Lemma pow2_57 : ((pow2 57%Z) = 144115188075855872%Z).
Clément Fumex's avatar
Clément Fumex committed
343 344 345 346 347
  easy.

Qed.

(* Why3 goal *)
348
Lemma pow2_58 : ((pow2 58%Z) = 288230376151711744%Z).
Clément Fumex's avatar
Clément Fumex committed
349 350 351 352
  easy.
Qed.

(* Why3 goal *)
353
Lemma pow2_59 : ((pow2 59%Z) = 576460752303423488%Z).
Clément Fumex's avatar
Clément Fumex committed
354 355 356 357
  easy.
Qed.

(* Why3 goal *)
358
Lemma pow2_60 : ((pow2 60%Z) = 1152921504606846976%Z).
Clément Fumex's avatar
Clément Fumex committed
359 360 361 362
  easy.
Qed.

(* Why3 goal *)
363
Lemma pow2_61 : ((pow2 61%Z) = 2305843009213693952%Z).
Clément Fumex's avatar
Clément Fumex committed
364 365 366 367
  easy.
Qed.

(* Why3 goal *)
368
Lemma pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
Clément Fumex's avatar
Clément Fumex committed
369 370 371 372
  easy.
Qed.

(* Why3 goal *)
373
Lemma pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
Clément Fumex's avatar
Clément Fumex committed
374 375 376 377
  easy.
Qed.

(* Why3 goal *)
378
Lemma pow2_64 : ((pow2 64%Z) = 18446744073709551616%Z).
Clément Fumex's avatar
Clément Fumex committed
379 380
  easy.
Qed.
Clement Fumex's avatar
Clement Fumex committed
381