aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/NatInt
AgeCommit message (Collapse)Author
2010-01-29Division in numbers: kills some Include to avoid bad alias Zsucc = ZDiv.Z.Z'.Sletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12704 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-17BigN, BigZ, BigQ: presentation via unique module with both ops and propsletouzey
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
2010-01-17Simplification of OrdersTac thanks to the functor application ! with no inlineletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12679 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-14Avoid some more re-declarations of Equivalence instancesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12671 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-08Numbers: BigN and BigZ get instantiations of all properties about div and modletouzey
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
2010-01-08NZAxioms plus a compare allows to build an OrderedTypeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12642 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
Old stuff DecidableType.v and OrderedType.v stay there and keep their names for the moment, for compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12641 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Include can accept both Module and Module Typeletouzey
Syntax Include Type is still active, but deprecated, and triggers a warning. The syntax M <+ M' <+ M'', which performs internally an Include, also benefits from this: M, M', M'' can be independantly modules or module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Numbers: separation of funs, notations, axioms. Notations via module, ↵letouzey
without scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12639 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-06"by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ↵letouzey
by ...") Application in some proofs of Numbers's abstract division git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12630 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-05Numbers abstract layer: more Module Type, used especially for divisions.letouzey
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
2010-01-05Avoid declaring hints about refl/sym/trans of eq in DecidableType2letouzey
This used to be convenient in FSets, but since we now try to integrate DecidableType and OrderedType as foundation for other part of the stdlib, this should be avoided, otherwise some eauto take a _long_ time. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-05Division in Numbers: proofs with less auto (less sensitive to hints, in ↵letouzey
particular about eq) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12625 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-05Division in Numbers: factorisation of signaturesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12624 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
NB: the grammar entry is placed in vernac:command on purpose even if it should have gone into vernac:gallina_ext. Camlp4 isn't factorising rules starting by "Declare" in a correct way otherwise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-17Division in Numbers : more properties, new filenames based on a paper by R. ↵letouzey
Boute Following R. Boute (paper "the Euclidean Definition of the Functions div and mod"): - ZDivFloor.v for Coq historical division (former ZDivCoq.v) - ZDivTrunc.v for Ocaml convention (former ZDivOcaml.v) - ZDivEucl.v for "Mathematical" convention 0<=r (former ZDivMath.v) These property functors are more or less finished (except that sign and abs stuff should be migrated to a separate file). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12594 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-16Division in Numbers: more properties proved (still W.I.P.)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12591 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-15A generic euclidean division in Numbers (Still Work-In-Progress)letouzey
- 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
2009-12-10NZDomain: investigation of the shape of NZ domain, more results about ↵letouzey
ofnat:nat->NZ.t git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12575 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Diamond-shape instead of linear hiearchy in Numbers/NatIntletouzey
NZBase -- NZAdd -- NZMul | | NZOrder ---------- NZAddOrder -- NZMulOrder -- NZProperties This is done by transforming NZBase into a functorial module type, and making NZAdd NZMul NZOrder accept an instance of NZBase as parameter. This is possible thanks to a combination of various new features of modules: - interactive proofs in module type (ie functors can be turned into type functors) - Include Type in Module (ie type functors can be turned into functors) - Include Self, <+ , etc, etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12534 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
"Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for "Module M (...). Include M1. Include M2. Include M3... End M." Moreover M2,M3,etc can be functors as long as they find what they need in what comes before them (see new command "Include Self"). The only real constraint is that M1,M2,M3,... should not have common elements (for the moment (?)). Same behavior for signature : Module Type M := M1 <+ M2 <+ M3. Note that this <+ is _not_ a primitive construct of the module language, for instance it cannot be used in signature (Module M <: M1 <+ M2 is illegal for the moment). Some example of use in Decidable2 and NZAxioms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-16Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsletouzey
We can now have a diamond-like approch to extentions of signatures, instead of a linear-only chains as earlier... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12529 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10Simplification of Numbers, mainly thanks to Includeletouzey
- 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
2009-11-06Numbers: more (syntactic) changes toward new style of type classesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12475 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-03Numbers: start using Classes stuff, Equivalence, Proper, Instance, etcletouzey
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
2009-10-08Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-12Uniformity with the rest of the StdLib : _symm --> _symletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11675 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
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
2008-06-02In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
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
2008-05-22switch theories/Numbers from Set to Type (both the abstract and the bignum ↵letouzey
part). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10964 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-15Coq headers + $ in theories/Numbers filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10934 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-08remove mention of an obsolete limitation of Add Morphismletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10908 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-27Suite r10857herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10858 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-07Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partmsozeau
of the fix I added an optional "by" annotation for rewrite to solve said conditions in the same tactic call. Most of the theories have been updated, only FSets is missing, Pierre will take care of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-06Plug the new setoid implemtation in, leaving the original one commentedmsozeau
out. The semantics of the old setoid are faithfully simulated by the new tactic, hence no scripts involving rewrite are modified. However, parametric morphism declarations need to be changed, but there are only a few in the standard library, notably in FSets. The declaration and the introduction of variables in the script need to be tweaked a bit, otherwise the proofs remain unchanged. Some fragile scripts not introducting their variable names explicitely were broken. Requiring Setoid requires Program.Basics which sets stronger implicit arguments on some constants, a few scripts benefit from that. Ring/field have been ported but do not really use the new typeclass architecture as well as they could. Performance should be mostly unchanged, but will certainly improve in the near future. Size of the vo's seems not to have changed at all. It will certainly break some contribs using Setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10631 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-22An update on Numbers. Added two files dealing with recursion, for ↵emakarov
information only. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10330 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-16Added theorems; created NZPlusOrder from NTimesOrder.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10325 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-14Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ↵emakarov
ZArith/Zorder on MacOS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10323 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-08Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10304 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-07Replaced BinNat with a new version that is based on ↵emakarov
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
2007-11-03An update of theories/Numbersemakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10285 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-23Added Numbers/Natural/Abstract/NIso.v that proves that any two models of ↵emakarov
natural numbers are isomorphic. Added NatScope and IntScope for abstract developments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10247 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-16Added transitivity and irreflexivity of <, as well as < -elimination for ↵emakarov
binary positive numbers. Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-02The following now compiles: abstract integers with plus, minus and times, ↵emakarov
binary implementation and integers as pairs of natural numbers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10167 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-01Added the compilation of theories/Numbers to Makefile.common. The following ↵emakarov
things compile: abstract natural numbers and integers with plus, times, minus, and order; Peano and binary implementations for natural numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10161 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-25An update on theories/Numbers.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10142 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-21Update on theories/Numbers. Natural numbers are mostly complete,emakarov
need to make NZOrdAxiomsSig a subtype of NAxiomsSig. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10132 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 18:25:46 +0000