1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Zdiv.v,v 1.21.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
35 (* Contribution by Claude March\233\ and Xavier Urbain *)
41 Defines first of function that allows Coq to normalize.
42 Then only after proves the main required property.
46 include "ZArith/ZArith_base.ma".
48 include "ZArith/Zbool.ma".
50 include "ZArith/Zcomplements.ma".
53 Open Local Scope Z_scope.
58 Euclidean division of a positive by a integer
59 (that is supposed to be positive).
61 total function than returns an arbitrary value when
62 divisor is not positive
66 inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl_POS.con" as definition.
70 Euclidean division of integers.
72 Total function than returns (0,0) when dividing by 0.
82 if b <> 0 and a = 0 : (0,0)
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)
87 if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r)
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)
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|.
97 inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl.con" as definition.
99 (*#* Division and modulo are projections of [Zdiv_eucl] *)
101 inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv.con" as definition.
103 inline procedural "cic:/Coq/ZArith/Zdiv/Zmod.con" as definition.
107 Eval Compute in `(Zdiv_eucl 7 3)`.
109 Eval Compute in `(Zdiv_eucl (-7) 3)`.
111 Eval Compute in `(Zdiv_eucl 7 (-3))`.
113 Eval Compute in `(Zdiv_eucl (-7) (-3))`.
119 Main division theorem.
121 First a lemma for positive
125 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mod_POS.con" as lemma.
127 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mod.con" as theorem.
129 (*#* Existence theorems *)
131 inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl_exist.con" as theorem.
134 Implicit Arguments Zdiv_eucl_exist.
137 inline procedural "cic:/Coq/ZArith/Zdiv/Zdiv_eucl_extended.con" as theorem.
140 Implicit Arguments Zdiv_eucl_extended.
143 (*#* Auxiliary lemmas about [Zdiv] and [Zmod] *)
145 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mod_eq.con" as lemma.
147 inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_lt.con" as lemma.
149 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_POS_ge0.con" as lemma.
151 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_ge0.con" as lemma.
153 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_lt.con" as lemma.
158 Infix "/" := Zdiv : Z_scope.
162 Infix "mod" := Zmod (at level 40, no associativity) : Z_scope.
165 (*#* Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *)
167 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_ge.con" as lemma.
169 inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_plus.con" as lemma.
171 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_plus.con" as lemma.
173 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_mult.con" as lemma.
175 inline procedural "cic:/Coq/ZArith/Zdiv/Z_mult_div_ge.con" as lemma.
177 inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_same.con" as lemma.
179 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_same.con" as lemma.
181 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_exact_1.con" as lemma.
183 inline procedural "cic:/Coq/ZArith/Zdiv/Z_div_exact_2.con" as lemma.
185 inline procedural "cic:/Coq/ZArith/Zdiv/Z_mod_zero_opp.con" as lemma.