| Age | Commit message (Collapse) | Author |
|---|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
This was decided during the Fall WG (2017).
The aliases that are kept as deprecated are the ones where the difference
is only a prefix becoming a qualified module name.
The intention is to turn the warning for deprecated notations on.
We change the compat version to 8.6 to allow the removal of VOld and V8_5.
|
|
|
|
|
|
|
|
|
|
|
|
- The earlier proof-of-concept file NPeano (which instantiates
the "Numbers" framework for nat) becomes now the entry point
in the Arith lib, and gets renamed PeanoNat. It still provides
an inner module "Nat" which sums up everything about type nat
(functions, predicates and properties of them).
This inner module Nat is usable as soon as you Require Import Arith,
or just Arith_base, or simply PeanoNat.
- Definitions of operations over type nat are now grouped in a new
file Init/Nat.v. This file is meant to be used without "Import",
hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
starts (but no proofs about them).
- The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
where here Nat is Init/Nat.v).
- This Coq.Init.Nat module (with only pure definitions) is Include'd
in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
sometimes instead of just Nat (for instance when doing "Print plus").
Normally it should be ok to just ignore these "Init" since
Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
it's possible to get rid of these "Init" prefixes.
- Concerning predicates, orders le and lt are still defined in Init/Peano.v,
with their notations "<=" and "<". Properties in PeanoNat.Nat directly
refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
we cannot yet include an Inductive to implement a Parameter), but these
aliased predicates won't probably be very convenient to use.
- Technical remark: I've split the previous property functor NProp in
two parts (NBasicProp and NExtraProp), it helps a lot for building
PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:
Module Nat.
Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
... (** proofs of specifications for basic ops such as + * - *)
Include NBasicProp. (** generic properties of these basic ops *)
... (** proofs of specifications for advanced ops (pow sqrt log2...)
that may rely on proofs for + * - *)
Include NExtraProp. (** all remaining properties *)
End Nat.
- All other files in directory Arith are now taking advantage of PeanoNat :
they are now filled with compatibility notations (when earlier lemmas
have exact counterpart in the Nat module) or lemmas with one-line proofs
based on the Nat module. All hints for database "arith" remain declared
in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
files are still Require'd (or not) by Arith.v, just as before.
- Compatibility should be almost complete. For instance in the stdlib,
the only adaptations were due to .ml code referring to some Coq constant
name such as Coq.Init.Peano.pred, which doesn't live well with the
new compatibility notations.
|
|
When arguments scopes are set manually, nothing new, they stay
as they are (until maybe another Arguments invocation).
But when argument scopes are computed out of the argument type and
the Bind Scope information, this kind of scope is now dynamic:
a later Bind Scope will be able to impact the scopes of an earlier
constant. For Instance:
Definition f (n:nat) := n.
About f. (* Argument scope is [nat_scope] *)
Bind Scope other_scope with nat.
About f. (* Argument scope is [other_scope] *)
This allows to get rid of hacks for modifying scopes during functor
applications. Moreover, the subst_arguments_scope is now
environment-insensitive (needed for forthcoming changes in declaremods).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- 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@14237 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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
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
|
|
- 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
|
|
This allow for instance to remove the dependency of List.v toward Min.v
To prove max_l and co, we push Le.le_pred and Le.le_S_n into Peano.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12784 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12717 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12671 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Update Numbers that was implicitely using [simpl_relation] instead of
the default tactic [program_simpl].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12647 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Properties are now rather passed as functor arg instead of via Include or
some inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12629 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For Z, we propose 3 conventions for the sign of the remainder...
- Instanciation for nat in NPeano.
- Beginning of instanciation in ZOdiv.
Still many proofs to finish, etc, etc, but soon we will have a decent
properties database for all divisions of all instances of Numbers (e.g. BigZ).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12590 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- No more nesting of Module and Module Type, we rather use Include.
- Instead of in-name-qualification like NZeq, we use uniform
short names + modular qualification like N.eq when necessary.
- Many simplification of proofs, by some autorewrite for instance
- In NZOrder, we instantiate an "order" tactic.
- Some requirements in NZAxioms were superfluous: compatibility
of le, min and max could be derived from the rest.
- NMul removed, since it was containing only an ad-hoc result for
ZNatPairs, that we've inlined in the proof of mul_wd there.
- Zdomain removed (was already not compiled), idea of a module
with eq and eqb reused in DecidableType.BooleanEqualityType.
- ZBinDefs don't contain any definition now, migrate it to ZBinary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12489 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
TODO: finish removing the "Add Relation", "Add Morphism" fun_* fun2_*
TODO: now that we have Include, flatten the hierarchy...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12464 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
for increased consistency with bignums parts
(commit part II: names of files + additional translation minus --> sub)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
for increased consistency with bignums parts
(commit part I: content of files)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11039 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
part).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10964 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10934 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
ZArith/Zorder on MacOS.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new BinNat are notations for the development in Numbers. Also added min and max to the new natural numbers and integers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10298 85f007b7-540e-0410-9357-904b9bb8a0f7
|
