helm/software/matita/contribs/procedural/Coq/ZArith/Zlogarithm.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: Zlogarithm.v,v 1.14.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
  34
  35 (*#*********************************************************************)
  36
  37 (*#* The integer logarithms with base 2.
  38
  39     There are three logarithms,
  40     depending on the rounding of the real 2-based logarithm:
  41     - [Log_inf]: [y = (Log_inf x) iff 2^y <= x < 2^(y+1)]
  42       i.e. [Log_inf x] is the biggest integer that is smaller than [Log x]
  43     - [Log_sup]: [y = (Log_sup x) iff 2^(y-1) < x <= 2^y]
  44       i.e. [Log_inf x] is the smallest integer that is bigger than [Log x]
  45     - [Log_nearest]: [y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)]
  46       i.e. [Log_nearest x] is the integer nearest from [Log x] *)
  47
  48 include "ZArith/ZArith_base.ma".
  49
  50 include "ZArith/Zcomplements.ma".
  51
  52 include "ZArith/Zpower.ma".
  53
  54 (* UNEXPORTED
  55 Open Local Scope Z_scope.
  56 *)
  57
  58 (* UNEXPORTED
  59 Section Log_pos
  60 *)
  61
  62 (* Log of positive integers *)
  63
  64 (*#* First we build [log_inf] and [log_sup] *)
  65
  66 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf.con" as definition.
  67
  68 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup.con" as definition.
  69
  70 (* UNEXPORTED
  71 Hint Unfold log_inf log_sup.
  72 *)
  73
  74 (*#* Then we give the specifications of [log_inf] and [log_sup]
  75     and prove their validity *)
  76
  77 (*i Hints Resolve ZERO_le_S : zarith. i*)
  78
  79 (* UNEXPORTED
  80 Hint Resolve Zle_trans: zarith.
  81 *)
  82
  83 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf_correct.con" as theorem.
  84
  85 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf_correct1.con" as definition.
  86
  87 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf_correct2.con" as definition.
  88
  89 (* UNEXPORTED
  90 Opaque log_inf_correct1 log_inf_correct2.
  91 *)
  92
  93 (* UNEXPORTED
  94 Hint Resolve log_inf_correct1 log_inf_correct2: zarith.
  95 *)
  96
  97 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup_correct1.con" as lemma.
  98
  99 (*#* For every [p], either [p] is a power of two and [(log_inf p)=(log_sup p)]
 100     either [(log_sup p)=(log_inf p)+1] *)
 101
 102 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup_log_inf.con" as theorem.
 103
 104 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup_correct2.con" as theorem.
 105
 106 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf_le_log_sup.con" as lemma.
 107
 108 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup_le_Slog_inf.con" as lemma.
 109
 110 (*#* Now it's possible to specify and build the [Log] rounded to the nearest *)
 111
 112 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_near.con" as definition.
 113
 114 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_near_correct1.con" as theorem.
 115
 116 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_near_correct2.con" as theorem.
 117
 118 (*i******************
 119 Theorem log_near_correct: (p:positive)
 120   `| (two_p (log_near p)) - (POS p) | <= (POS p)-(two_p (log_inf p))`
 121   /\`| (two_p (log_near p)) - (POS p) | <= (two_p (log_sup p))-(POS p)`.
 122 Intro.
 123 Induction p.
 124 Intros p0 [(Einf1,Einf2)|(Esup1,Esup2)].
 125 Unfold log_near log_inf log_sup. Fold log_near log_inf log_sup.
 126 Rewrite Einf1.
 127 Repeat Rewrite two_p_S.
 128 Case p0; [Left | Left | Right].
 129
 130 Split.
 131 Simpl.
 132 Rewrite E1; Case p0; Try Reflexivity.
 133 Compute.
 134 Unfold log_near; Fold log_near.
 135 Unfold log_inf; Fold log_inf.
 136 Repeat Rewrite E1.
 137 Split.
 138 **********************************i*)
 139
 140 (* UNEXPORTED
 141 End Log_pos
 142 *)
 143
 144 (* UNEXPORTED
 145 Section divers
 146 *)
 147
 148 (*#* Number of significative digits. *)
 149
 150 inline procedural "cic:/Coq/ZArith/Zlogarithm/N_digits.con" as definition.
 151
 152 inline procedural "cic:/Coq/ZArith/Zlogarithm/ZERO_le_N_digits.con" as lemma.
 153
 154 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf_shift_nat.con" as lemma.
 155
 156 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup_shift_nat.con" as lemma.
 157
 158 (*#* [Is_power p] means that p is a power of two *)
 159
 160 inline procedural "cic:/Coq/ZArith/Zlogarithm/Is_power.con" as definition.
 161
 162 inline procedural "cic:/Coq/ZArith/Zlogarithm/Is_power_correct.con" as lemma.
 163
 164 inline procedural "cic:/Coq/ZArith/Zlogarithm/Is_power_or.con" as lemma.
 165
 166 (* UNEXPORTED
 167 End divers
 168 *)
 169