| Age | Commit message (Collapse) | Author |
|---|
|
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
|
|
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Note that in NSig (and hence NMake and BigN), to_N is now
Z.to_N (to_Z ...) instead of Z.abs_N (to_Z ...). This doesn't
change the result (since to_Z create non-negative integers),
but some proofs may have to be adapted
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14250 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Start of a uniform treatment of compare, eqb, leb, ltb:
- We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos
- Some generic properties are derived in OrdersFacts.BoolOrderFacts
In BinPos, more work about sub_mask with nice implications
on compare (e.g. simplier proof of lt_trans).
In BinNat/BinPos, for uniformity, compare_antisym is now
(y ?= x) = CompOpp (x ?=y) instead of the symmetrical result.
In BigN / BigZ, eq_bool is now eqb
In BinIntDef, gtb and geb are kept for the moment, but
a comment advise to rather use ltb and leb. Z.div now uses
Z.ltb and Z.leb.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
To avoid names¬ations clashs with list, Vector shouldn't be
"Import"ed but one can "Import Vector.VectorNotations." to have
notations.
SetoidVector at least remains to do.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Now we have:
- Zdiv and Zdiv2 : round toward bottom, no easy sign rule, remainder
of a/2 is 0 or 1, operations related with two's-complement Zshiftr.
- Zquot and Zquot2 : round toward zero, Zquot2 (-a) = - Zquot2 a,
remainder of a/2 is 0 or Zsgn a.
Ok, I'm introducing an incompatibility here, but I think coherence is
really desirable. Anyway, people using Zdiv on positive numbers only
shouldn't even notice the change. Otherwise, it's just a matter of
sed -e "s/div2/quot2/g".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13695 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
|
|
No infix notation "rem" for Zrem (that will probably become Z.rem in
a close future). This way, we avoid conflict with people already using
rem for their own need. Same for BigZ. We still use infix rem, but
only in the abstract layer of Numbers, in a way that doesn't inpact
the rest of Coq. Btw, the axiomatized function is now named rem
instead of remainder.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13640 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
|
|
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
|
|
Initially, I was using notation 1 := (S 0) and so on. But then, when
implementing by NArith or ZArith, some lemmas statements were filled
with Nsucc's and Zsucc's instead of 1 and 2's.
Concerning BigN, things are rather complicated: zero, one, two
aren't inlined during the functor application creating BigN.
This is deliberate, at least for the other operations like BigN.add.
And anyway, since zero, one, two are defined too early in NMake,
we don't have 0%bigN in the body of BigN.zero but something complex that
reduce to 0%bigN, same for one and two. Fortunately, apply or
rewrite of generic lemmas seem to work, even if there's BigZ.zero
on one side and 0 on the other...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- ring/field: detection of constants for ring/field,
detection of power, potential use of euclidean division.
- for BigN and BigZ, x^n now takes a N as 2nd arg instead of a positive
- mention that we can use (r)omega thanks to (ugly) BigN.zify, BigZ.zify.
By the way, BigN.zify could still be improved (no insertion of positivity
hyps yet, unlike the original zify).
- debug of BigQ.qify (autorewrite was looping on spec_0).
- for BigQ, start of a generic functor of properties QProperties.
- BigQ now implements OrderedType, TotalOrder, and contains facts
about min and max.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12681 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We use the <+ operation to regroup all known facts about BigN
(resp BigZ, ...) in a unique module. This uses also the new ! feature
for controling inlining. By the way, we also make sure that these
new BigN and BigZ modules implements OrderedTypeFull and TotalOrder,
and also contains facts about min and max (cf. GenericMinMax).
Side effects:
- In NSig and ZSig, specification of compare and eq_bool is now
done with respect to Zcompare and Zeq_bool, as for other ops.
The order <= and < are also defined via Zle and Zlt, instead
of using compare. Min and max are axiomatized instead of being
macros.
- Some proofs rework in QMake
- QOrderedType and Qminmax were in fact not compiled by make world
Still todo: OrderedType + MinMax for BigQ, etc etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12680 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
NB: for declaring div and mod as a morphism, even when divisor is zero,
I've slightly changed the definition of div_eucl: it now starts by a
check of whether the divisor is zero. Not very nice, but this way
we can say that BigN.div and BigZ.div _always_ answer like Zdiv.Zdiv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12646 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This allow to really finish files about division.
An abs and sgn is added to BigZ.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12644 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* Isolate and put forward the interfaces NSig and ZSig that describe
what should contain structures of natural numbers and integers (specs
are done by translation to ZArith).
* Functors NSigNAxioms and ZSigZAxioms proving that these NSig and
ZSig implements the fully-abstract NAxioms and ZAxioms module types.
* BigN and BigZ now contains more notations, plus an export of all
abstract results proved by Evgeny instantiated thanks to NSigNAxioms
and ZSigZAxioms. In addition, BigN and BigZ are declared as
(semi/full)-rings.
* as a consequence, some incompatibities have to be fixed in BigQ:
- take care of some name masking (via Import, Open Scope ...)
- some additionnal constants like BigN.lt to deal with
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
