aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Update before joining all signatures into one.Gravatar emakarov2007-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10119 85f007b7-540e-0410-9357-904b9bb8a0f7
* - renaming Qle_shift_recip_r into Qle_shift_inv_r, etcGravatar roconnor2007-09-07
| | | | | | | | | | | | - Adding Qlt_shift_div_l, etc - Adding Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b). - Adding Qle_Qabs : forall a, a <= Qabs a. - Removing redudnent Qminus' x y := Qred (Qminus x y) from Qabs. It is already defined elsewhere (in it's proper place). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10118 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a few lemmas for reasoning about inequalities over the Gravatar roconnor2007-08-28
| | | | | | | rationals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10101 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add more equality tactics. Upgrade program_simpl for discrimination of ↵Gravatar msozeau2007-08-26
| | | | | | conjuncts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10093 85f007b7-540e-0410-9357-904b9bb8a0f7
* An update on axiomatic number classes.Gravatar emakarov2007-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10075 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix dependency bugs due to Program modules renamings.Gravatar msozeau2007-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10064 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 better Program documentation. Include it in the generated stdlib doc.Gravatar msozeau2007-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move Program tactics into a proper theories/ directory as they are general ↵Gravatar msozeau2007-08-07
| | | | | | purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7
* mul and sqrtGravatar thery2007-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n etGravatar notin2007-07-25
| | | | | | | | do_norm. Corrigé par analogie avec N11, N12, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10048 85f007b7-540e-0410-9357-904b9bb8a0f7
* proof of compare addedGravatar thery2007-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10045 85f007b7-540e-0410-9357-904b9bb8a0f7
* An update on axiomatization of numbers.Gravatar emakarov2007-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10041 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
* J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir Gravatar aspiwack2007-07-18
| | | | | | | | | | | | 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
* An update on axiomatization of number classes.Gravatar emakarov2007-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Qpower_plus' and Zpower_QpowerGravatar roconnor2007-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small cleanupGravatar letouzey2007-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9996 85f007b7-540e-0410-9357-904b9bb8a0f7
* Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans leGravatar herbelin2007-07-13
| | | | | | | | 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
* Deletion of some firstorder calls in FSetAVL: Gravatar letouzey2007-07-13
| | | | | | | | | 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
* Proof for subGravatar thery2007-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9990 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deletion of an obsolete file (euclidian division done in old syntax with ↵Gravatar letouzey2007-07-12
| | | | | | realizers) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9987 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
* Proof for succ, add, predGravatar thery2007-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added ForAll_Str_nth_tlGravatar roconnor2007-07-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9967 85f007b7-540e-0410-9357-904b9bb8a0f7
* Big reorganization of romega/ReflOmegaCore.v: towards a modular Gravatar letouzey2007-07-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Update of theories/Numbers directory.Gravatar emakarov2007-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9955 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update on numbers.Gravatar emakarov2007-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Qpower_mult theorem.Gravatar roconnor2007-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9946 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité des noms longs de Bool déplacés dans DatatypesGravatar herbelin2007-07-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction (partielle) du bug #1587Gravatar notin2007-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9931 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the directory theories/Numbers where axiomatizations and ↵Gravatar emakarov2007-06-29
| | | | | | 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
* - Extensions of FMap(Weak)Facts: Gravatar letouzey2007-06-27
| | | | | | | | | | | | | | | 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
* eqlistA is now equivlistAGravatar letouzey2007-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added zwqipWith.Gravatar roconnor2007-06-26
| | | | | | | 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
* additional properties for FMap (and slight rework of SetoidList and ↵Gravatar letouzey2007-06-26
| | | | | | FSetProperties) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated Qpow_tac to work on a a more realistic set of exponent values.Gravatar roconnor2007-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9907 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout exist & cie à la table des hints par symétrie avec ex_intro &Gravatar herbelin2007-06-22
| | | | | | | | | | 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
* Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, Gravatar notin2007-06-21
| | | | | | | | 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
* Adding: Field instance for Q.Gravatar roconnor2007-06-21
| | | | | | | | : 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
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9900 85f007b7-540e-0410-9357-904b9bb8a0f7
* safe_shift correct recursionGravatar thery2007-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9899 85f007b7-540e-0410-9357-904b9bb8a0f7
* safe_shift recursionGravatar thery2007-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9898 85f007b7-540e-0410-9357-904b9bb8a0f7
* safe_shift recursionGravatar thery2007-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9897 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding function is_even, safe_shiftl, safe_shiftrGravatar thery2007-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9894 85f007b7-540e-0410-9357-904b9bb8a0f7
* genN.ml syncGravatar thery2007-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct height computationGravatar thery2007-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9892 85f007b7-540e-0410-9357-904b9bb8a0f7
* oups: one file forgotten in my previous commitGravatar letouzey2007-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9891 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rework of FSetProperties, in order to add more easily a Properties functor Gravatar letouzey2007-06-14
| | | | | | | | 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
* undeletion of E_ST and Equal_ST: these records aren't mandatory, but quite ↵Gravatar letouzey2007-06-11
| | | | | | useful git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9887 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 08:26:14 +0000