aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/NatInt/NZBase.v
AgeCommit message (Collapse)Author
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2013-07-17More dynamic argument scopesletouzey
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
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-11Annotations at functor applications:letouzey
- 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
2011-01-04f_equiv : a clone of f_equal that handles setoid equivalencesletouzey
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
2011-01-03Numbers: some improvements in proofsletouzey
- 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
2010-10-14Numbers: new functions pow, even, odd + many reorganisationsletouzey
- 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
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- 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
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-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
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-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-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
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-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-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-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-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-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-04-24 07:03:41 +0000