aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2007-07-24proof of compare addedthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10045 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-24An update on axiomatization of numbers.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10041 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
------------------------------------------------ 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
2007-07-18J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir aspiwack
noté cette erreur de ma part (copier/coller mon amour). Ça créait des soucis dans les dépendance dans l'ancienne architecture de Makefile, probablement dans la nouvelle aussi dans certaines circonstances. Exit les bêtise, c'est plus propre maintenant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10019 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13An update on axiomatization of number classes.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10002 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13Added Qpower_plus' and Zpower_Qpowerroconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9997 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13Small cleanupletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9996 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans leherbelin
répertoire Num. Suppression de ce dernier de l'archive courante. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9995 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13Deletion of some firstorder calls in FSetAVL: letouzey
after commit 9983 of Bruno concerning kernel/closure.ml, a few firstorder were awfully slow. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9994 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Proof for subthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9990 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Deletion of an obsolete file (euclidian division done in old syntax with ↵letouzey
realizers) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9987 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12normalisation (by closure) was not performed under fixpointsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9983 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-12Proof for succ, add, predthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9971 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-11Added ForAll_Str_nth_tlroconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9967 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-10Big reorganization of romega/ReflOmegaCore.v: towards a modular letouzey
and generic romega tactic... For the moment, nothing is visible yet from the user's point of view (hopefully). But internally, we prepare a romega that can works on any integer types. ReflOmegaCore is now separated in several modules: * First, an interface Int that specifies the minimal amount of things needed on our integer type for romega to work: - int should be a ring (re-use of ring_theory definition ;-) - it should come with an total order, compatible with + * - - we should have a decidable ternary comparison function - moreover, we ask one (and only one!) critical property specific to integers: a<b <-> a<=b-1 * Then a functor IntProperties derives from this interface all the various lemmas on integers that are used in the romega part, in particular the famous OMEGA?? lemmas. * The romega reflexive part is now in another functor IntOmega, that rely on some Int: no more Z inside. The main changes is that Z0 was a constructor whereas our abstract zero isn't. So matching Z0 is transformed into (if beq ... 0 then ...). With extensive use of && and if then else, it's almost clearer this way. * Finally, for the moment Z_as_Int show that Z fulfills our interface, and ZOmega = IntOmega(Z_as_Int) is used by the tactic. Remains to be done: - revision of the refl_omega to use any Int instead of just Z, and creating a user interface. - Int has no particular reason to use the leibniz equality (only rely on the beq boolean test). Setoids someday ? - a version with "semi-ring" for nat ? or rather a generic way to plug additional equations on the fly, e.g. n>=0 for every nat subpart ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9966 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-06Update of theories/Numbers directory.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9955 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-05Update on numbers.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9947 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-05Added Qpower_mult theorem.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9946 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-03Compatibilité des noms longs de Bool déplacés dans Datatypesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9936 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-02Correction (partielle) du bug #1587notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9931 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-29Added the directory theories/Numbers where axiomatizations and ↵emakarov
implementations (unary, binary, etc.) of different number classes (natural, integer, rational, real, complex, etc.) will be stored.Currently there are axiomatized natural numbers with two implementations and axiomatized integers. Modified Makefile accordingly but dod not include the new files in THEORIESVO yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9916 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-27- Extensions of FMap(Weak)Facts: letouzey
fold properties and induction principles for (weak) maps. - Simplification in SetoidList: the two important results fold_right_equivlistA and fold_right_add are now proved without using removeA and hence do not depend anymore on a decidable equality (good for maps and their arbitrary datas). In fact, removeA is not used at all anymore, but I leave it here (mostly), since it can't hurt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9914 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-27eqlistA is now equivlistAletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9913 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26Added zwqipWith.roconnor
Added theory about intractions between nth and map, and zipWith. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9909 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26additional properties for FMap (and slight rework of SetoidList and ↵letouzey
FSetProperties) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9908 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-25Updated Qpow_tac to work on a a more realistic set of exponent values.roconnor
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9907 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-22Ajout exist & cie à la table des hints par symétrie avec ex_intro &herbelin
cie (cf message coq-club 21/6/07). De plus, left/right inleft/inright, eux aussi dans Set/Type, y étaient déjà donc l'argument d'être dans Type n'est pas recevable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9906 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-21Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, notin
et une typo dans Eqdep_deq.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9905 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-21Adding: Field instance for Q.roconnor
: Power function from Q -> Z -> Q. : Absolute value function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9901 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-20ajout de head0 et tail0 en natifbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19safe_shift correct recursionthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9899 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19safe_shift recursionthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9898 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19safe_shift recursionthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9897 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19Adding function is_even, safe_shiftl, safe_shiftrthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9894 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-19genN.ml syncthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9893 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-18Correct height computationthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9892 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14oups: one file forgotten in my previous commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9891 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14Rework of FSetProperties, in order to add more easily a Properties functor letouzey
for FMap (for the moment in FMapFacts). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9890 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-11undeletion of E_ST and Equal_ST: these records aren't mandatory, but quite ↵letouzey
useful git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9887 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-08some more properties of fold and elements in FSetPropertiesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9885 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-08Removed an extra \tacindex occurrence for the tactic discriminate.emakarov
Added a tactic "now" which is nonrecursive but generalizes "trivial". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9884 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07Extension of NArith: Nminus, Nmin, etcletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07* For uniformity, FSetAVL uses Implicit Arguments (a bit)letouzey
* Some additionnal properties: - two more induction principles on sets - some results about union, filter, etc - Subset is declared to be a Setoid Relation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9882 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-06tail0thery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9877 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-05Gestion espaces dans notation _ = _ :> _herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9876 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-30mul_norm for Q fixedthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9871 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-28comparison functions should be Defined not Qedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9867 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-27As suggested by Pierre Casteran, fold for FSets/FMaps now takes a letouzey
(A:Type) instead of a (A:Set). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9863 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-25fix for bug #1347 (no more Scope pollution by FSets)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9861 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-22Comparaison JMeq/eq_depherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9849 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 22:14:49 +0000