aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/BigN
Commit message (Collapse)AuthorAge
* DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationGravatar letouzey2010-02-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Records of operations and specs in CyclicAxioms are now type classes (under a module ZnZ for qualification). We benefit from inference and from generic names: (ZnZ.mul x y) instead of (znz_mul (some_ops...) x y). - Beware of typeclasses unfolds: the line about Typeclasses Opaque w1 w2 ... is critical for decent compilation time (x2.5 without it). - Functions defined via same_level are now obtained from a generic version by (Eval ... in ...) during definition. The code obtained this way should be just as before, apart from some (minor?) details. Proofs for these functions are _way_ simplier and lighter. - The macro-generated NMake_gen.v contains only generic iterators and compare, mul, div_gt, mod_gt. I hope to be able to adapt these functions as well soon. - Spec of comparison is now fully done with respect to Zcompare - A log2 function has been added. - No more unsafe_shiftr, we detect the underflow directly with sub_c git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12713 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake (and hence BigN): shiftr, shiftl now in the signature NSigGravatar letouzey2010-01-25
| | | | | | | | we export the "safe" version of these functions, working for all input and not only reasonably small shifting arg. The former "unsafe" shiftr and shiftl are now unsafe_shiftr and unsafe_shiftl. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12688 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake: several things need not be macro-generatedGravatar letouzey2010-01-25
| | | | | | | The macro-generated .v file is now NMake_gen.v, while NMake.v now contain the static things (i.e. definition of gcd via mod). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ring31 : a ring structure and tactic for int31Gravatar letouzey2010-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12685 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake_gen: fix previous commit (some spaces were critical), remove some more ↵Gravatar letouzey2010-01-19
| | | | | | spaces git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12684 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake_gen: no more spaces at end of linesGravatar letouzey2010-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12683 85f007b7-540e-0410-9357-904b9bb8a0f7
* More improvements of BigN, BigZ, BigQ:Gravatar letouzey2010-01-18
| | | | | | | | | | | | | | | - 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
* BigN, BigZ, BigQ: presentation via unique module with both ops and propsGravatar letouzey2010-01-17
| | | | | | | | | | | | | | | | | | | | | 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
* Numbers: BigN and BigZ get instantiations of all properties about div and modGravatar letouzey2010-01-08
| | | | | | | | | 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
* BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)Gravatar letouzey2009-11-12
| | | | | | | | | | | | | | | | | | | | | | | - In fact, Bind Scope has no retrospective effect. Since we don't want it inside functor, we use it late, and hence we are forced to use manual "Arguments Scope" commands. - Added syntax for power in BigN / BigZ / BigQ. - Added syntax p#q in BigQ for representing fractions (constructor BigQ.Qq) as in QArith. Display of a rational numeral is hence either an integer (constructor BigQ.Qz) or something like 6756 # 8798. - Fix of function BigQ.Qred that was not simplifing (67#1) into 67. - More tests in test-suite/output/NumbersSyntax.v A nice one not in the test-suite: Time Eval vm_compute in BigQ.red ((2/3)^(-100000) * (2/3)^(100000)). = 1 : bigQ Finished transaction in 3. secs (3.284206u,0.004s) :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12507 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repair interpretation of numeral for BigQ, add a printer (close #2160)Gravatar letouzey2009-11-12
| | | | | | | | | | | | | | | on the way: - Added a testsuite output file - Try to avoid nasty unfolding (fix nfun ...) in type of I31. Idealy we would need a "Eval compute in" for the type of a inductive constructor - Stop opening Scopes for BigQ, BigN, BigZ by default The user should do some Open Scope. TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope (and so on for other operations), even with some Bind Scope around. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12504 85f007b7-540e-0410-9357-904b9bb8a0f7
* SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMaxGravatar letouzey2009-11-10
| | | | | | | | To retrieve the old behavior of spec_sub0 and spec_sub with precondition on order, just chain spec_sub with Zmax_r or Zmax_l. Idem with spec_pred0 and spec_pred. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12490 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
| | | | | | | | | | | | | | | | | - 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
| | | | | | | | | | | | [discriminated]] with a switch for using the more experimantal dnet impl for every hint. Also add [Hint Transparent/Opaque] which parameterize the dnet and the unification flags used by auto/eauto with a particular database. Document all this. Remove [Typeclasses unfold] directives that are no longer needed (everything is unfoldable by default) and move to [Typeclasses Transparent/Opaque] syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1899: no more strange notations for Qge and QgtGravatar letouzey2008-07-04
| | | | | | | | | | | | | | In fact, Qge and Ggt disappear, and we only leave notations for > and >= that map directly to Qlt and Qle. We also adopt the same approach for BigN, BigZ, BigQ. By the way, various clean-up concerning Zeq_bool, Zle_bool and similar functions for Q. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11205 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
| | | | | | | | | | | | | | | | | goals containing existentials and use transparency information on constants (optionally). Only used by the typeclasses eauto engine for now, but could be used for other hint bases easily (just switch a boolean). Had to add a new "creation" hint to be able to set said boolean upon creation of the typeclass_instances hint db. Improve the proof-search algorithm for Morphism, up to 10 seconds gained in e.g. Field_theory, Ring_polynom. Added a morphism declaration for [compose]. One needs to declare more constants as being unfoldable using the [Typeclasses unfold] command so that discrimination is done correctly, but that amounts to only 6 declarations in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11184 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
| | | | | | | | (résolution entre autres des bugs 1882, 1883, 1884). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11145 85f007b7-540e-0410-9357-904b9bb8a0f7
* In abstract parts of theories/Numbers, plus/times becomes add/mul, Gravatar letouzey2008-06-03
| | | | | | | | | | 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
* In abstract parts of theories/Numbers, plus/times becomes add/mul, Gravatar letouzey2008-06-02
| | | | | | | | | | 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
* Enhance the BigN and BigZ infrastructure: Gravatar letouzey2008-06-01
| | | | | | | | | | | | | | | | | | | | | | * 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
* NBigN: proofs that BigN implements axioms of NAxiomsSigGravatar letouzey2008-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11016 85f007b7-540e-0410-9357-904b9bb8a0f7
* CyclicAxioms: after discussion with Laurent, znz_WW and variants areGravatar letouzey2008-05-28
| | | | | | | | | transformed into generic functions, and aren't anymore fields of records znz_op/znz_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11012 85f007b7-540e-0410-9357-904b9bb8a0f7
* switch theories/Numbers from Set to Type (both the abstract and the bignum ↵Gravatar letouzey2008-05-22
| | | | | | part). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurateGravatar letouzey2008-05-16
| | | | | | | | | | | (n _must_ in fact be a power of 2). Worse: Z_31Z is just plain wrong since it is Z/(2^31)Z and not Z/31Z (my fault). As a consequence, switch to CyclicAxioms, Cyclic31, DoubleCyclic, etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10940 85f007b7-540e-0410-9357-904b9bb8a0f7
* BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZGravatar letouzey2008-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10939 85f007b7-540e-0410-9357-904b9bb8a0f7
* More BigNum cleanup: Gravatar letouzey2008-05-16
| | | | | | | | | | | * View of Int31 as a Z/nZ moved to file Z31Z.v (TO FINISH: specs are still admitted!) * Modular specification of Z/nZ moved to ZnZ and renamed CyclicType * More isolation between Cyclic/Abstract and Cyclic/DoubleCyclic * A few comments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq headers + $ in theories/Numbers filesGravatar letouzey2008-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10934 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups, my new version of NMake_gen.ml was relying on a 3.10 feature:Gravatar letouzey2008-05-08
| | | | | | | | | the very handy Printf.ifprintf was not available on earlier ocaml. This file now uses a very dirty compatibility hack. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10906 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration of theories/Ints into theories/Numbers, again : better ↵Gravatar letouzey2008-05-08
| | | | | | | | | | | | generation of NMake.v - genN.ml becomes NMake_gen.ml - no need to produce the corresponding binary: we use ocaml NMake_gen.ml > NMake.v - beware! redoing a ./configure is mandatory after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration of theories/Ints into theories/Numbers, part 3: auto-generation ↵Gravatar letouzey2008-05-08
| | | | | | of NMake.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10902 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration of theories/Ints into theories/Numbers, part 1: moving filesGravatar letouzey2008-05-07
For the moment, the Ints files are simply moved into directories in theories/Numbers with meaningful names. No filenames changed, apart from: Zaux.v -> theories/Numbers/BigNumPrelude.v MemoFn.v -> theories/Lists/StreamMemo.v More to come... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10899 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-17 20:42:51 +0000