aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Znumtheory.v
Commit message (Collapse)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
| | | | | | | | | | | | | | | | | | | | This was decided during the Fall WG (2017). The aliases that are kept as deprecated are the ones where the difference is only a prefix becoming a qualified module name. The intention is to turn the warning for deprecated notations on. We change the compat version to 8.6 to allow the removal of VOld and V8_5.
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
| | | | | induction/elim over a dependent elimination principle for Prop arguments.
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
| | | | | | | Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | - For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | | | | | Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing typo in previous commit r15180.Gravatar herbelin2012-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15181 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - tauto/intuition now works uniformly on and, prod, or, sum, False, Empty_set, unit, True (and isomorphic copies of them), iff, ->, and on all inhabited singleton types with a no-arguments constructor such as "eq t t" (even though the last case goes out of propositional logic: this features is so often used that it is difficult to come back on it). - New dtauto and dintuition works on all inductive types with one constructors and no real arguments (for instance, they work on records such as "Equivalence"), in addition to -> and eq-like types. - Moreover, both of them no longer unfold inner negations (this is a souce of incompatibility for intuition and evaluation of the level of incompatibility on contribs still needs to be done). Incidentally, and amazingly, fixing bug #2680 made that constants InfA_compat and InfA_eqA in SetoidList.v lost one argument: old tauto had indeed destructed a section hypothesis "@StrictOrder A ltA@ thinking it was a conjunction, making this section hypothesis artificially necessary while it was not. Renouncing to the unfolding of inner negations made auto/eauto sometimes succeeding more, sometimes succeeding less. There is by the way a (standard) problem with not in auto/eauto: even when given as an "unfold hint", it works only in goals, not in hypotheses, so that auto is not able to solve something like "forall P, (forall x, ~ P x) -> P 0 -> False". Should we automatically add a lemma of type "HYPS -> A -> False" in the hint database everytime a lemma ""HYPS -> ~A" is declared (and "unfold not" is a hint), and similarly for all unfold hints? At this occasion, also re-did some proofs of Znumtheory. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15180 85f007b7-540e-0410-9357-904b9bb8a0f7
* Znumtheory: a correct version of a compatibility Zdivide_introGravatar letouzey2011-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14240 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clean-up of Znumtheory, deletion of Zgcd_defGravatar letouzey2011-06-24
| | | | | | | | | | | In particular, we merge the old Zdivide (used to be an ad-hoc inductive predicate) and the new Z.divide (based on exists). Notations allow to do that (almost) transparently, the only impact is that the name picked by the system will not be "q" anymore when destructing a Z.divide. Some fragile scripts may have to be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14239 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14237 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
| | | | | | | | | | | All the functions about Z is now in a separated file BinIntDef, which is Included in BinInt.Z. This BinInt.Z directly implements ZAxiomsSig, and instantiates derived properties ZProp. Note that we refer to Z instead of t inside BinInt.Z, otherwise ring breaks later on @eq Z.t git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 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
* 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
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - 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
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 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
* 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
* 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
* 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
* Mise en forme des theoriesGravatar notin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
* commit de field + renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de Zgcd_spec (compat.)Gravatar notin2006-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8990 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvel algorithme pour Zgcd (plus rapide) + un QcompareGravatar letouzey2006-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de précédence de l'argument du by de assert; ↵Gravatar herbelin2006-05-23
| | | | | | conséquences sur les .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
* On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_posGravatar letouzey2006-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8817 85f007b7-540e-0410-9357-904b9bb8a0f7
* typoGravatar letouzey2006-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8814 85f007b7-540e-0410-9357-904b9bb8a0f7
* un Zgcd calculant dans coqGravatar letouzey2006-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8813 85f007b7-540e-0410-9357-904b9bb8a0f7
* une fonction pouvant calculer le gcd en coqGravatar letouzey2006-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8809 85f007b7-540e-0410-9357-904b9bb8a0f7
* un Zgcd general gardant trace des coefsGravatar letouzey2006-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement, préservation de la compatibilité pour Z_lt_induction et ajout ↵Gravatar herbelin2005-05-02
| | | | | | plutôt de nouveaux énoncés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6984 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed hypotheses of Z_lt_induction (see #957)Gravatar herbelin2005-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6962 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Duplication temporaire des règles de syntaxe des pairesGravatar herbelin2003-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace ↵Gravatar herbelin2003-12-04
| | | | | | par un niveau ajoute dynamiquement; plus de limite vers le haut: divide au niveau 260 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵Gravatar herbelin2003-11-29
| | | | | | par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de lemmes de Znumtheory dans Zabs ou BinIntGravatar herbelin2003-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5018 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de Znumtheory.v dans ZArithGravatar letouzey2003-11-19
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4952 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 16:01:30 +0000