aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers
AgeCommit message (Collapse)Author
2009-03-27Parsing files for numerals (+ ascii/string) moved into pluginsletouzey
Idea: make coqtop more independant of the standard library. In the future, we can imagine loading the syntax for numerals right after their definition. For the moment, it is easier to stay lazy and load the syntax plugins slightly before the definitions. After this commit, the main (sole ?) references to theories/ from the core ml files are in Coqlib (but many parts of coqlib are only used by plugins), and it mainly concerns Init (+ Logic/JMeq and maybe a few others). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12024 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-10Cyclic31: proof of a forgotten admitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11906 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-12Uniformity with the rest of the StdLib : _symm --> _symletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11675 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
[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
2008-07-26Even better test for choosing rewrite or setoid_rewrite.msozeau
Now there is a class "SetoidRelation" for registering relations that should always be considered as setoids and never unfolded. Every "Add Relation" command adds an instance and impl,iff are there by default. Now the test is: if there is a SetoidRelation instance, use it ; otherwise, allow unfolding to find an eq or fallback on setoid_rewrite. To avoid searching for SetoidRelation instances repeateadly we check that it is really needed first by unfolding the hyp. Only two scripts relied on the now-forbidden semantics of rewriting by an @eq inside a setoid relation, in Numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11269 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-15Autour du parsing:herbelin
- Utilisation de notations de type "abbreviation paramétrée" plutôt que de notations introduisant des mots-clés, là où c'est possible (cela affecte QDen, in_left/in_right, inhabited, S/P dans NZCyclic). - Extension du lexeur pour qu'il prenne le plus long token valide au lieu d'échouer sur un plus long préfixe non valide de token (permet notamment de faire passer la notation de Georges "'C_ G ( A )" sans invalider toute séquence commençant par 'C et non suivie de _) - Rajout d'un point final à certains messages d'erreur qui n'en avaient pas. - Ajout String.copy dans string_of_label ("trou" de mutabilité signalé par Georges -- le "trou" lié aux vecteurs des noeuds App restant lui ouvert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-04Fix bug #1899: no more strange notations for Qge and Qgtletouzey
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
2008-07-01Various bug fixes in type classes and subtac:msozeau
- Cases on multiple objects - Avoid dangerous coercion with evars in subtac_coercion - Resolve typeclasses method-by-method to get better error messages. - Correct merging of instance databases (and add debug printer) - Fix a script in NOrder where a setoid_replace was not working before. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11198 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-30QMake : alternative equivalences with Qcanon thanks to earlier ↵letouzey
irreducibility results git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11194 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-28QMake: Proofs that add_norm and other ..._norm functions produce irreducible ↵letouzey
fractions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11186 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
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
2008-06-25Some work on BigQ :letouzey
* keep only one implementation of BigQ * QMake (ex-Q0Make) becomes functorial * proofs in it have been reworked, some new functions (e.g. red, power) * BigQ.t is declared to be a setoid and a field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11178 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
(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
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
- 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
2008-06-03In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
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
2008-06-02In abstract parts of theories/Numbers, plus/times becomes add/mul, letouzey
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
2008-06-02newton iteration for sqrt31thery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11034 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inletouzey
a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t))) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01BigQ: starting to create and use an interface QSigletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11028 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01Enhance the BigN and BigZ infrastructure: letouzey
* 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
2008-05-29NBigN: proofs that BigN implements axioms of NAxiomsSigletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11016 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are letouzey
now dumb wrappers around Zsqrt_plain. Wanted (dead or alive): better implemntations _and_ their proofs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11013 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-28Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left !letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11003 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-27Cyclic31: proof of auxiliary function iter_int31 + (failed) attempt at ↵letouzey
proving addmuldiv31 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11002 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-27Correction du problème de complexité de Print Assumptions :aspiwack
- Suite à une modification faite maladroitement, on ne se contentait pas de comparer le nom de la supposition quand on l'insérait dans l'ensemble des suppositions utilisées, mais aussi son type, ce qui était inutilement long (mais pas le facteur principal) - L'environnement était parcouru deux fois pour chaque variable de section. Ce n'était pas très grave vu qu'en général on a assez peu de variables de sections sous la main. Mais ça restait inutile. - Les noms qui ont déjà étés explorés sont maintenant memoizés, ce qui gagne dans le cas les pires (comme les théorèmes sur les réels typiquement) une exponentiel dans le temps de recherche (si on visualise l'espace de recherche comme un DAG, l'ancienne procédure le parcourais comme si il était un arbre, ce qui a une complexité exponentielle en la taille du DAG). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11001 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-27Cyclic31: migrate auxiliary lemmas to their legitimate filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10999 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-27Cyclic31 : proof of the spec of gcd31letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10997 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Int31 : gcd31 was wrongletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10995 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26Cyclic31: cleanup, 2 Admitted killed (6 remaining)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10993 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ↵letouzey
one. Conversion to lists of digits is really the Right Way (TM). Maybe other parts can also benefit from this idea. To be continued... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10978 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23(Not completely finished) proofs that int31 integers fulfill the ↵letouzey
CyclicAxioms specs Currently, 8 lemmas remains to tackle. One proof is done via a _very_ brute-force ugly approach. The all story for proving composition of phi and phi_inv (and the other way around) is surprisingly long and tricky. In both cases, comments are welcome, I may have missed an easier road (?) As a consequence of the above, we have a additional time-eager file in the stdlib (about a minute to compile here). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10973 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22writing a match on a digit via syntax "if ... then ... else" is not a good ↵letouzey
idea :-( (some bad interaction with Arnaud's framework ??) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10969 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22Proposition for a almost-bitsize-independent Int31.v (joint work with J. ↵letouzey
Vouillon) As said at the beginning of the file: This file contains basic definitions of a 31-bit integer arithmetic. In fact it is more general than that. The only reason for this use of 31 is the underlying mecanism for hardware-efficient computations by A. Spiwack. Apart from this, a switch to, say, 63-bit integers is now just a matter of replacing every occurences of 31 by 63. This is actually made possible by the use of dependently-typed n-ary constructions for the inductive type [int31], its constructor [I31] and any pattern matching on it. If you modify this file, please preserve this genericity. From the user point-of-view, almost nothing has changed: functions like On, In, shiftr, shiftl and a few others now have a syntactically-different definition, but thanks to Eval compute in their definition, this leads to the exact same coq objects as before. The only difference is "Check I31" that shows the compact n-ary version (nfun digits 31 int31) instead of (digits -> ... -> digits -> int31). But even "Print int31" shows the same answer as before (the above type of I31 is shown after expansion). Arnaud, could you check whether all this works fine with your retroknowledge ? Notice the new file NaryFunction that contain generic stuff about n-ary dependent functions. It should end some day in another place than theories/Numbers, but I cant figure where for now. This file is also quite skinny yet, but it's a start. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10967 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-22QRewrite is now obsolete. It was containing manual ltac stuffletouzey
for helping rewriting under Quantifiers and binders, but Matthieu's setoid rewrite now has the same kind of capabilities by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10966 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-19Thanks to Matthieu's commit 10941, Ad-hoc tactics contained in QRewrite are ↵letouzey
no longer needed to compile theories/Numbers. QRewrite will probably be removed in a latter commit (need to check 2-3 things first with Matthieu and Evgeny) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10943 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-17ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsletouzey
This isn't useful for BigN et BigZ, but it can't hurt; and moreover it's a simple way to understand CyclicAxioms. Next step: proving that Int31 is also an implementation of CyclicAxiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10942 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-17Fix a de Bruijn bug in setoid_rewrite when rewriting undermsozeau
a non-dependent product under a lambda. Now qiff can be replaced by a simple setoid_rewrite in NumPrelude. Change configure to not do stripping if compiling with -g... Add -g / CAMLDEBUG flags to the native compilation command too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10941 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-16ZTreeMod was meant to prove that BigZ correspond to the Integer Axioms.letouzey
In fact, for the moment, it was only containing a proof that Z/nZ implements the NatInt NZAxiomsSig. We move it to a more meaningful place and name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10937 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-15In practice, the new setoid rewrite (and the "at" syntax) allows to avoid letouzey
using the ad-hoc qsetoid_rewrite. Could QRewrite.v be made completely obsolete ? For the moment rewrite under fun and exists don't work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10935 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-11- Changement du code de Zplus pour accomoder ring qui sinon prend uneherbelin
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
2008-05-08remove mention of an obsolete limitation of Add Morphismletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10908 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-08Oups, my new version of NMake_gen.ml was relying on a 3.10 feature:letouzey
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
2008-05-08Integration of theories/Ints into theories/Numbers, again : better ↵letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-20 09:00:03 +0000