aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
...
* Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope.Gravatar letouzey2010-11-16
| | | | | | | | | | | No infix notation "rem" for Zrem (that will probably become Z.rem in a close future). This way, we avoid conflict with people already using rem for their own need. Same for BigZ. We still use infix rem, but only in the abstract layer of Numbers, in a way that doesn't inpact the rest of Coq. Btw, the axiomatized function is now named rem instead of remainder. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13640 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups, fix last commit, a missing file in a vo.itargetGravatar letouzey2010-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13634 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (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
* Numbers: axiomatization, properties and implementations of gcdGravatar letouzey2010-11-05
| | | | | | | | | | | | | | | | | | | - 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
* Add small utility lemmas about nat/P/Z/Q arithmetic.Gravatar letouzey2010-11-02
| | | | | | Initial patch by Eelis van der Weegen, minor adaptations by myself git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13613 85f007b7-540e-0410-9357-904b9bb8a0f7
* NZSqrt : since spec is complete, no need for morphism axiom sqrt_wdGravatar letouzey2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13609 85f007b7-540e-0410-9357-904b9bb8a0f7
* NZLog : since spec is complete, no need for morphism axiom log2_wdGravatar letouzey2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: misc improvementsGravatar letouzey2010-11-02
| | | | | | | | | - Add alternate specifications of pow and sqrt - Slightly more general pow_lt_mono_r - More explicit equivalence of Plog2_Z and log_inf - Nicer proofs in Zpower git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers : log2. Abstraction, properties and implementations.Gravatar letouzey2010-11-02
| | | | | | | | | | 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
* NArith: a log2 functionGravatar letouzey2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13605 85f007b7-540e-0410-9357-904b9bb8a0f7
* NPeano: A log2 function for natGravatar letouzey2010-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: specs about sqrt and pow of neg numbers, even in NZGravatar letouzey2010-11-02
| | | | | | | 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
* Numbers: NZPowProp as a Module Type, some module variable renamingGravatar letouzey2010-11-02
| | | | | | | | | We temporary use a hack to convert a module type into a module Module M := T is refused, so we force an include via Module M := Nop <+ T where Nop is an empty module. To be fixed later more beautifully... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
| | | | | | | Beware! after this, a ./configure must be done. It might also be a good idea to chase any phantom .vo remaining after a make clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 85f007b7-540e-0410-9357-904b9bb8a0f7
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
| | | | | | | | | | Program in terms of implicit arguments to the rest of the library. This commit only covers the case of list of implicit arguments that have a different length in Program (e.g. inl, Vcons) but not the case of implicit arguments which differs only in their maximality status (e.g. pair). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13575 85f007b7-540e-0410-9357-904b9bb8a0f7
* FMapFacts: typo noticed by AaronGravatar letouzey2010-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13572 85f007b7-540e-0410-9357-904b9bb8a0f7
* Still another Open Scope than should be LocalGravatar letouzey2010-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solve name conflict about pow introduced by commit 13546.Gravatar letouzey2010-10-21
| | | | | | | - NPeano isn't Exported by default anymore (contains pow for nat). - in coq_micromega.ml, we specify more where to find the pow of R. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13569 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups, new file Zsqrt_def was exporting Z_scopeGravatar letouzey2010-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13567 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: no need for advanced functions (e.g. sqrt) in NStrongRec, NDefOps, etcGravatar letouzey2010-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13565 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add sqrt in NumbersGravatar letouzey2010-10-19
| | | | | | | | | | | | | | | | | | | | | | 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
* Numbers : also axiomatize constants 1 and 2.Gravatar letouzey2010-10-14
| | | | | | | | | | | | | | | | | 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
* Numbers: new functions pow, even, odd + many reorganisationsGravatar letouzey2010-10-14
| | | | | | | | | | | | | | | | | | | | | | | | - 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
* Zeven: some complements, e.g. proofs that Zeven_bool and co are okGravatar letouzey2010-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13545 85f007b7-540e-0410-9357-904b9bb8a0f7
* NArith: add some functions Neven and NoddGravatar letouzey2010-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13544 85f007b7-540e-0410-9357-904b9bb8a0f7
* NArith: Definition of a Npow power functionGravatar letouzey2010-10-14
| | | | | | | | | | | | | By the way, adds an Piter_op iterator : Piter_op op p a is "a op a ... op a" with a occurring p times. It could be use to define Pmult_nat and hence nat_of_P (not fully done for maintaining compatibility). Unlike iter_pos, Piter_op is logarithmic in p, not linear. Note: We should adapt someday the brain-damaged Zpower to make it use Piter_op instead of iter_pos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using multiple lists of implicit arguments in Program for preservingGravatar herbelin2010-10-03
| | | | | | | | | | | | | | the compatibility with the rest of the theories. Used multiple lists of implicit arguments in Init only when the maximality status is not modified in Program (and thus the compatibility is strictly preserved). This improves the compatibility for the implicit arguments of eq_refl and JMeq_refl between 8.2 and 8.3 when using Program (up to the residual differences in the maximality status). For the constants Acc_inv, inl, inr, left, right, Vnil, Vcons, the compatibility with 8.2 is not improved but the consistency between Program and the rest of the library is. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bvector.Vshiftin was wrong for agesGravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: re-introduce some eta-expansions in rare situations leading to ↵Gravatar letouzey2010-09-20
| | | | | | | | | | | | | | | | | | | | | '_a types If there's no lambdas at the top of a constant body and its type is functional and this type contains type variable and we're extracting to Ocaml then we perform one eta-expansion to please the ML type-checker This might slow down things, if some computations are shared thanks to the partial application. But it seems quite unlikely to encounter both situations (clever partial application and non-generalizable variable) at the same time. Compcert is ok, for instance. As a consequence, no need for manual eta-expansion in AVL code (and by the way MSetAVL.element wasn't a problem, it is monomorphic) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13441 85f007b7-540e-0410-9357-904b9bb8a0f7
* For the moment, two small manual eta-expansions to avoid '_a after extractionGravatar letouzey2010-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13425 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake : another round of heavy reworkGravatar letouzey2010-09-09
| | | | | | | | | | | | | | | | - generic iterator [iter] factorized in the same way as [same_level] - as a consequence, remaining operations [mul] [compare] [div_gt] are now defined and proved in a short and nice way and moved to NMake.v. - lots of other simplifications / factorisations in NMake_gen. This file is still macro-generated, but is much shorter, and the major part of it is now invariant. - As advised by B. Gregoire, try to (re)create clever partial applications in code of operators, in order to avoid projecting ZnZ fields all the time in base cases. Case 0 can still be improved, but it's already better this way :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [clenv_missing] to compute a better approximation of missingGravatar msozeau2010-08-02
| | | | | | | | | | dependent arguments. It breaks compatibility as some [apply with] clauses are not necessary anymore. Typically when applying [f_equal], the domain type of the function can be infered even if it does not appear directly in the conclusion of the goal. Fixes bug #2154. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed commit r13359 which was incomplete for its "trunk" part. ThanksGravatar herbelin2010-07-31
| | | | | | to Julien for noticing it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rather quick hack to make basic unicode notations available byGravatar herbelin2010-07-29
| | | | | | requiring a file Utf8_core. That needs to be improved... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite Heap merging so that it extracts to an O(n log n) definition.Gravatar msozeau2010-07-28
| | | | | | | Fixes bug #2047. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13345 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes:Gravatar msozeau2010-07-27
| | | | | | | | | - Document and fix [autounfold] - Fix warning about default Firstorder tactic object not being defined - Fix treatment of implicits in Program Lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made notations for exists, exists! and notations of Utf8.v recursive notationsGravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backported r13308 (ConstructiveEpsilon.v) to branch v8.3Gravatar herbelin2010-07-22
| | | | | | Also removed trailing spaces of the file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13309 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of ConstructiveEpsilon.v by Jean-François Monin.Gravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetPositive: mention MSetInterface instead of FSetInterfaceGravatar letouzey2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13288 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSetPositive: sets of positive inspired by FMapPositive.Gravatar letouzey2010-07-16
| | | | | | | | | | Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant. I've also included a MSets version, hence FSetPositive might become soon a mere wrapper for MSetPositive, as for other FSets implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bool: shorter and more systematic proofs + an iff lemma about eqbGravatar letouzey2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13286 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bool: iff lemmas about or, a reflect inductive, an is_true functionGravatar letouzey2010-07-10
| | | | | | | | | | | For the moment, almost no lemmas about (reflect P b), just the proofs that it is equivalent with an P<->b=true. is_true b is (b=true), and is meant to be added as a coercion if one wants it. In the StdLib, this coercion is not globally activated, but particular files are free to use Local Coercion... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13275 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSets/Msets: some renaming of module params to simplify the task of the ↵Gravatar letouzey2010-07-05
| | | | | | extraction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13239 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sorting library: export as hints only lemmas that obviously simplifyGravatar herbelin2010-07-02
| | | | | | | | | | | | the size of the problem to solve. This is still more powerful than what 8.2 provided since no hints were exported yet when Permutation was in List.v in 8.2. Whether no hints should be exported at all, and whether hints should be exported in a specific database or not is unclear. At least, the contribs apparently supported the extra added power of auto introduced in r12585 (date of the revision of the Sorting library), so let's continue with it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13231 85f007b7-540e-0410-9357-904b9bb8a0f7
* QArith: typo in name of hint db (fix #2346)Gravatar letouzey2010-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13220 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 08:05:31 +0000