aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/OrderedType.v
Commit message (Collapse)AuthorAge
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Same global ideas (in particular the use of modules/functors), but: - frequent use of Type Classes inside interfaces/implementation. For instance, no more eq_refl/eq_sym/eq_trans, but Equivalence. A class StrictOrder for lt in OrderedType. Extensive use of Proper and rewrite. - now that rewrite is mature, we write specifications of set operators via iff instead of many separate requirements based on ->. For instance add_spec : In y (add x s) <-> E.eq y x \/ In x s. Old-style specs are available in the functor Facts. - compare is now a pure function (t -> t -> comparison) instead of returning a dependent type Compare. - The "Raw" functors (the ones dealing with e.g. list with no sortedness proofs yet, but morally sorted when operating on them) are given proper interfaces and a generic functor allows to obtain a regular set implementation out of a "raw" one. The last two points allow to manipulate set objects that are completely free of proof-parts if one wants to. Later proofs will rely on type-classes instance search mechanism. No need to emphasis the fact that this new version is severely incompatible with the earlier one. I've no precise ideas yet on how allowing an easy transition (functors ?). For the moment, these new Sets are placed alongside the old ones, in directory MSets (M for Modular, to constrast with forthcoming CSets, see below). A few files exist currently in version foo.v and foo2.v, I'll try to merge them without breaking things. Old FSets will probably move to a contrib later. Still to be done: - adapt FMap in the same way - integrate misc stuff like multisets or the map function - CSets, i.e. Sets based on Type Classes : Integration of code contributed by S. Lescuyer is on the way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 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
* Better compatibility after commit 11693 by adding an alias ↵Gravatar letouzey2008-12-17
| | | | | | OrderedTypeFacts.eq_dec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11694 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSet/OrderedType now includes an eq_dec, and hence become an extension of ↵Gravatar letouzey2008-12-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | DecidableType After lots of hesitations, OrderedType now requires this "eq_dec" field, which is redundant (can be deduced from "compare"), but allows the subtyping relation DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly extensions of weak sets. Of course this change introduces a last-minute incompatibility, but: - There is a clear gain in term of functionnality / simplicity. - FSets 8.2 already needs some adaptations when compared with 8.1, so it's the right time to push such incompatible changes. - Transition shouldn't be too hard: the old OrderedType still exists under the name MiniOrderedType, and functor MOT_to_OT allows to convert from one to the other. Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType (resp. OrderedType), an eq_dec on sets is now required in these interfaces and in the implementations. In pratice, it is really easy to build from equal and equal_1 and equal_2. Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun, while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M). Idem with WDecide, WProperties and WEqProperties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11693 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
* * A few Parameter Inline, but they dont seem to help much concerning Gravatar letouzey2007-11-24
| | | | | | | | | | the "alias invasion" problem * A quicker way to build a DecidableType: see MiniDecidableType * pairs of DecidableType seen as DecidableType git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10335 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revision of the FSetWeak Interface, so that it becomes a precise Gravatar letouzey2007-10-29
| | | | | | | | | | | | | | | | | | | | | | | | subtype of the FSet Interface (and idem for FMapWeak / FMap). 1) No eq_dec is officially required in FSetWeakInterface.S.E (EqualityType instead of DecidableType). But of course, implementations still needs this eq_dec. 2) elements_3 differs in FSet and FSetWeak (sort vs. nodup). In FSetWeak we rename it into elements_3w, whereas in FSet we artificially add elements_3w along to the original elements_3. Initial steps toward factorization of FSetFacts and FSetWeakFacts, and so on... Even if it's not required, FSetWeakList provides a eq_dec on sets, allowing weak sets of weak sets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10271 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
* Transparence de eq_dec et lt_dec daans OrderedTypeFactsGravatar notin2007-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9690 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite tentative pour permettre l'utilisation de modules de FSetsGravatar letouzey2006-05-20
| | | | | | | | | avec <: au lieu de : sans surprise de modules genre Raw partout ou autres alias dépliés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8834 85f007b7-540e-0410-9357-904b9bb8a0f7
* meilleur nommage pour PairOrderedTypeGravatar letouzey2006-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8772 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / ↵Gravatar letouzey2006-03-28
| | | | | | OrderedType.Lt,Eq,Gt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 85f007b7-540e-0410-9357-904b9bb8a0f7
* propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble ↵Gravatar letouzey2006-03-16
| | | | | | des fichiers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8639 85f007b7-540e-0410-9357-904b9bb8a0f7
* renommage NoRedun vers le plus joli NoDupGravatar letouzey2006-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8635 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation de FSet (back to 8628)Gravatar notin2006-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8631 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation des $Gravatar letouzey2006-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8629 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de theories/FSets contenant la partie "light" de FSets et FMap:Gravatar letouzey2006-03-15
pas d'implementations par AVL, mais celles par lists, ainsi que les foncteurs de proprietes. Au passage, ajout de MoreList (complements de List) et SetoidList (quelques relations sur des listes considerees modulo un eq ou lt non standard. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8628 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:41:47 +0000