aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2010-01-07Include can accept both Module and Module Typeletouzey
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
2010-01-07Numbers: separation of funs, notations, axioms. Notations via module, ↵letouzey
without scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12639 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07Rework of GenericMinMax: new axiomatic, split logical/decidable parts, ↵letouzey
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
2010-01-07MSetInterface: more modularityletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12637 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07OrderTac: use TotalOrder, no more "change" before calling "order" (stuff ↵letouzey
with Inline) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12636 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07DecidableType2+OrderedType2 : notations in specific Module Type, slicing of ↵letouzey
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
2010-01-07misc improvements in some Structures filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12634 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-07MSetAVL: hints made local since some of them are quite violent (transitivity)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12633 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-06Patch on subtyping check of opaque constants.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12631 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-06"by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ↵letouzey
by ...") Application in some proofs of Numbers's abstract division git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12630 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-05Numbers abstract layer: more Module Type, used especially for divisions.letouzey
Properties are now rather passed as functor arg instead of via Include or some inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12629 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-05Zdiv seen as a quasi-instantation of generic ZDivFloor from theories/Numbersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12627 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-05Avoid declaring hints about refl/sym/trans of eq in DecidableType2letouzey
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
2010-01-05Division in Numbers: proofs with less auto (less sensitive to hints, in ↵letouzey
particular about eq) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12625 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-05Division in Numbers: factorisation of signaturesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12624 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
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
2009-12-19Backtrack on making exact hints for lemmas starting with productsmsozeau
(e.g. transitivity lemmas) and fix bug #2207, avoiding the generation of useless eta-redexes during type class instance resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12600 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-18RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndletouzey
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
2009-12-17ZOdiv: fully use generic properties from ZDivTrunc.vletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12596 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-17Reverse order of arguments in min_case_strong for better uniformity (and ↵letouzey
compatibility...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12595 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-17Division in Numbers : more properties, new filenames based on a paper by R. ↵letouzey
Boute Following R. Boute (paper "the Euclidean Definition of the Functions div and mod"): - ZDivFloor.v for Coq historical division (former ZDivCoq.v) - ZDivTrunc.v for Ocaml convention (former ZDivOcaml.v) - ZDivEucl.v for "Mathematical" convention 0<=r (former ZDivMath.v) These property functors are more or less finished (except that sign and abs stuff should be migrated to a separate file). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12594 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-16Division in Numbers: more properties proved (still W.I.P.)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12591 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-15A generic euclidean division in Numbers (Still Work-In-Progress)letouzey
- For Z, we propose 3 conventions for the sign of the remainder... - Instanciation for nat in NPeano. - Beginning of instanciation in ZOdiv. Still many proofs to finish, etc, etc, but soon we will have a decent properties database for all divisions of all instances of Numbers (e.g. BigZ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12590 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-13Addition of mergesort + cleaning of the Sorting libraryherbelin
- New (modular) mergesort purely using structural recursion - Move of the (complex) notion of permutation up to setoid equality formerly defined in Permutation.v to file PermutSetoid.v - Re-use of the file Permutation.v for making the canonical notion of permutation that was in List.v more visible - New file Sorted.v that contains two definitions of sorted: "Sorted" is a renaming of "sort" that was defined in file Sorting.v and "StronglySorted" is the intuitive notion of sorted (there is also LocallySorted which is a variant of Sorted) - File Sorting.v is replaced by a call to the main Require of the directory - The merge function whose specification rely on counting elements is moved to Heap.v and both are stamped deprecated (the sort defined in Heap.v has complexity n^2 in worst case) - Added some new naming conventions - Removed uselessly-maximal implicit arguments of Forall2 predicate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12585 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-10NZDomain: investigation of the shape of NZ domain, more results about ↵letouzey
ofnat:nat->NZ.t git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12575 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵letouzey
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
2009-12-08Fix the build of coq via ocamlbuildletouzey
- no more plugins/interface - a few missing files in theories.itarget - a few things required Unix now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12572 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-08integrate MSetToFiniteSet into the compilation (and fix it)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12571 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-07No more specific syntax "Include Self" for inclusion of partially-applied ↵letouzey
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
2009-12-06Forgot a file in last commit.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12563 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-06Fix anomaly when using typeclass resolution with filtered hyps in evars.msozeau
Make setoid_rewrite-through-rewrite's selection of occurences more robust: do not try unification with reduction if not needed. This changes a few scripts that were using reduction in a far from obvious way and could break more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12562 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-03Rename proper to proper_prf to avoid clash with CoRN, msozeau
it's rarely used anyway. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12557 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-01Fix make_exact_entry to allow applying [forall x, P x] hints directly,msozeau
avoiding the introduction of eta-redexes. Prioritize hints over intros in typeclass resolution to profit from that. Add a minor fix in coqdoc by F. Garillot. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-30Fix backtracking heuristic in typeclass resolution. msozeau
Now that backtracking is working correctly, we need to avoid a non-termination issue introduced by the [RelCompFun] definition in RelationPairs, by adding a [Measure] typeclass. It could be used to have a uniform notation for measures/interpretations in Numbers and be but in the interfaces too, only the mimimal change was implemented. Fix syntax change in test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12547 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-27Added support for definition of fixpoints using tactics.herbelin
Fixed some bugs in -beautify and robustness of {struct} clause. Note: I tried to make the Automatic Introduction mode on by default for version >= 8.3 but it is to complicated to adapt even in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-24Minor fixes in typeclasses, avoiding repeated evar normalizations.msozeau
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
2009-11-24Small extra result on JMeq vs eq_dep.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12540 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Diamond-shape instead of linear hiearchy in Numbers/NatIntletouzey
NZBase -- NZAdd -- NZMul | | NZOrder ---------- NZAddOrder -- NZMulOrder -- NZProperties This is done by transforming NZBase into a functorial module type, and making NZAdd NZMul NZOrder accept an instance of NZBase as parameter. This is possible thanks to a combination of various new features of modules: - interactive proofs in module type (ie functors can be turned into type functors) - Include Type in Module (ie type functors can be turned into functors) - Include Self, <+ , etc, etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12534 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-18Module subtyping : allow many <: and module type declaration with <:letouzey
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
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
"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
2009-11-16Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsletouzey
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
2009-11-16Some lemmas about dependent choice + extensions of Compare_dec +herbelin
synonyms in Le.v, Lt.v, Gt.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12527 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-15Document Generalizable Variables, and change syntax to msozeau
[Generalizable (All|No) Variables (ident+)?], also update type classes documentation to reflect the latest changes in instance decls. Fix a bug in [Util.list_split_when]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12525 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-15Fix [Instance: forall ..., C args := t] declarations to behave asmsozeau
expected, not introducing the [forall ...] variables to avoid unnecessary eta-expansions. Force to use { } in instance declarations when the class is a record even if it's a singleton. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12524 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)letouzey
- In fact, Bind Scope has no retrospective effect. Since we don't want it inside functor, we use it late, and hence we are forced to use manual "Arguments Scope" commands. - Added syntax for power in BigN / BigZ / BigQ. - Added syntax p#q in BigQ for representing fractions (constructor BigQ.Qq) as in QArith. Display of a rational numeral is hence either an integer (constructor BigQ.Qz) or something like 6756 # 8798. - Fix of function BigQ.Qred that was not simplifing (67#1) into 67. - More tests in test-suite/output/NumbersSyntax.v A nice one not in the test-suite: Time Eval vm_compute in BigQ.red ((2/3)^(-100000) * (2/3)^(100000)). = 1 : bigQ Finished transaction in 3. secs (3.284206u,0.004s) :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12507 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-12Repair interpretation of numeral for BigQ, add a printer (close #2160)letouzey
on the way: - Added a testsuite output file - Try to avoid nasty unfolding (fix nfun ...) in type of I31. Idealy we would need a "Eval compute in" for the type of a inductive constructor - Stop opening Scopes for BigQ, BigN, BigZ by default The user should do some Open Scope. TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope (and so on for other operations), even with some Bind Scope around. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12504 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Better compatibility for Peqbletouzey
As show by contrib TreeAutomata, the Peqb now placed in BinPos was using 1st arg as "struct", instead of 2nd arg as earlier. Fix that, and remove the "Import BinPos BinNat" hack in Ndec (merci Hugo :-). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12503 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
- Deactivation of short names registration and printing for abbreviations to identical names, what avoids printing uselessly qualified names binding where the short name is in fact equivalent. - New treatment of abbreviations to names: don't insert any maximally inserted implicit arguments at all at the time of the abbreviation and use the regular internalization strategy to have them inserted at use time. - The previous modifications altogether make redirections of qualified names easier and avoid the semantic change of r12349 and hence allows to keep "Notation b := @a" as it was before, i.e. as a notation for the deactivation of the implicit arguments of a. - Took benefit of these changes and updated nil/cons/list/app redefinition in "List.v". - Fixed parsing/printing notation bugs (loop on partially applied abreviations for constructors in constrintern.ml + bad reverting of notations with holes that captured non anonymous variables in match_cases_pattern). - Add support for parsing/printing abbreviations to @-like constructors and for reverting printing for abbreviations to constructors applied to parameters only (function extern_symbol_pattern). - Minor error messages fixes and minor APIs cleaning. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMaxletouzey
To retrieve the old behavior of spec_sub0 and spec_sub with precondition on order, just chain spec_sub with Zmax_r or Zmax_l. Idem with spec_pred0 and spec_pred. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12490 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-10Simplification of Numbers, mainly thanks to Includeletouzey
- 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-17 11:35:58 +0000