coq/theories/Numbers/vo.itarget, branch master

drop vo.itarget files and compute the corresponding the corresponding values automatically instead

2017-06-01T15:33:19+00:00

Definitions of positive, N, Z moved in Numbers/BinNums.v

2011-05-05T15:12:09+00:00

 In the coming reorganisation, the name Z in BinInt will be a
 module containing all code and properties about binary integers.
 The inductive type Z hence cannot be at the same location.
 Same for N and positive. Apart for this naming constraint, it
 also have advantages : presenting the three types at once is
 clearer, and we will be able to refer to N in BinPos (for instance
 for output type of a predecessor function on positive).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7

Numbers and bitwise functions.

2010-12-06T15:47:32+00:00

 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

Oups, fix last commit, a missing file in a vo.itarget

2010-11-10T13:14:13+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13634 85f007b7-540e-0410-9357-904b9bb8a0f7

Integer division: quot and rem (trunc convention) in addition to div and mod

2010-11-10T12:58:38+00:00

(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

Numbers: axiomatization, properties and implementations of gcd

2010-11-05T18:27:39+00:00

 - 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

Numbers : log2. Abstraction, properties and implementations.

2010-11-02T15:10:43+00:00

 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

Add sqrt in Numbers

2010-10-19T10:16:57+00:00

 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

Numbers: new functions pow, even, odd + many reorganisations

2010-10-14T11:37:33+00:00

 - Simplification of functor names, e.g. ZFooProp instead of ZFooPropFunct
 - The axiomatisations of the different fonctions are now in {N,Z}Axioms.v
   apart for Z division (three separate flavours in there own files).
   Content of {N,Z}AxiomsSig is extended, old version is {N,Z}AxiomsMiniSig.
 - In NAxioms, the recursion field isn't that useful, since we axiomatize
   other functions and not define them (apart in the toy NDefOps.v).
   We leave recursion there, but in a separate NAxiomsFullSig.
 - On Z, the pow function is specified to behave as Zpower : a^(-1)=0
 - In BigN/BigZ, (power:t->N->t) is now pow_N, while pow is t->t->t
   These pow could be more clever (we convert 2nd arg to N and use pow_N).
   Default "^" is now (pow:t->t->t). BigN/BigZ ring is adapted accordingly
 - In BigN, is_even is now even, its spec is changed to use Zeven_bool.
   We add an odd. In BigZ, we add even and odd.
 - In ZBinary (implem of ZAxioms by ZArith), we create an efficient Zpow
   to implement pow. This Zpow should replace the current linear Zpower
   someday.
 - In NPeano (implem of NAxioms by Arith), we create pow, even, odd functions,
   and we modify the div and mod functions for them to be linear, structural,
   tail-recursive.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13546 85f007b7-540e-0410-9357-904b9bb8a0f7

Numbers: properties of min/max with respect to 0,S,P,add,sub,mul

2010-02-09T17:45:06+00:00

 With these properties, we can kill Arith/MinMax, NArith/Nminmax,
 and leave ZArith/Zminmax as a compatibility file only. Now
 the instanciations NPeano.Nat, NBinary.N, ZBinary.Z, BigZ, BigN
 contains all theses facts.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12718 85f007b7-540e-0410-9357-904b9bb8a0f7