aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-11-10 12:58:38 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-11-10 12:58:38 +0000
commitf1da4e3df5abd1daa5bfee184512f1e363bc9688 (patch)
tree4dc54964cdf6cf05b9d060fb6ed0f5898a2bad41 /theories/Structures
parent51f5f4d37fdc3db1e7da951db11119bdb5a7554b (diff)
Integer division: quot and rem (trunc convention) in addition to div and mod
(floor convention). We follow Haskell naming convention: quot and rem are for Round-Toward-Zero (a.k.a Trunc, what Ocaml, C, Asm do by default, cf. the ex-ZOdiv file), while div and mod are for Round-Toward-Bottom (a.k.a Floor, what Coq does historically in Zdiv). We use unicode รท for quot, and infix rem for rem (which is actually remainder in full). This way, both conventions can be used at the same time. Definitions (and proofs of specifications) for div mod quot rem are migrated in a new file Zdiv_def. Ex-ZOdiv file is now Zquot. With this new organisation, no need for functor application in Zdiv and Zquot. On the abstract side, ZAxiomsSig now provides div mod quot rem. Zproperties now contains properties of them. In NZDiv, we stop splitting specifications in Common vs. Specific parts. Instead, the NZ specification is be extended later, even if this leads to a useless mod_bound_pos, subsumed by more precise axioms. A few results in ZDivTrunc and ZDivFloor are improved (sgn stuff). A few proofs in Nnat, Znat, Zabs are reworked (no more dependency to Zmin, Zmax). A lcm (least common multiple) is derived abstractly from gcd and division (and hence available for nat N BigN Z BigZ :-). In these new files NLcm and ZLcm, we also provide some combined properties of div mod quot rem gcd. We also provide a new file Zeuclid implementing a third division convention, where the remainder is always positive. This file instanciate the abstract one ZDivEucl. Operation names are ZEuclid.div and ZEuclid.modulo. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13633 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Structures')
-rw-r--r--theories/Structures/OrdersEx.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index f8a08bf4e..ffc5b91bc 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -22,7 +22,7 @@ Require Import Orders NPeano POrderedType NArith
Module Nat_as_OT := NPeano.Nat.
Module Positive_as_OT := POrderedType.Positive_as_OT.
Module N_as_OT := NArith.N.
-Module Z_as_OT := ZArith.Z.
+Module Z_as_OT := ZBinary.Z.
(** An OrderedType can now directly be seen as a DecidableType *)