aboutsummaryrefslogtreecommitdiff
path: root/theories/FSets
AgeCommit message (Collapse)Author
2008-03-15Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)letouzey
* FSetAVL is greatly lightened : modulo a minor change in bal, formal proofs of avl invariant is not needed for building a functor implementing FSetInterface.S (even if this invariant is still true) * Non-structural functions (union, subset, compare, equal) are transformed into efficient structural versions * Both proofs of avl preservation and non-structural functions are moved to a new file FSetFullAVL, that can be ignored by the average user. Same for FMapAVL (still work in progress...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10679 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-07f_equal, revert, specialize in ML, contradict in better Ltac (+doc)letouzey
* "f_equal" is now a tactic in ML (placed alongside congruence since it uses it). Normally, it should be completely compatible with the former Ltac version, except that it doesn't suffer anymore from the "up to 5 args" earlier limitation. * "revert" also becomes an ML tactic. This doesn't bring any real improvement, just some more uniformity with clear and generalize. * The experimental "narrow" tactic is removed from Tactics.v, and replaced by an evolution of the old & undocumented "specialize" ML tactic: - when specialize is called on an hyp H, the specialization is now done in place on H. For instance "specialize (H t u v)" removes the three leading forall of H and intantiates them by t u and v. - otherwise specialize still works as before (i.e. as a kind of generalize). See the RefMan and test-suite/accept/specialize.v for more infos. Btw, specialize can still accept an optional number for specifying how many premises to instantiate. This number should normally be useless now (some autodetection mecanism added). Hence this feature is left undocumented. For the happy few still using specialize in the old manner, beware of the slight incompatibities... * finally, "contradict" is left as Ltac in Tactics.v, but it has now a better shape (accepts unfolded nots and/or things in Type), and also some documentation in the RefMan git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10637 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-07repair FSets/FMap after the change in setoid rewriteletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10636 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-06Plug the new setoid implemtation in, leaving the original one commentedmsozeau
out. The semantics of the old setoid are faithfully simulated by the new tactic, hence no scripts involving rewrite are modified. However, parametric morphism declarations need to be changed, but there are only a few in the standard library, notably in FSets. The declaration and the introduction of variables in the script need to be tweaked a bit, otherwise the proofs remain unchanged. Some fragile scripts not introducting their variable names explicitely were broken. Requiring Setoid requires Program.Basics which sets stronger implicit arguments on some constants, a few scripts benefit from that. Ring/field have been ported but do not really use the new typeclass architecture as well as they could. Performance should be mostly unchanged, but will certainly improve in the near future. Size of the vo's seems not to have changed at all. It will certainly break some contribs using Setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10631 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-03-02A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)letouzey
... but still no idea why it was working fine on some machines even without this patch... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10614 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Some suggestions about FMap by P. Casteran: letouzey
- clarifications about Equality on maps Caveat: name change, what used to be Equal is now Equivb - the prefered equality predicate (the new Equal) is declared a setoid equality, along with several morphisms - beginning of a filter/for_all/exists_/partition section in FMapFacts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10608 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28cardinal is promoted to the rank of primitive member of the FMap interfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10605 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Nicer third spec of choose. letouzey
The old version is now a properties in FSetProperties.OrdProperties git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10601 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27For more uniformity, use implicits in FSetAVLletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10600 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-10Major revision: use of Function, including some non-structural onesletouzey
Sequel of commit 10545 on FSetAVL. This time, no compile-time penality since there are fewer non-structural functions in FMapAVL. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10546 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
2008-02-08misc improvementsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10539 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08better comments in FMapInterfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10536 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08better comments in FSetInterfaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10535 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08more complete FSets.vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10528 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-05kill some useless module aliases E:=X (for better name printing, see Elie's ↵letouzey
14097) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10511 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-04Reorganization of FSet+FMap : no more files specific to Weak Sets/Mapsletouzey
Thanks to Elie's work and especially "Include Type ...", full sets can be simply expressed as extensions of weak sets. Moreover, Facts and Properties functors can be factorized almost completely. As a result, things like FSetWeakAAA.BBB can now be found as FSetAAA.WBBB, Same with maps / weak maps ... No backward compatibility intended for weak sets / maps, but porting scripts should mostly amounts to name changes (see above). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10505 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-02factorization part II (Properties + EqProperties), inclusion of FSetDecide ↵letouzey
(from A. Bohannon) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10500 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-01Thanks to Elie, we can share duplicated stuff in FSets: for a start, ↵letouzey
FSetWeakFacts and FSetFacts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10498 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-04more user-friendly versions of some properties lemmas in FSets/FMapletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10420 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-11-24* A few Parameter Inline, but they dont seem to help much concerning letouzey
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
2007-11-06small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is letouzey
more general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10295 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-30temporary workaround for bug #1738letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10278 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-30A useless Add Morphism: since Subset is a Setoid Relation, it is alsoletouzey
automatically a Morphism about itself (avoid a warning about redeclared Setoids). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10277 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-29Revision of the FSetWeak Interface, so that it becomes a precise letouzey
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
2007-10-21Cleanup attempt of Hints in *Interface.v files.letouzey
See recent discussion in coq-club. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10243 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
------------------------------------------------ See file PreOmega for more details and/or test-suite/succes/*Omega*.v The zify tactic performs a Z-ification of your current goal, transforming parts of type nat, N, positive, taking advantage of many equivalences of operations, and of the positivity implied by these types. Integration with omega and romega: (r)omega : the earlier tactics, 100% compatible (r)omega with * : full zify applied before the (r)omega run (r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z}, applies only specific parts of zify (btw "with Z" means take advantage of Zmax, Zmin, Zabs and Zsgn). As a particular consequence, "romega with nat" should now be a close-to-perfect replacement for omega. Slightly more powerful, since (forall x:nat, x*x>=0) is provable and also slightly less powerful: if False is somewhere in the hypothesis, it doesn't use it. For the moment zify is done in a direct way in Ltac, using rewrite when necessary, but crucial chains of rewrite may be made reflexive some day. Even though zify is designed to help (r)omega, I think it might be of interest for other tactics (micromega ?). Feel free to complete zify if your favorite operation / type isn't handled yet. Side-effects: - additional results for ZArith, NArith, etc... - definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope - romega now start by doing "intros". Since the conclusion will be negated, and this operation will be justified by means of decidability, it helps to have as little as possible in the conclusion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-13Deletion of some firstorder calls in FSetAVL: letouzey
after commit 9983 of Bruno concerning kernel/closure.ml, a few firstorder were awfully slow. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9994 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-27- Extensions of FMap(Weak)Facts: letouzey
fold properties and induction principles for (weak) maps. - Simplification in SetoidList: the two important results fold_right_equivlistA and fold_right_add are now proved without using removeA and hence do not depend anymore on a decidable equality (good for maps and their arbitrary datas). In fact, removeA is not used at all anymore, but I leave it here (mostly), since it can't hurt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9914 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-26additional properties for FMap (and slight rework of SetoidList and ↵letouzey
FSetProperties) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9908 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-14Rework of FSetProperties, in order to add more easily a Properties functor letouzey
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
2007-06-11undeletion of E_ST and Equal_ST: these records aren't mandatory, but quite ↵letouzey
useful git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9887 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-08some more properties of fold and elements in FSetPropertiesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9885 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07Extension of NArith: Nminus, Nmin, etcletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-07* For uniformity, FSetAVL uses Implicit Arguments (a bit)letouzey
* Some additionnal properties: - two more induction principles on sets - some results about union, filter, etc - Subset is declared to be a Setoid Relation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9882 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-28comparison functions should be Defined not Qedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9867 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-27As suggested by Pierre Casteran, fold for FSets/FMaps now takes a letouzey
(A:Type) instead of a (A:Set). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9863 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-25fix for bug #1347 (no more Scope pollution by FSets)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9861 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-26PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ↵letouzey
OrderedType git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9730 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-08Transparence de eq_dec et lt_dec daans OrderedTypeFactsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9690 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-28FSetInterface: new item choose_equal in the spec S (request of P. Casteran)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9684 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-25oups, ne chargeait pas les bons fichiersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9278 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-21incomplete and temporary fix for PR#1222: revert accepts up to 10 argsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9156 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-14comparison functions should be Defined not Qedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9066 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-09Argument Scope de list déplacé dans List.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9035 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Passage des graphes de Function dans Type jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Déplacement Int.v dans ZArith, déplacement de DecidableType.v et ↵herbelin
DecidableTypeEx.v dans Logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8933 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-06+ ameliorating the tactic "functional induction"jforest
+ bug correction in proof of structural principles + up do to date test-suite/success/Funind.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8899 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-12 18:18:35 +0000