aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/DoubleCyclic
AgeCommit message (Collapse)Author
2010-02-08DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generationletouzey
- 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
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-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
2009-04-14Rewrite autorewrite to use a dnet indexed by the left-hand sides (ormsozeau
rhs) of rewrite lemmas for efficient retrieval of matching lemmas. Autorewrite's implementation is still unchanged but the dnet can be used through the [hints] strategy of the new generalized rewrite. Now lemmas are checked to actually be rewriting lemmas at declaration time hence the change in DoubleSqrt where some unapplicable constants were declared as lemmas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12087 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28CyclicAxioms: after discussion with Laurent, znz_WW and variants areletouzey
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
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-19Minor improvement: group stuff about carry apart from stuff about zn2zletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10944 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-16Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurateletouzey
(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
2008-05-16BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10939 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-16More BigNum cleanup: letouzey
* 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
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-07Integration of theories/Ints into theories/Numbers, part 1: moving filesletouzey
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.25.1) at 2026-10-05 16:04:41 +0000