aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
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-22Rename obligations_tactic to obligation_tactic and fix bugs #1893.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11164 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-20typo in a commentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11155 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-13Temporary fix for bug #1876, printing fails because of unresolvedmsozeau
globals. Change program_simpl to use [auto] and not [auto with *]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11124 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-12Changing the definitions of pred and minus in the style of GGwerner
in order for them to preserve the structural order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11115 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-11Zpow_facts.Zmult_power: kills a useless hypothesisletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11098 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-10- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.herbelin
- Test match dépendant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11095 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-10- Correct handling of DependentMorphism error, using tclFAIL instead ofmsozeau
letting the exception go uncatched. - Reorder definitions in Morphisms, move the PER on (R ==> R') in Morphisms where it can be declared properly. Add an instance for Equivalence => Per. - Change bug#1604 test file to the new semantics of [setoid_rewrite at] - More unicode characters parsed by coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-08- Patch sur "intros until 0"herbelin
- MAJ CHANGES et COMPATIBILITY - Réservation de || et && dans Notations.v - code mort et MAJ suite commit 11072 (tactics.ml et changes.txt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11073 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-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
Minor fix in Morphisms which prevented working with higher-order morphisms and PER relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11065 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06avoid duplicated creation of WFacts instancesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11064 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Fix setoid_rewrite documentation examples.msozeau
Debug handling of identifiers in coqdoc (should work with modules and sections) and add missing macros. Move theories/Program to THEORIESVO to put the files in the standard library documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 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-02Petites corrections diverses :herbelin
- bug d'installation (coq_config.cmo était installé une 2ème fois au lieu d'installer coq_config.cmx) - suite nettoyage configure, option reals - ajout d'une option "only parsing" oubliée dans Peano.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11035 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-30Improve the dependent induction tactic to automatically find themsozeau
generalized hypotheses. Also move part of the tactic to ML and improve the generated proof term in case of non-dependent induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11023 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-28- Modification de la déf de minus et pred conformément aux remarques deherbelin
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
2008-05-28Notation concise pour la valeur par défaut des cas reconnus commeherbelin
impossibles dans un filtrage dépendant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11014 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-28- Correction bug highlighting "Module" dans Coqideherbelin
- Divers code mort (evarutil.ml, Bvector.v) - MAJ perf-analysis git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11004 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 08:55:20 +0000