aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* drop vo.itarget files and compute the corresponding the corresponding values ↵Gravatar Matej Kosik2017-06-01
| | | | automatically instead
* Remove v62 from stdlib.Gravatar Théo Zimmermann2016-10-24
| | | | | This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore.
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fixing typo absorption (bug #3751).Gravatar Hugo Herbelin2014-10-22
|
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
|
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
| | | | | | | Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | - For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Follow-up concerning eqb / ltb / leb comparisonsGravatar letouzey2011-06-21
| | | | | | | | | | | - All statement using reflect are made transparent. (Otherwise, since reflect isn't in Prop, extraction complains now about opaque Type definition). - remove two local Peqb_spec and Neqb_spec, now provided globally as Pos.eqb_spec and N.eqb_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14232 85f007b7-540e-0410-9357-904b9bb8a0f7
* First release of Vector library.Gravatar pboutill2010-12-10
| | | | | | | | | | To avoid names&notations clashs with list, Vector shouldn't be "Import"ed but one can "Import Vector.VectorNotations." to have notations. SetoidVector at least remains to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
| | | | | | | | | | | | | | | | | | | | | | | See NatInt/NZBits.v for the common axiomatization of bitwise functions over naturals / integers. Some specs aren't pretty, but easier to prove, see alternate statements in property functors {N,Z}Bits. Negative numbers are considered via the two's complement convention. We provide implementations for N (in Ndigits.v), for nat (quite dummy, just for completeness), for Z (new file Zdigits_def), for BigN (for the moment partly by converting to N, to be improved soon) and for BigZ. NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in the reversed order (for consistency with the rest of the world): for instance BigN.shiftl 1 10 is 2^10. NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2) on negative numbers. For the moment I've kept it intact, and have just added a Zdiv2' which is truly equivalent to (Zdiv _ 2). To reorganize someday ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some more revision of {P,N,Z}Arith + bitwise ops in NdigitsGravatar letouzey2010-11-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Initial plan was only to add shiftl/shiftr/land/... to N and other number type, this is only partly done, but this work has diverged into a big reorganisation and improvement session of PArith,NArith,ZArith. Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a) PArith/BinPos: - added a power function Ppow - iterator iter_pos moved from Zmisc to here + some lemmas - added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2 - more lemmas on Pcompare and succ/+/* and order, allow to simplify a lot some old proofs elsewhere. - new/revised results on Pminus (including some direct proof of stuff from Pnat) PArith/Pnat: - more direct proofs (limit the need of stuff about Pmult_nat). - provide nicer names for some lemmas (eg. Pplus_plus instead of nat_of_P_plus_morphism), compatibility notations provided. - kill some too-specific lemmas unused in stdlib + contribs NArith/BinNat: - N_of_nat, nat_of_N moved from Nnat to here. - a lemma relating Npred and Nminus - revised definitions and specification proofs of Npow and Nlog2 NArith/Nnat: - shorter proofs. - stuff about Z_of_N is moved to Znat. This way, NArith is entirely independent from ZArith. NArith/Ndigits: - added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr - revised proofs about Nxor, still using functional bit stream - use the same approach to prove properties of Nand Nor Ndiff ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N ZArith/Zmisc: almost empty new, only contain stuff about badly-named iter. Should be reformed more someday. ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes proofs and avoid slowdown due to adding 1 in Z instead of in positive Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt as long as I dont't know why it's slower on powers of two. Elsewhere: propagate new names + some nicer proofs NB: Impact on compatibility is probably non-zero, but should be really moderate. We'll see on contribs, but a few Require here and there might be necessary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13651 85f007b7-540e-0410-9357-904b9bb8a0f7
* Used multiple lists of implicit arguments to transfer the choices ofGravatar herbelin2010-10-23
| | | | | | | | | | Program in terms of implicit arguments to the rest of the library. This commit only covers the case of list of implicit arguments that have a different length in Program (e.g. inl, Vcons) but not the case of implicit arguments which differs only in their maximality status (e.g. pair). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bvector.Vshiftin was wrong for agesGravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bool: shorter and more systematic proofs + an iff lemma about eqbGravatar letouzey2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13286 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bool: iff lemmas about or, a reflect inductive, an is_true functionGravatar letouzey2010-07-10
| | | | | | | | | | | For the moment, almost no lemmas about (reflect P b), just the proofs that it is equivalent with an P<->b=true. is_true b is (b=true), and is meant to be added as a coercion if one wants it. In the StdLib, this coercion is not globally activated, but particular files are free to use Local Coercion... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13275 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kill some useless dependencies (Bvector, Program.Syntax)Gravatar letouzey2010-02-17
| | | | | | | | Bvector uses only Minus, so let's avoid loading Arith (and hence ArithRing and hence parts of Z, N) Program.Syntax no longer need Lists now that list is in Datatypes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵Gravatar letouzey2009-12-09
| | | | | | | | | | | | in */*/vo.itarget On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: finish files NStrongRec and NDefOpsGravatar letouzey2009-11-06
| | | | | | | | | | | | | | | | | | - 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
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
| | | | | | | | | | | | | | | | | | | 1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsGravatar letouzey2009-09-09
| | | | | | | | | | | | 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
* - Correction bug highlighting "Module" dans CoqideGravatar herbelin2008-05-28
| | | | | | | | | - 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
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | du filtrage. Cela permet de détecter les cas impossibles et de simuler les contraintes d'inversion exprimables sous la forme d'un assignement des arguments du constructeurs (cf le cas de Vtail dans Bvector.v). Si l'on filtre sur t:I u1 .. un, et que chaque ui a la forme vi(wi) avec vi composé uniquement de constructeurs, et que le résultat final est P(w1,...,wn) (qui est éventuellement lui-même une evar) alors on construit le prédicat Q:=fun x1 .. xn y => match x1 .. xn y with | v1(z) .. vn(z) t => P(z) | _ .. _ _ => ?evar-speciale-cas-impossible end qui vérifiera bien que Q u1 .. un = P(w1,..,wp). En raison de limitations de l'unification (on aurait besoin d'eta conversion pour résoudre des problèmes du genre "terme rigide == match x with _ => ?evar end", et besoin d'instanciation par constructeurs pour des cas comme "A(y) = match ?evar with C x => A(x) end"), je n'ai pas réussi à traiter le cas général. Aussi, on adopte une stratégie pragmatique consistant à tester plusieurs prédicats possibles : - si un type final est donné, on essaie d'abord l'algorithme de Matthieu et sinon le nouvel algorithme (permet par exemple de traiter certains cas d'élimination dépendante de Bvector.v), - s'il n'y a pas de type final, on essaie d'abord le nouvel algo et sinon, on essaie avec un prédicat sans dépendance (permet de traiter des cas compliqués comme celui de par cas sur I' dans le fichier Case13.v de la test-suite). Dans la pratique, il y a beaucoup de changement dans le code de compile_case. - Par exemple, la compilation est maintenant toujours appelé avec un prédicat (là où l'on pouvait avoir None, on a maintenant toujours au moins une evar). - En revanche, le membre droit des clauses est maintenant optionnel. Si c'est None, c'est qu'on se trouve dans le cas d'une branche impossible au moment du calcul du prédicat de retour. - Aussi, on renonce aux PrLetIn et PrProd dans l'expression du predicat de retour mais il faut savoir que c'est maintenant la liste des tomatchs qui spécifie le contexte exact dans lequel le prédicat de retour est bien typé. - Et d'autres... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10883 85f007b7-540e-0410-9357-904b9bb8a0f7
* No compatibility notations for andb and co (this restore a correct Print output)Gravatar letouzey2008-04-17
| | | | | | | | | | | | 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
* Prevent the apparition of &&& when printing a (if ... then ... else false)Gravatar letouzey2008-04-17
| | | | | | | | 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
* - notations &&& and ||| equivalent to andb and orb, Gravatar letouzey2008-03-27
| | | | | | | | | | 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
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Major revision of FSetAVL: more Function, including some non-structural onesGravatar letouzey2008-02-09
| | | | | | | | | | | | | 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
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05
| | | | | | | | | | | | | | | | | | | | | | | | 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
* 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
* 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
* Déplacement des opérations sur bool dans l'état initialGravatar herbelin2007-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noms "canoniques" pour certaines des propriétés de xor.Gravatar herbelin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9246 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en forme des theoriesGravatar notin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
| | | | | | | | | | | sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵Gravatar notin2006-04-28
| | | | | | 'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2-3 lemmes en plus pour que les Bvectors soient effectivement utilisablesGravatar letouzey2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 01:38:29 +0000