aboutsummaryrefslogtreecommitdiff
path: root/theories/Bool/Bool.v
AgeCommit message (Collapse)Author
2009-11-06Numbers: finish files NStrongRec and NDefOpsletouzey
- NStrongRec provides a "strong" recursor based on the usual one: recursive calls can be done here on any lower value. See binary log in NDefOps for an example of use. - NDefOps contains alternative definitions of usual operators (add, mul, ltb, pow, even, half, log) via usual or strong recursor, and proofs of correctness and/or of equivalence with axiomatized operators. These files were in the archive but not being compiled, some proofs of correction for functions defined there were missing. By the way, some more iff-style lemmas in Bool. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12476 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-09Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsletouzey
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
2008-04-17No compatibility notations for andb and co (this restore a correct Print output)letouzey
The benefit of these "only-parsing" notations in Bool.v were to avoid replacing qualified Bool.andb by Datatypes.andb and so on. But such Bool.xxxx are fairly rare (e.g. none in contribs), and these notations have one serious drawback: with them, Print andb leads to Datatypes.andb instead of the body of andb. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10812 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-17Prevent the apparition of &&& when printing a (if ... then ... else false)letouzey
and idem for |||, thanks to a specific scope lazy_bool_scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10811 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-27- notations &&& and ||| equivalent to andb and orb, letouzey
but with lazy behavior while (vm_)computing - FSetAVL.split has now a dedicated output type instead of ( ,( , )) - Some proof adaptations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10725 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-04migration from Set to Type of FSet/FMap + some dependencies...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-09Major revision of FSetAVL: more Function, including some non-structural onesletouzey
NB: this change adds about 10s of compile-time to a file that is already taking about 30s on my machine. If somebody strongly objects to this, contact me. I really think that the gain in uniformity, clarity, and computability (in Coq) worth the extra compile-time: no more function-by-tactic, everything (vm_)computes, and quite efficiently. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10545 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-05 Added the automatic generation of the boolean equality if possible and thevsiles
decidability of the usual equality Major changes: * andb_prop & andb_true_intro have been moved from Bool.v to Datatypes.v * added 2 files: * toplevel/ind_tables.ml* : tables where the boolean eqs and the decidability proofs are stored * toplevel/auto_ind_decl.ml* : code of the schemes that are automatically generated from inductives types (currently boolean eq & decidability ) * improvement of injection: if the decidability have been correctly computed, injection can now break the equalities over dependant pair How to use: Set Equality Scheme. to set the automatic generation of the equality when you create a new inductive type Scheme Equality for I. tries to create the equality for the already declared type I git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10180 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-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-04-28Déplacement des opérations sur bool dans l'état initialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9803 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Noms "canoniques" pour certaines des propriétés de xor.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9246 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17Modification des propriétés (svn:executable)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Nettoyage Bool:herbelin
Suppression de bool_2, bool_4 et bool_5 très ad hoc Renommage des lemmes demorgan* qui n'énoncent en fait pas les lois de de Morgan Tentative partielle de renommage (un peu) plus uniforme Pour les Hint: - bool_5 de core remplacé en mettant exact diff_false_true dans core (un peu plus faible mais marche dans la pratique pour les contribs) - bool_2 remplacé par la transitivité sur bool (plus fort mais OK dans la pratique, et pas trop fort pour ne pas atteindre la force de trans_eq) - bool_4 apparemment pas utilisé - andb_false_elim, spécifique, apparemment pas utilisé, et supprimé comme hint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8031 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-31Ajout décidabilitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7965 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Ajout delimiteur pour bool_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5321 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵herbelin
par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵herbelin
entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4751 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Syntax errorherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4653 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Suppression des surcharge de regles de grammaire en v7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4650 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26'Open Local Scope' en attendant que le core_scope sache se mettre devant ↵herbelin
implicitement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4485 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-26Passage de Destruct a NewDestruct; '-' pour negbherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4480 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13FSets, mais pas compile' par make worldfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4150 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-29Ne pas mettre d'associatif a droite au niveau 3 en V7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4088 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4047 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3979 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-09Making the sumbool functions transparent, so that they can used tobertot
compute even inside Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2846 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-06Standardisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2667 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-03-04Nouveau Rewrite-in plus economiquebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2507 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-28Ajout andb_true_eq pour PolyList.list_beqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2497 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-27Simplification de deux preuves. En outre ca simplifie leur extraction.letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2082 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1880 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-19Mise de (*i autour CVS infomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1619 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30Ajout de lemmes sur les booleensmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1508 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01- coqc : option -imagefilliatr
- coqmktop : manquaient des -I - tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau - correction d'un bug de Simpl avec Fix (découvert dans preuve FTA) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Elimination du 'delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1000 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-05Plus besoin de débrancher la preuve qui ne passait pasherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@804 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Ajout du langage de tactiquesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-02portage Omega (mais toujours pas Zpower et Zlogarithm)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@400 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-16mise sous CVSfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@318 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 11:00:24 +0000