aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith
Commit message (Collapse)AuthorAge
* Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.Gravatar herbelin2009-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12370 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
| | | | | | | | | | | | | | | | | | | 1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.Gravatar herbelin2009-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12358 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
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
| | | | | | | | | | | | Mostly results about Zgcd (commutativity, associativity, ...). Slight improvement of ZMicromega. Beware: some lemmas of Zdiv/ Znumtheory were asking for too strict or useless hypothesis. Some minor glitches may occur. By the way, some iff lemmas about negb in Bool.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed extra space in printing notation { x & P } + minor other thingsGravatar herbelin2009-08-11
| | | | | | (shorter proof of O_S in trunk + typo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12271 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12250 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
| | | | | | | I wonder how many of us were aware of the existence of such syntax ;-) Anyway, it is now subsumed by "rewrite by". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12248 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
| | | | | | | | | | | | | | - "*" implements Arthur Charguéraud's "introv" - "**" works as "; intros" (see also "*" in ssreflect). - Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui. - Shy attempt to seize the opportunity to clean Zarith_dec but Coq's library is really going anarchically (see a summary of the various formulations of total order, dichotomy of order and decidability of equality and in stdlib-project.tex in branch V8revised-theories). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7
* adds a theorem to reason at the level of ZGravatar bertot2009-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12119 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some additions in Max and Zmax. Unifiying list of statements and namesGravatar herbelin2009-04-14
| | | | | | | | in both files. Late update of CHANGES wrt classical Tauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12084 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith/Int: no need to load romega here (but rather in FullAVL)Gravatar letouzey2009-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12027 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
| | | | | | | | | | | | | - Backtrack on precise unfolding of "iff" in "tauto": it has effects on the naming of hypotheses (especially when doing "case H" with H of type "{x|P<->Q}" since not unfolding will eventually introduce a name "i" while unfolding will eventually introduce a name "a" (deep sigh). - Miscellaneous (error when a plugin is missing, doc hnf, standardization of names manipulating type constr_pattern, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zdiv: eqm (equality modulo some N) can now be declared as Parametric RelationGravatar letouzey2008-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11476 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tauto breaking not only binary "conjunctions" seems like a bad ideaGravatar msozeau2008-07-24
| | | | | | | after all... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11259 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oops... forgot some debug code.Gravatar msozeau2008-07-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11247 85f007b7-540e-0410-9357-904b9bb8a0f7
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
| | | | | | | | | | | It breaks tauto as [?X _ _] matches much more terms. It is mostly fixed by not destructing objects of record types. The new [intuition] was also pulling an unneeded dependency in Field_theory which can be cleared easily. Zis_gcd_bezout is also considered a conjunction now, which seems correct(?). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11243 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
* Zpow_facts.Zmult_power: kills a useless hypothesisGravatar letouzey2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11098 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
| | | | | | | | | | | | | | | | | - Ajout clause "in" à "remember" (et passage du code en ML). - Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute aussi une égalité pour se souvenir du terme sur lequel l'induction ou l'analyse de cas s'applique. - Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de Programs qui avait la sémantique de "pose proof" tandis que le nouveau a la même sémantique que "pose (id:=t)"). - Un peu de réorganisation, uniformisation de noms dans Arith, et ajout EqNat dans Arith. - Documentation tactiques et notations de tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11072 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Modification de la déf de minus et pred conformément aux remarques deGravatar herbelin2008-05-28
| | | | | | | | | | | Assia et Benjamin W. de telle sorte qu'ils respectent le critère de décroissance structurelle lorsqu'utilisés dans un point-fixe. - Ajout des noms "standard" des lemmes de Peano et correction d'un nom de BinInt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11015 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cyclic31: migrate auxiliary lemmas to their legitimate filesGravatar letouzey2008-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cyclic31 : proof of the spec of gcd31Gravatar letouzey2008-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10997 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
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
| | | | | | | | | | | | | | | complexité exponentielle dans la machine lazy depuis que l'algo de compilation du filtrage évite systématiquement d'expanser quand le filtrage n'est pas dépendant. - Un peu plus de colorisation dans coqide. - Utilisation de formats pour améliorer de l'affichage des notations Utf8. - Systématisation paire Local/Global dans g_vernac.ml4 (même si le défaut n'est pas toujours le même) - Bug Makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10918 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
| | | | | | | | now. Fix proof scripts that failed correspondingly. Should make many contribs compile again... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10863 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
| | | | | | | | | | | | | substitution. Makes unification succeed a bit more often, hence auto works better in some cases. - Backtrack the changes of auto using Hint Unfold to do more delta and add a new tactic "new auto" which does that, for compatibility. The first fix may have a big impact on the contribs, whereas the second should make them compile again... we'll see. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10855 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug 1816 (ajout d'un lemme dans Znat) et suppressionGravatar notin2008-03-28
| | | | | | | | d'un test non significatif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
| | | | | | | | | | | | | | | | | | implementation. Mostly syntax changes when declaring parametric relations, but also some declarations were relying on "default" relations on some carrier. Added a new DefaultRelation type class that allows to do that, falling back to the last declared Equivalence relation by default. This will be bound to Add Relation in the next commit. Also, move the "left" and "right" notations in Program.Utils to "in_left" and "in_right" to avoid clashes with existing scripts. Minor change to record to allow choosing the name of the argument for the record in projections to avoid possible incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
| | | | | | | | | | | | | | | | | | | | 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
* one more substitution s/Set/Type/Gravatar letouzey2008-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10617 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proposal of a nice notation for constructors xI and xO of type positiveGravatar letouzey2008-02-10
| | | | | | | | More details in the header of BinPos.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10547 85f007b7-540e-0410-9357-904b9bb8a0f7
* one forgotten compatibility lemmaGravatar letouzey2008-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10526 85f007b7-540e-0410-9357-904b9bb8a0f7
* Keep the Z_scope local to this file.Gravatar roconnor2008-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding Zdiv_le_compat_lGravatar thery2008-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10461 85f007b7-540e-0410-9357-904b9bb8a0f7
* A result about Zsgn(a/b), both for Zdiv and ZOdivGravatar letouzey2007-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10313 85f007b7-540e-0410-9357-904b9bb8a0f7
* First reasonably complete version of ZOdiv, including some propertiesGravatar letouzey2007-11-10
| | | | | | | | | | | that aren't so nice after all. For instance, ((a+b*c) mod c) might differ from (a mod c), due to sign issues. Minor improvements to Zdiv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10312 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 ↵Gravatar jforest2007-11-09
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* more about ZOdiv and ZOmod (still not finished)Gravatar letouzey2007-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10307 85f007b7-540e-0410-9357-904b9bb8a0f7
* setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. Gravatar letouzey2007-11-08
| | | | | | | | | | | | | | A file ZOdiv is added which contains results about this euclidean division. Interest compared with Zdiv: ZOdiv implements others (better?) conventions concerning negative numbers, in particular it is compatible with Caml div and mod. ZOdiv is only partially finished... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10302 85f007b7-540e-0410-9357-904b9bb8a0f7
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
| | | | | | | | more general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension ↵Gravatar letouzey2007-11-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | of Zdiv Some details: - ZAux.v is the only file left in Ints/Z. The few elements that remain in it are rather specific or compatibility oriented. Others parts and files have been either deleted when unused or pushed into some place of ZArith. - Ints/List/ is removed since it was not needed anymore - Ints/Tactic.v disappear: some of its tactic were unused, some already in Tactics.v (case_eq, f_equal instead of eq_tac), and the nice contradict has been added to Tactics.v - Znumtheory inherits lots of results about Zdivide, rel_prime, prime, Zgcd, ... - A new file Zpow_facts inherits lots of results about Zpower. Placing them into Zpower would have been difficult with respect to compatibility (import of ring) - A few things added to Zmax, Zabs, Znat, Zsqrt, Zeven, Zorder - Adequate adaptations to Ints/num/* (mainly renaming of lemmas) Now, concerning Zdiv, the behavior when dividing by a negative number is now fully proved. When this was possible, existing lemmas has been extended, either from strictly positive to non-zero divisor, or even to arbitrary divisor (especially when playing with Zmod). These extended lemmas are named with the suffix _full, whereas the original restrictive lemmas are retained for compatibility. Several lemmas now have shorter proofs (based on unicity lemmas). Lemmas are now more or less organized by themes (division and order, division and usual operations, etc). Three possible choices of spec for divisions on negative numbers are presented: this Zdiv, the ocaml approach and the remainder-always-positive approach. The ugly behavior of Zopp with the current choice of Zdiv/Zmod is now fully covered. A embryo of division "a la Ocaml" is given: Odiv and Omod. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding Qround.v (and helper lemmas and hints)Gravatar roconnor2007-11-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10282 85f007b7-540e-0410-9357-904b9bb8a0f7
* In agreement with Laurent Thery, start migration of auxiliary results Gravatar letouzey2007-11-01
| | | | | | | | | | | | present in Ints. For the moment, mainly: - Q parts go in QArith - Some of the Zdivide & Zgcd stuff go in Znumtheory More to come ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_leGravatar roconnor2007-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10242 85f007b7-540e-0410-9357-904b9bb8a0f7
* Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vGravatar emakarov2007-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10063 85f007b7-540e-0410-9357-904b9bb8a0f7
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ------------------------------------------------ See file PreOmega for more details and/or test-suite/succes/*Omega*.v The zify tactic performs a Z-ification of your current goal, transforming parts of type nat, N, positive, taking advantage of many equivalences of operations, and of the positivity implied by these types. Integration with omega and romega: (r)omega : the earlier tactics, 100% compatible (r)omega with * : full zify applied before the (r)omega run (r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z}, applies only specific parts of zify (btw "with Z" means take advantage of Zmax, Zmin, Zabs and Zsgn). As a particular consequence, "romega with nat" should now be a close-to-perfect replacement for omega. Slightly more powerful, since (forall x:nat, x*x>=0) is provable and also slightly less powerful: if False is somewhere in the hypothesis, it doesn't use it. For the moment zify is done in a direct way in Ltac, using rewrite when necessary, but crucial chains of rewrite may be made reflexive some day. Even though zify is designed to help (r)omega, I think it might be of interest for other tactics (micromega ?). Feel free to complete zify if your favorite operation / type isn't handled yet. Side-effects: - additional results for ZArith, NArith, etc... - definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope - romega now start by doing "intros". Since the conclusion will be negated, and this operation will be justified by means of decidability, it helps to have as little as possible in the conclusion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 85f007b7-540e-0410-9357-904b9bb8a0f7
* normalisation (by closure) was not performed under fixpointsGravatar barras2007-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Transparency of Z_lt_le_decGravatar notin2007-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug nommage Zgt_trans_succGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9438 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 01:44:49 +0000