aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
Commit message (Collapse)AuthorAge
...
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
| | | | | | | | | | | In interfaces fields like compare_spec, a CompSpec is prefered to get nice extraction, but then no "destruct (compare_spec .. ..)" is possible in a Type context. Now you can say there "destruct (CompSpec2Type (compare_spec ... ...))" This translate to the Type variant, and make the analysis on it (which is equivalent to analysing the comparison directly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12753 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
* NBinary improved, contains more, subsumes NOrderedTypeGravatar letouzey2010-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12715 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeGravatar letouzey2010-02-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12714 85f007b7-540e-0410-9357-904b9bb8a0f7
* BigN, BigZ, BigQ: presentation via unique module with both ops and propsGravatar letouzey2010-01-17
| | | | | | | | | | | | | | | | | | | | | We use the <+ operation to regroup all known facts about BigN (resp BigZ, ...) in a unique module. This uses also the new ! feature for controling inlining. By the way, we also make sure that these new BigN and BigZ modules implements OrderedTypeFull and TotalOrder, and also contains facts about min and max (cf. GenericMinMax). Side effects: - In NSig and ZSig, specification of compare and eq_bool is now done with respect to Zcompare and Zeq_bool, as for other ops. The order <= and < are also defined via Zle and Zlt, instead of using compare. Min and max are axiomatized instead of being macros. - Some proofs rework in QMake - QOrderedType and Qminmax were in fact not compiled by make world Still todo: OrderedType + MinMax for BigQ, etc etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12680 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification of OrdersTac thanks to the functor application ! with no inlineGravatar letouzey2010-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Try to avoid re-declaring Equivalence, especially for Logic.eqGravatar letouzey2010-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12662 85f007b7-540e-0410-9357-904b9bb8a0f7
* GenericMinMax: still a min_case_strong with hypothesis in the wrong orderGravatar letouzey2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12661 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
| | | | | | | Old stuff DecidableType.v and OrderedType.v stay there and keep their names for the moment, for compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12641 85f007b7-540e-0410-9357-904b9bb8a0f7
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
| | | | | | | | Syntax Include Type is still active, but deprecated, and triggers a warning. The syntax M <+ M' <+ M'', which performs internally an Include, also benefits from this: M, M', M'' can be independantly modules or module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: separation of funs, notations, axioms. Notations via module, ↵Gravatar letouzey2010-01-07
| | | | | | without scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rework of GenericMinMax: new axiomatic, split logical/decidable parts, ↵Gravatar letouzey2010-01-07
| | | | | | | | | | Leibniz part Moreover, instantiation like MinMax are now made without redefining generic properties (easier maintenance). We start using inner modules for qualifying (e.g. Z.max_comm). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12638 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderTac: use TotalOrder, no more "change" before calling "order" (stuff ↵Gravatar letouzey2010-01-07
| | | | | | with Inline) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12636 85f007b7-540e-0410-9357-904b9bb8a0f7
* DecidableType2+OrderedType2 : notations in specific Module Type, slicing of ↵Gravatar letouzey2010-01-07
| | | | | | | | | | | | | | | | OrderedType2 OrderedType2 is reorganized in atomic module type following the same approach used for DecidableType2. We use the following convention: module type Foo' is exactly module type Foo, except that some notations may have been added. In functor arg, we can use Foo or Foo' depending on whether we want nice notation or not. Note that any implementation of Foo is accepted as implementation of Foo' :-). For the moment, these notations are not placed in specific scopes, I think it isn't useful, but I may be wrong, we'll see later when using them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12635 85f007b7-540e-0410-9357-904b9bb8a0f7
* misc improvements in some Structures filesGravatar letouzey2010-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12634 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid declaring hints about refl/sym/trans of eq in DecidableType2Gravatar letouzey2010-01-05
| | | | | | | | This used to be convenient in FSets, but since we now try to integrate DecidableType and OrderedType as foundation for other part of the stdlib, this should be avoided, otherwise some eauto take a _long_ time. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
| | | | | | | | | NB: the grammar entry is placed in vernac:command on purpose even if it should have gone into vernac:gallina_ext. Camlp4 isn't factorising rules starting by "Declare" in a correct way otherwise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
* RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndGravatar letouzey2009-12-18
| | | | | | | As a consequence, revert to some pedestrian proofs of Equivalence here and there, without the need for the Measure class. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverse order of arguments in min_case_strong for better uniformity (and ↵Gravatar letouzey2009-12-17
| | | | | | compatibility...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12595 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
* No more specific syntax "Include Self" for inclusion of partially-applied ↵Gravatar letouzey2009-12-07
| | | | | | | | | | | | | | | | | | | functors For Module F(X:SIG), making now a Include F will try to find the X fields in the current context, just as was doing earlier Include Self F. This specific syntax is removed, freeing the keyword "Self". Anyway, with the use of the syntax "<+" there was already hardly any need for syntax "Include Self". Idem for Include Type. Beware that a typo such as "Include F" instead of "Include F G" will produce a different message now, about a missing field instead of a not-enough-applied functor. By the way, some code clean-up and factorisation of inner recursive functions in declaremods.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
| | | | | | | | | | | Improve generalization by equalities tactic, now allowing to generalize an arbitrary application, e.g. in preparation for applying an elimination principle for a function. This adds a flag to generalize_dep so that it doesn't abstract the variable if it is defined, just introducing a let-in. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12541 85f007b7-540e-0410-9357-904b9bb8a0f7
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
| | | | | | | | | | Any place where <: was legal can now contain many <: declarations. Moreover we can say that the module type we are declaring is a subtype of an earlier module type. See DecidableType2 for examples. Also try to handle correctly the freeze/unfreeze summaries when simulating start/include/end (syntax ... := ... <+ ...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12532 85f007b7-540e-0410-9357-904b9bb8a0f7
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
| | | | | | | | | | | | | | | | | | | | "Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for "Module M (...). Include M1. Include M2. Include M3... End M." Moreover M2,M3,etc can be functors as long as they find what they need in what comes before them (see new command "Include Self"). The only real constraint is that M1,M2,M3,... should not have common elements (for the moment (?)). Same behavior for signature : Module Type M := M1 <+ M2 <+ M3. Note that this <+ is _not_ a primitive construct of the module language, for instance it cannot be used in signature (Module M <: M1 <+ M2 is illegal for the moment). Some example of use in Decidable2 and NZAxioms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7
* Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsGravatar letouzey2009-11-16
| | | | | | | We can now have a diamond-like approch to extentions of signatures, instead of a linear-only chains as earlier... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12529 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification of Numbers, mainly thanks to IncludeGravatar letouzey2009-11-10
| | | | | | | | | | | | | | | | | - No more nesting of Module and Module Type, we rather use Include. - Instead of in-name-qualification like NZeq, we use uniform short names + modular qualification like N.eq when necessary. - Many simplification of proofs, by some autorewrite for instance - In NZOrder, we instantiate an "order" tactic. - Some requirements in NZAxioms were superfluous: compatibility of le, min and max could be derived from the rest. - NMul removed, since it was containing only an ad-hoc result for ZNatPairs, that we've inlined in the proof of mul_wd there. - Zdomain removed (was already not compiled), idea of a module with eq and eqb reused in DecidableType.BooleanEqualityType. - ZBinDefs don't contain any definition now, migrate it to ZBinary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12489 85f007b7-540e-0410-9357-904b9bb8a0f7
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
| | | | | | + adaptation of {Nat,N,P,Z,Q,R}_as_DT for them to provide both eq_dec and eqb git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12462 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
* List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, ↵Gravatar letouzey2009-11-02
| | | | | | ForallPairs, etc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12459 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
| | | | | | | | | | | | | variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
| | | | | | | | | | | | Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSetCompat: a compatibility wrapper between FSets and MSetsGravatar letouzey2009-10-20
| | | | | | | | | | | | Thanks to the functors in FSetCompat, the three implementations of FSets (FSetWeakList, FSetList, FSetAVL) are just made of a few lines adapting the corresponding MSets implementation to the old interface. This approach breaks FSetFullAVL. Since this file is of little use for stdlib users, we migrate it into contrib Orsay/FSets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge SetoidList2 into SetoidList: forgotten reference to the removed fileGravatar letouzey2009-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
| | | | | | | | | This file contains low-level stuff for FSets/FMaps. Switching it to the new version (the one using Equivalence and so on instead of eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in FSets/FMaps that are minor and probably invisible to standard users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12400 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedType2 : trivial lemmas are turned into tests for order.Gravatar letouzey2009-10-16
| | | | | | | In particular we remove them from the hint db, a few autos become calls to order. Moreover, lt_antirefl --> lt_irrefl for uniformity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12398 85f007b7-540e-0410-9357-904b9bb8a0f7
* Structure/OrderTac.v : highlight the "order" tactic by isolating it from ↵Gravatar letouzey2009-10-16
| | | | | | | | | | | | | | FSets, and improve it As soon as you have a eq, a lt and a le (that may be lt\/eq, or (complement (flip (lt))) and a few basic properties over them, you can instantiate functor MakeOrderTac and gain an "order" tactic. See comments in the file for the scope of this tactic. NB: order doesn't call auto anymore. It only searches for a contradiction in the current set of (in)equalities (after the goal was optionally turned into hyp by double negation). Thanks to S. Lescuyer for his suggestions about this tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12397 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedType2.order : fix the last fix (a fail at the wrong place)Gravatar letouzey2009-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12391 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in last commitGravatar letouzey2009-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved tactic "order" in OrderedTypeGravatar letouzey2009-10-14
| | | | | | | | | | | | | | | | | | | I forgot to mention in last commit message about MSets that the corresponding OrderedType2 comes with a redesigned "order" tactic. It should now be complete for its purpose (that is solve systems of (in)equations of variables over == < <= <>). Non-linear matching is cool, I love Ltac :-). Unlike the old "order", this new version is meant to completely solve the goal or fail. Speed might be an issue for big systems, but in pratice it is quite efficient on the examples encountered in FSets. This commit: - propagages this new "order" to the original OrderedType.v file used for the old FSet. - fixes a bug : the ltac loop shouldn't fail otherwise strange backtrack occurs. I hate Ltac :-( git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12388 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 08:51:14 +0000