helm/software/matita/contribs/procedural/Coq/ZArith/Zdiv.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: Zdiv.v,v 1.21.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
  34
  35 (* Contribution by Claude March\233\ and Xavier Urbain *)
  36
  37 (*#*
  38
  39 Euclidean Division
  40
  41 Defines first of function that allows Coq to normalize.
  42 Then only after proves the main required property.
  43
  44 *)
  45
  46 include "ZArith/ZArith_base.ma".
  47
  48 include "ZArith/Zbool.ma".
  49
  50 include "ZArith/Zcomplements.ma".
  51
  52 (* UNEXPORTED
  53 Open Local Scope Z_scope.
  54 *)
  55
  56 (*#*
  57
  58   Euclidean division of a positive by a integer
  59   (that is supposed to be positive).
  60
  61   total function than returns an arbitrary value when
  62   divisor is not positive
  63
  64 *)
  65
  66 inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl_POS.con" as definition.
  67
  68 (*#*
  69
  70   Euclidean division of integers.
  71
  72   Total function than returns (0,0) when dividing by 0.
  73
  74 *)
  75
  76 (*
  77
  78   The pseudo-code is:
  79
  80   if b = 0 : (0,0)
  81
  82   if b <> 0 and a = 0 : (0,0)
  83
  84   if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in
  85                        if r = 0 then (-q,0) else (-(q+1),b-r)
  86
  87   if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r)
  88
  89   if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in
  90                        if r = 0 then (-q,0) else (-(q+1),b+r)
  91
  92   In other word, when b is non-zero, q is chosen to be the greatest integer
  93   smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b|.
  94
  95 *)
  96
  97 inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl.con" as definition.
  98
  99 (*#* Division and modulo are projections of [Zdiv_eucl] *)
 100
 101 inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv.con" as definition.
 102
 103 inline procedural "cic:/Coq/ZArith/Zdiv/Zmod.con" as definition.
 104
 105 (* Tests:
 106
 107 Eval Compute in `(Zdiv_eucl 7 3)`.
 108
 109 Eval Compute in `(Zdiv_eucl (-7) 3)`.
 110
 111 Eval Compute in `(Zdiv_eucl 7 (-3))`.
 112
 113 Eval Compute in `(Zdiv_eucl (-7) (-3))`.
 114
 115 *)
 116
 117 (*#*
 118
 119   Main division theorem.
 120
 121   First a lemma for positive
 122
 123 *)
 124
 125 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mod_POS.con" as lemma.
 126
 127 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mod.con" as theorem.
 128
 129 (*#* Existence theorems *)
 130
 131 inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl_exist.con" as theorem.
 132
 133 (* UNEXPORTED
 134 Implicit Arguments Zdiv_eucl_exist.
 135 *)
 136
 137 inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl_extended.con" as theorem.
 138
 139 (* UNEXPORTED
 140 Implicit Arguments Zdiv_eucl_extended.
 141 *)
 142
 143 (*#* Auxiliary lemmas about [Zdiv] and [Zmod] *)
 144
 145 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mod_eq.con" as lemma.
 146
 147 inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_lt.con" as lemma.
 148
 149 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_POS_ge0.con" as lemma.
 150
 151 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_ge0.con" as lemma.
 152
 153 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_lt.con" as lemma.
 154
 155 (*#* Syntax *)
 156
 157 (* NOTATION
 158 Infix "/" := Zdiv : Z_scope.
 159 *)
 160
 161 (* NOTATION
 162 Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
 163 *)
 164
 165 (*#* Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *)
 166
 167 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_ge.con" as lemma.
 168
 169 inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_plus.con" as lemma.
 170
 171 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_plus.con" as lemma.
 172
 173 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mult.con" as lemma.
 174
 175 inline procedural "cic:/Coq/ZArith/Zdiv/Z_mult_div_ge.con" as lemma.
 176
 177 inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_same.con" as lemma.
 178
 179 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_same.con" as lemma.
 180
 181 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_exact_1.con" as lemma.
 182
 183 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_exact_2.con" as lemma.
 184
 185 inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_zero_opp.con" as lemma.
 186