| Age | Commit message (Collapse) | Author |
|---|
|
automatically instead
|
|
- Zpow_def, Zpower, Zpow_facts shortened thanks to stuff in BinInt.Z
- The alternative Zpower_alt is now in a separate file Zpow_alt.v,
not loaded by default.
- Some more injection lemmas in Znat (pow, div, mod, quot, rem)
- Btw, added a "square" function in Z, N, Pos, ... (instead of
Zpow_facts.Zsquare).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14253 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14247 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14246 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14244 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In particular, we merge the old Zdivide (used to be an ad-hoc
inductive predicate) and the new Z.divide (based on exists).
Notations allow to do that (almost) transparently, the only
impact is that the name picked by the system will not be "q"
anymore when destructing a Z.divide. Some fragile scripts
may have to be fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14239 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
All the functions about Z is now in a separated file BinIntDef,
which is Included in BinInt.Z. This BinInt.Z directly
implements ZAxiomsSig, and instantiates derived properties ZProp.
Note that we refer to Z instead of t inside BinInt.Z,
otherwise ring breaks later on @eq Z.t
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
See NatInt/NZBits.v for the common axiomatization of bitwise functions
over naturals / integers. Some specs aren't pretty, but easier to
prove, see alternate statements in property functors {N,Z}Bits.
Negative numbers are considered via the two's complement convention.
We provide implementations for N (in Ndigits.v), for nat (quite dummy,
just for completeness), for Z (new file Zdigits_def), for BigN
(for the moment partly by converting to N, to be improved soon)
and for BigZ.
NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
the reversed order (for consistency with the rest of the world):
for instance BigN.shiftl 1 10 is 2^10.
NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
on negative numbers. For the moment I've kept it intact, and have
just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
To reorganize someday ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(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
|
|
- For nat, we create a brand-new gcd function, structural in
the sense of Coq, even if it's Euclid algorithm. Cool...
- We re-organize the Zgcd that was in Znumtheory, create out of it
files Pgcd, Ngcd_def, Zgcd_def. Proofs of correctness are revised
in order to be much simpler (no omega, no advanced lemmas of
Znumtheory, etc).
- Abstract Properties NZGcd / ZGcd / NGcd could still be completed,
for the moment they contain up to Gauss thm. We could add stuff
about (relative) primality, relationship between gcd and div,mod,
or stuff about parity, etc etc.
- Znumtheory remains as it was, apart for Zgcd and correctness proofs
gone elsewhere. We could later take advantage of ZGcd in it.
Someday, we'll have to switch from the current Zdivide inductive,
to Zdivide' via exists. To be continued...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Btw, we finally declare the original Zpower as the power on Z.
We should switch to a more efficient one someday, but in the
meantime BigN is proved with respect to the old one.
TODO: reform Zlogarithm with respect to Zlog_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13606 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
As for power recently, we add a specification in NZ,N,Z,
derived properties, implementations for nat, N, Z, BigN, BigZ.
- For nat, this sqrt is brand new :-), cf NPeano.v
- For Z, we rework what was in Zsqrt: same algorithm,
no more refine but a pure function, based now on a sqrt
for positive, from which we derive a Nsqrt and a Zsqrt.
For the moment, the old Zsqrt.v file is kept as Zsqrt_compat.v.
It is not loaded by default by Require ZArith.
New definitions are now in Psqrt.v, Zsqrt_def.v and Nsqrt_def.v
- For BigN, BigZ, we changed the specifications to refer to Zsqrt
instead of using characteristic inequations.
On the way, many extensions, in particular BinPos (lemmas about order),
NZMulOrder (results about squares)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13564 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12714 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Numbers/.../ZBinary.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12670 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in */*/vo.itarget
On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
if you want a partial build, make a specific rule such as theories-light
Beware: these vo.itarget should not contain comments. Even if this is legal
for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
|
