| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
| |
A sub-module N in BinNat now contains functions add (ex-Nplus),
mul (ex-Nmult), ... and properties.
In particular, this sub-module N directly instantiates NAxiomsSig
and includes all derived properties NProp.
Files Ndiv_def and co are now obsolete and kept only for compat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
BinPos now contain a sub-module Pos, in which are placed functions
like add (ex-Pplus), mul (ex-Pmult), ... and properties like
add_comm, add_assoc, ...
In addition to the name changes, the organisation is changed quite
a lot, to try to take advantage more of the orders < and <= instead
of speaking only of the comparison function.
The main source of incompatibilities in scripts concerns this compare:
Pos.compare is now a binary operation, expressed in terms of the
ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg),
this ternary version being called now Pos.compare_cont. As for everything
else, compatibility notations (only parsing) are provided. But notations
"_ ?= _" on positive will have to be edited, since they now point to
Pos.compare.
We also make the sub-module Pos to be directly an OrderedType,
and include results about min and max.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14098 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
checking types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14023 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13943 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations
eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y),
(Plt=lt x y) (Pgt=lt y x), but this may not be always the case,
especially for Pgt. The former CompSpec is now defined in term of
CompareSpec. Compatibility is preserved (except maybe a rare unfold
or red to break the CompSpec definition).
Typically, CompareSpec looks nicer when we have infix notations, e.g.
forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x)
while CompSpec is shorter when we directly refer to predicates:
forall x y, CompSpec eq lt x y (compare x y)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
conversion when checking types of instanciations while having
restricted delta reduction for unification itself. This
makes auto/eauto... backward compatible.
- Change semantics of [Instance foo : C a.] to _not_ search
for an instance of [C a] automatically and potentially slow
down interaction, except for trivial classes with no fields.
Use [C a := _.] or [C a := {}] to search for an instance of
the class or for every field.
- Correct treatment of transparency information for classes
declared in sections.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Initial patch by Robbert Krebbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13900 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13851 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
conversion.
- Fix trans_fconv* to use evars correctly.
- Normalize the goal with respect to evars before rewriting in
[rewrite], allowing to see instanciations from other subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For Argument Scope, we now record types (more precisely classes cl_typ)
in addition to scope list. After substitution (e.g. at functor application),
the new types are used to search for corresponding concrete scopes.
Currently, this automatic scope substitution of argument scope takes
precedence (if successful) over scope declared in the functor (even
by the user). On the opposite, the manual scope substitution
(cf last commit introducing annotation [scope foo to bar])
is done _after_ the automatic scope substitution.
TODO: if this behavior is satisfactory, document it ...
Note that Classops.find_class_type lose its env args since it was
actually unused, and is now used for Notation.find_class
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13840 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- The experimental syntax "<30>F M" is transformed into "F M [inline at level 30]"
- The earlier syntax !F X should now be written "F X [no inline]"
(note that using ! is still possible for compatibility)
- A new annotation "F M [scope foo_scope to bar_scope]" allow to substitute
foo_scope by bar_scope in all arguments scope of objects in F.
BigN and BigZ are cleaned from the zillions of Arguments Scope used earlier.
Arguments scope for lemmas are fixed for instances of Numbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13839 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As said in CHANGES:
<<
The inlining done during application of functors can now be controlled
more precisely. In addition to the "!F G" syntax preventing any inlining,
we can now use a priority level to select parameters to inline :
"<30>F G" means "only inline in F the parameters whose levels are <= 30".
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
the flag "Set Inline Level ..." to set a level.
>>
Nota : the syntax "Parameter Inline(30) foo" is equivalent to
"Set Inline Level 30. Parameter Inline foo.",
and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G."
For instance, in ZBinary, eq is @Logic.eq and should rather be inlined,
while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined.
We could achieve this behavior by setting a level such as 30 to the
parameter eq, and then tweaking the current level when applying functors.
This idea of levels might be too restrictive, we'll see, but at least
the implementation of this change was quite simple. There might be
situation where parameters cannot be linearly ordered according to their
"inlinablility". For these cases, we would need to mention names to inline
or not at a functor application, and this is a bit more tricky
(and might be a pain to use if there are many names).
No documentation for the moment, since this feature is experimental
and might still evolve.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
According to B. Gregoire, this stuff is obsolete. Fine control
on when to launch the VM in conversion problems is now provided
by VMcast. We were already almost never boxing definitions anymore
in stdlib files.
"(Un)Boxed Definition foo" will now trigger a parsing error,
same with Fixpoint. The option "(Un)Set Boxed Definitions"
aren't there anymore, but tolerated (as no-ops), since unknown
options raise a warning instead of an error by default.
Some more cleaning could be done in the vm.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
We now specify testbit by some initial and recursive equations.
The previous spec (via a complex split of the number in
low and high parts) is now a derived property in {N,Z}Bits.v
This way, proofs of implementations are quite simplier.
Note that these new specs doesn't imply anymore that testbit is a
morphism, we have to add this as a extra spec (but this lead
to trivial proofs when implementing).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13792 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13764 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
For example, if we know that [f] is a morphism for [E1==>E2==>E],
then the goal [E (f x y) (f x' y')] will be transformed by [f_equiv]
into the subgoals [E1 x x'] and [E2 y y'].
This way, we can remove most of the explicit use of the morphism
instances in Numbers (lemmas foo_wd for each operator foo).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13763 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- a ltac solve_proper which generalizes solve_predicate_wd and co
- using le_elim is nicer that (apply le_lteq; destruct ...)
- "apply ->" can now be "apply" most of the time.
Benefit: NumPrelude is now almost empty
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13762 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
By writing y instead of 0 in the branch where y is 0,
Coq can see that (modulo x y) is a structural subterm of y
(but not necessarily a strict one).
Same trick for div, but here it doesn't help.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13722 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13721 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The auxiliary variable q is now increased continuously instead
of being doubled from time to time. Interest: this version is
obviously linear, and specification proofs are slightly simplier.
NB: the previous version was in fact also linear I think, but
proving this requires a proper complexity analysis.
I'm sure this algorithm is related with some cellular automata
stuff in the spirit of the firing squad :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13720 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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Initial plan was only to add shiftl/shiftr/land/... to N and
other number type, this is only partly done, but this work has
diverged into a big reorganisation and improvement session
of PArith,NArith,ZArith.
Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a)
PArith/BinPos:
- added a power function Ppow
- iterator iter_pos moved from Zmisc to here + some lemmas
- added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2
- more lemmas on Pcompare and succ/+/* and order, allow
to simplify a lot some old proofs elsewhere.
- new/revised results on Pminus (including some direct proof of
stuff from Pnat)
PArith/Pnat:
- more direct proofs (limit the need of stuff about Pmult_nat).
- provide nicer names for some lemmas (eg. Pplus_plus instead of
nat_of_P_plus_morphism), compatibility notations provided.
- kill some too-specific lemmas unused in stdlib + contribs
NArith/BinNat:
- N_of_nat, nat_of_N moved from Nnat to here.
- a lemma relating Npred and Nminus
- revised definitions and specification proofs of Npow and Nlog2
NArith/Nnat:
- shorter proofs.
- stuff about Z_of_N is moved to Znat. This way, NArith is
entirely independent from ZArith.
NArith/Ndigits:
- added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr
- revised proofs about Nxor, still using functional bit stream
- use the same approach to prove properties of Nand Nor Ndiff
ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff
ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat
ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N
ZArith/Zmisc: almost empty new, only contain stuff about badly-named
iter. Should be reformed more someday.
ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes
proofs and avoid slowdown due to adding 1 in Z instead of in positive
Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt
as long as I dont't know why it's slower on powers of two.
Elsewhere: propagate new names + some nicer proofs
NB: Impact on compatibility is probably non-zero, but should be
really moderate. We'll see on contribs, but a few Require here
and there might be necessary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13651 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Some more results about sqrt. Similar results for sqrt_up.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13649 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
as log2
Some more results about log2. Similar results for log2_up.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13648 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13634 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13609 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13608 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- Add alternate specifications of pow and sqrt
- Slightly more general pow_lt_mono_r
- More explicit equivalence of Plog2_Z and log_inf
- Nicer proofs in Zpower
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13607 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13604 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
These additional specs are useless (but trivially provable) for N.
They are quite convenient when deriving properties in NZ.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13603 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
We temporary use a hack to convert a module type into a module
Module M := T is refused, so we force an include via
Module M := Nop <+ T where Nop is an empty module.
To be fixed later more beautifully...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13602 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13565 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@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- generic iterator [iter] factorized in the same way as [same_level]
- as a consequence, remaining operations [mul] [compare] [div_gt]
are now defined and proved in a short and nice way and moved to
NMake.v.
- lots of other simplifications / factorisations in NMake_gen.
This file is still macro-generated, but is much shorter,
and the major part of it is now invariant.
- As advised by B. Gregoire, try to (re)create clever partial
applications in code of operators, in order to avoid projecting
ZnZ fields all the time in base cases. Case 0 can still be improved,
but it's already better this way :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13402 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13212 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13095 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
people use the undocumented "Lemma foo x : t" feature in a way
incompatible with this activation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
|