helm/software/matita/contribs/procedural/Coq/ZArith/Zpower.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i $Id: Zpower.v,v 1.11.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
  34
  35 include "ZArith/ZArith_base.ma".
  36
  37 include "ZArith/Zcomplements.ma".
  38
  39 (* UNEXPORTED
  40 Open Local Scope Z_scope.
  41 *)
  42
  43 (* UNEXPORTED
  44 Section section1
  45 *)
  46
  47 (*#* [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
  48     integer (type [nat]) and [z] a signed integer (type [Z]) *)
  49
  50 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_nat.con" as definition.
  51
  52 (*#* [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
  53     [plus : nat->nat] and [Zmult : Z->Z] *)
  54
  55 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_nat_is_exp.con" as lemma.
  56
  57 (*#* [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
  58     integer (type [positive]) and [z] a signed integer (type [Z]) *)
  59
  60 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_pos.con" as definition.
  61
  62 (*#* This theorem shows that powers of unary and binary integers
  63    are the same thing, modulo the function convert : [positive -> nat] *)
  64
  65 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_pos_nat.con" as theorem.
  66
  67 (*#* Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
  68    deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
  69    for [add : positive->positive] and [Zmult : Z->Z] *)
  70
  71 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_pos_is_exp.con" as theorem.
  72
  73 inline procedural "cic:/Coq/ZArith/Zpower/Zpower.con" as definition.
  74
  75 (* NOTATION
  76 Infix "^" := Zpower : Z_scope.
  77 *)
  78
  79 (* UNEXPORTED
  80 Hint Immediate Zpower_nat_is_exp: zarith.
  81 *)
  82
  83 (* UNEXPORTED
  84 Hint Immediate Zpower_pos_is_exp: zarith.
  85 *)
  86
  87 (* UNEXPORTED
  88 Hint Unfold Zpower_pos: zarith.
  89 *)
  90
  91 (* UNEXPORTED
  92 Hint Unfold Zpower_nat: zarith.
  93 *)
  94
  95 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_exp.con" as lemma.
  96
  97 (* UNEXPORTED
  98 End section1
  99 *)
 100
 101 (* Exporting notation "^" *)
 102
 103 (* NOTATION
 104 Infix "^" := Zpower : Z_scope.
 105 *)
 106
 107 (* UNEXPORTED
 108 Hint Immediate Zpower_nat_is_exp: zarith.
 109 *)
 110
 111 (* UNEXPORTED
 112 Hint Immediate Zpower_pos_is_exp: zarith.
 113 *)
 114
 115 (* UNEXPORTED
 116 Hint Unfold Zpower_pos: zarith.
 117 *)
 118
 119 (* UNEXPORTED
 120 Hint Unfold Zpower_nat: zarith.
 121 *)
 122
 123 (* UNEXPORTED
 124 Section Powers_of_2
 125 *)
 126
 127 (*#* For the powers of two, that will be widely used, a more direct
 128    calculus is possible. We will also prove some properties such
 129    as [(x:positive) x < 2^x] that are true for all integers bigger
 130    than 2 but more difficult to prove and useless. *)
 131
 132 (*#* [shift n m] computes [2^n * m], or [m] shifted by [n] positions *)
 133
 134 inline procedural "cic:/Coq/ZArith/Zpower/shift_nat.con" as definition.
 135
 136 inline procedural "cic:/Coq/ZArith/Zpower/shift_pos.con" as definition.
 137
 138 inline procedural "cic:/Coq/ZArith/Zpower/shift.con" as definition.
 139
 140 inline procedural "cic:/Coq/ZArith/Zpower/two_power_nat.con" as definition.
 141
 142 inline procedural "cic:/Coq/ZArith/Zpower/two_power_pos.con" as definition.
 143
 144 inline procedural "cic:/Coq/ZArith/Zpower/two_power_nat_S.con" as lemma.
 145
 146 inline procedural "cic:/Coq/ZArith/Zpower/shift_nat_plus.con" as lemma.
 147
 148 inline procedural "cic:/Coq/ZArith/Zpower/shift_nat_correct.con" as theorem.
 149
 150 inline procedural "cic:/Coq/ZArith/Zpower/two_power_nat_correct.con" as theorem.
 151
 152 (*#* Second we show that [two_power_pos] and [two_power_nat] are the same *)
 153
 154 inline procedural "cic:/Coq/ZArith/Zpower/shift_pos_nat.con" as lemma.
 155
 156 inline procedural "cic:/Coq/ZArith/Zpower/two_power_pos_nat.con" as lemma.
 157
 158 (*#* Then we deduce that [two_power_pos] is also correct *)
 159
 160 inline procedural "cic:/Coq/ZArith/Zpower/shift_pos_correct.con" as theorem.
 161
 162 inline procedural "cic:/Coq/ZArith/Zpower/two_power_pos_correct.con" as theorem.
 163
 164 (*#* Some consequences *)
 165
 166 inline procedural "cic:/Coq/ZArith/Zpower/two_power_pos_is_exp.con" as theorem.
 167
 168 (*#* The exponentiation [z -> 2^z] for [z] a signed integer.
 169     For convenience, we assume that [2^z = 0] for all [z < 0]
 170     We could also define a inductive type [Log_result] with
 171     3 contructors [ Zero | Pos positive -> | minus_infty]
 172     but it's more complexe and not so useful. *)
 173
 174 inline procedural "cic:/Coq/ZArith/Zpower/two_p.con" as definition.
 175
 176 inline procedural "cic:/Coq/ZArith/Zpower/two_p_is_exp.con" as theorem.
 177
 178 inline procedural "cic:/Coq/ZArith/Zpower/two_p_gt_ZERO.con" as lemma.
 179
 180 inline procedural "cic:/Coq/ZArith/Zpower/two_p_S.con" as lemma.
 181
 182 inline procedural "cic:/Coq/ZArith/Zpower/two_p_pred.con" as lemma.
 183
 184 inline procedural "cic:/Coq/ZArith/Zpower/Zlt_lt_double.con" as lemma.
 185
 186 (* UNEXPORTED
 187 End Powers_of_2
 188 *)
 189
 190 (* UNEXPORTED
 191 Hint Resolve two_p_gt_ZERO: zarith.
 192 *)
 193
 194 (* UNEXPORTED
 195 Hint Immediate two_p_pred two_p_S: zarith.
 196 *)
 197
 198 (* UNEXPORTED
 199 Section power_div_with_rest
 200 *)
 201
 202 (*#* Division by a power of two.
 203     To [n:Z] and [p:positive], [q],[r] are associated such that
 204     [n = 2^p.q + r] and [0 <= r < 2^p] *)
 205
 206 (*#* Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *)
 207
 208 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest_aux.con" as definition.
 209
 210 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest.con" as definition.
 211
 212 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest_correct1.con" as lemma.
 213
 214 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest_correct2.con" as lemma.
 215
 216 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest_proofs.ind".
 217
 218 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest_correct.con" as lemma.
 219
 220 (* UNEXPORTED
 221 End power_div_with_rest
 222 *)
 223