aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Max.v
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
|
* 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
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - The earlier proof-of-concept file NPeano (which instantiates the "Numbers" framework for nat) becomes now the entry point in the Arith lib, and gets renamed PeanoNat. It still provides an inner module "Nat" which sums up everything about type nat (functions, predicates and properties of them). This inner module Nat is usable as soon as you Require Import Arith, or just Arith_base, or simply PeanoNat. - Definitions of operations over type nat are now grouped in a new file Init/Nat.v. This file is meant to be used without "Import", hence providing for instance Nat.add or Nat.sqrt as soon as coqtop starts (but no proofs about them). - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult) are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul where here Nat is Init/Nat.v). - This Coq.Init.Nat module (with only pure definitions) is Include'd in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat sometimes instead of just Nat (for instance when doing "Print plus"). Normally it should be ok to just ignore these "Init" since Init.Nat is included in the full PeanoNat.Nat. I'm investigating if it's possible to get rid of these "Init" prefixes. - Concerning predicates, orders le and lt are still defined in Init/Peano.v, with their notations "<=" and "<". Properties in PeanoNat.Nat directly refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le", we cannot yet include an Inductive to implement a Parameter), but these aliased predicates won't probably be very convenient to use. - Technical remark: I've split the previous property functor NProp in two parts (NBasicProp and NExtraProp), it helps a lot for building PeanoNat.Nat incrementally. Roughly speaking, we have the following schema: Module Nat. Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *) ... (** proofs of specifications for basic ops such as + * - *) Include NBasicProp. (** generic properties of these basic ops *) ... (** proofs of specifications for advanced ops (pow sqrt log2...) that may rely on proofs for + * - *) Include NExtraProp. (** all remaining properties *) End Nat. - All other files in directory Arith are now taking advantage of PeanoNat : they are now filled with compatibility notations (when earlier lemmas have exact counterpart in the Nat module) or lemmas with one-line proofs based on the Nat module. All hints for database "arith" remain declared in these old-style file (such as Plus.v, Lt.v, etc). All the old-style files are still Require'd (or not) by Arith.v, just as before. - Compatibility should be almost complete. For instance in the stdlib, the only adaptations were due to .ml code referring to some Coq constant name such as Coq.Init.Peano.pred, which doesn't live well with the new compatibility notations.
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solve name conflict about pow introduced by commit 13546.Gravatar letouzey2010-10-21
| | | | | | | - NPeano isn't Exported by default anymore (contains pow for nat). - in coq_micromega.ml, we specify more where to find the pow of R. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13569 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
* 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
* Arith's min and max placed in Peano (+basic specs max_l and co)Gravatar letouzey2010-02-17
| | | | | | | This allow for instance to remove the dependency of List.v toward Min.v To prove max_l and co, we push Le.le_pred and Le.le_S_n into Peano. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Min, Max: for avoiding inelegant NPeano.max printing, we Export this libGravatar letouzey2010-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: properties of min/max with respect to 0,S,P,add,sub,mulGravatar letouzey2010-02-09
| | | | | | | | | With these properties, we can kill Arith/MinMax, NArith/Nminmax, and leave ZArith/Zminmax as a compatibility file only. Now the instanciations NPeano.Nat, NBinary.N, ZBinary.Z, BigZ, BigN contains all theses facts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12718 85f007b7-540e-0410-9357-904b9bb8a0f7
* NPeano improved, subsumes NatOrderedTypeGravatar letouzey2010-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12717 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
| | | | | | | | | | | | | | | | | | | | | | | | - A richer OrderedTypeFull interface : OrderedType + predicate "le" - Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics - By the way: as suggested by S. Lescuyer, specification of compare is now inductive - GenericMinMax: axiomatisation + properties of min and max out of OrderedTypeFull structures. - MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax, with also some domain-specific results, and compatibility layer with already existing results. - Some ML code of plugins had to be adapted, otherwise wrong "eq", "lt" or simimlar constants were found by functions like coq_constant. - Beware of the aliasing problems: for instance eq:=@eq t instead of eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t instead of Z in statement of Zmax_spec). - Some Morphism declaration are now ambiguous: switch to new syntax anyway. - Misc adaptations of FSets/MSets - Classes/RelationPairs.v: from two relations over A and B, we inspect relations over A*B and their properties in terms of classes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12461 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
* A few additions in Min.v.Gravatar herbelin2009-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12368 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
* Some additions in Max and Zmax. Unifiying list of statements and namesGravatar herbelin2009-04-14
| | | | | | | | in both files. Late update of CHANGES wrt classical Tauto. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12084 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed bug #2021 (uncaught exception with injection/discriminate whenGravatar herbelin2009-01-01
| | | | | | | | | | | | the inductive status of a projectable position comes from a dependency). - Improved doc of the stdlib chapter (see bug #2018), and fixed tex bugs introduced in r11725. - Applied wish #2012 (max_dec transparent). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension of NArith: Nminus, Nmin, etcGravatar letouzey2007-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajouts de lemmes dans Min et MaxGravatar notin2007-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9660 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
* 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
* Unification max_case et max_case2Gravatar herbelin2006-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵Gravatar herbelin2003-11-29
| | | | | | par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit Variables TypeGravatar herbelin2003-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3809 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commentaire coqweb non ferméGravatar herbelin2001-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2370 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un fichier Max dans Arith, et enrichissement du Min.Gravatar letouzey2001-11-15
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2195 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 05:02:22 +0000