aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Numbers : also axiomatize constants 1 and 2.Gravatar letouzey2010-10-14
| | | | | | | | | | | | | | | | | Initially, I was using notation 1 := (S 0) and so on. But then, when implementing by NArith or ZArith, some lemmas statements were filled with Nsucc's and Zsucc's instead of 1 and 2's. Concerning BigN, things are rather complicated: zero, one, two aren't inlined during the functor application creating BigN. This is deliberate, at least for the other operations like BigN.add. And anyway, since zero, one, two are defined too early in NMake, we don't have 0%bigN in the body of BigN.zero but something complex that reduce to 0%bigN, same for one and two. Fortunately, apply or rewrite of generic lemmas seem to work, even if there's BigZ.zero on one side and 0 on the other... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13555 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: new functions pow, even, odd + many reorganisationsGravatar letouzey2010-10-14
| | | | | | | | | | | | | | | | | | | | | | | | - Simplification of functor names, e.g. ZFooProp instead of ZFooPropFunct - The axiomatisations of the different fonctions are now in {N,Z}Axioms.v apart for Z division (three separate flavours in there own files). Content of {N,Z}AxiomsSig is extended, old version is {N,Z}AxiomsMiniSig. - In NAxioms, the recursion field isn't that useful, since we axiomatize other functions and not define them (apart in the toy NDefOps.v). We leave recursion there, but in a separate NAxiomsFullSig. - On Z, the pow function is specified to behave as Zpower : a^(-1)=0 - In BigN/BigZ, (power:t->N->t) is now pow_N, while pow is t->t->t These pow could be more clever (we convert 2nd arg to N and use pow_N). Default "^" is now (pow:t->t->t). BigN/BigZ ring is adapted accordingly - In BigN, is_even is now even, its spec is changed to use Zeven_bool. We add an odd. In BigZ, we add even and odd. - In ZBinary (implem of ZAxioms by ZArith), we create an efficient Zpow to implement pow. This Zpow should replace the current linear Zpower someday. - In NPeano (implem of NAxioms by Arith), we create pow, even, odd functions, and we modify the div and mod functions for them to be linear, structural, tail-recursive. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Zeven: some complements, e.g. proofs that Zeven_bool and co are okGravatar letouzey2010-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13545 85f007b7-540e-0410-9357-904b9bb8a0f7
* NArith: add some functions Neven and NoddGravatar letouzey2010-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13544 85f007b7-540e-0410-9357-904b9bb8a0f7
* NArith: Definition of a Npow power functionGravatar letouzey2010-10-14
| | | | | | | | | | | | | By the way, adds an Piter_op iterator : Piter_op op p a is "a op a ... op a" with a occurring p times. It could be use to define Pmult_nat and hence nat_of_P (not fully done for maintaining compatibility). Unlike iter_pos, Piter_op is logarithmic in p, not linear. Note: We should adapt someday the brain-damaged Zpower to make it use Piter_op instead of iter_pos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using multiple lists of implicit arguments in Program for preservingGravatar herbelin2010-10-03
| | | | | | | | | | | | | | the compatibility with the rest of the theories. Used multiple lists of implicit arguments in Init only when the maximality status is not modified in Program (and thus the compatibility is strictly preserved). This improves the compatibility for the implicit arguments of eq_refl and JMeq_refl between 8.2 and 8.3 when using Program (up to the residual differences in the maximality status). For the constants Acc_inv, inl, inr, left, right, Vnil, Vcons, the compatibility with 8.2 is not improved but the consistency between Program and the rest of the library is. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes of 'make doc'Gravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13472 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bvector.Vshiftin was wrong for agesGravatar pboutill2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13471 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: re-introduce some eta-expansions in rare situations leading to ↵Gravatar letouzey2010-09-20
| | | | | | | | | | | | | | | | | | | | | '_a types If there's no lambdas at the top of a constant body and its type is functional and this type contains type variable and we're extracting to Ocaml then we perform one eta-expansion to please the ML type-checker This might slow down things, if some computations are shared thanks to the partial application. But it seems quite unlikely to encounter both situations (clever partial application and non-generalizable variable) at the same time. Compcert is ok, for instance. As a consequence, no need for manual eta-expansion in AVL code (and by the way MSetAVL.element wasn't a problem, it is monomorphic) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13441 85f007b7-540e-0410-9357-904b9bb8a0f7
* For the moment, two small manual eta-expansions to avoid '_a after extractionGravatar letouzey2010-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13425 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake : another round of heavy reworkGravatar letouzey2010-09-09
| | | | | | | | | | | | | | | | - generic iterator [iter] factorized in the same way as [same_level] - as a consequence, remaining operations [mul] [compare] [div_gt] are now defined and proved in a short and nice way and moved to NMake.v. - lots of other simplifications / factorisations in NMake_gen. This file is still macro-generated, but is much shorter, and the major part of it is now invariant. - As advised by B. Gregoire, try to (re)create clever partial applications in code of operators, in order to avoid projecting ZnZ fields all the time in base cases. Case 0 can still be improved, but it's already better this way :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [clenv_missing] to compute a better approximation of missingGravatar msozeau2010-08-02
| | | | | | | | | | dependent arguments. It breaks compatibility as some [apply with] clauses are not necessary anymore. Typically when applying [f_equal], the domain type of the function can be infered even if it does not appear directly in the conclusion of the goal. Fixes bug #2154. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed commit r13359 which was incomplete for its "trunk" part. ThanksGravatar herbelin2010-07-31
| | | | | | to Julien for noticing it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rather quick hack to make basic unicode notations available byGravatar herbelin2010-07-29
| | | | | | requiring a file Utf8_core. That needs to be improved... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite Heap merging so that it extracts to an O(n log n) definition.Gravatar msozeau2010-07-28
| | | | | | | Fixes bug #2047. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13345 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes:Gravatar msozeau2010-07-27
| | | | | | | | | - Document and fix [autounfold] - Fix warning about default Firstorder tactic object not being defined - Fix treatment of implicits in Program Lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 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
* Made notations for exists, exists! and notations of Utf8.v recursive notationsGravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backported r13308 (ConstructiveEpsilon.v) to branch v8.3Gravatar herbelin2010-07-22
| | | | | | Also removed trailing spaces of the file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13309 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of ConstructiveEpsilon.v by Jean-François Monin.Gravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetPositive: mention MSetInterface instead of FSetInterfaceGravatar letouzey2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13288 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSetPositive: sets of positive inspired by FMapPositive.Gravatar letouzey2010-07-16
| | | | | | | | | | Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant. I've also included a MSets version, hence FSetPositive might become soon a mere wrapper for MSetPositive, as for other FSets implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bool: shorter and more systematic proofs + an iff lemma about eqbGravatar letouzey2010-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13286 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bool: iff lemmas about or, a reflect inductive, an is_true functionGravatar letouzey2010-07-10
| | | | | | | | | | | For the moment, almost no lemmas about (reflect P b), just the proofs that it is equivalent with an P<->b=true. is_true b is (b=true), and is meant to be added as a coercion if one wants it. In the StdLib, this coercion is not globally activated, but particular files are free to use Local Coercion... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13275 85f007b7-540e-0410-9357-904b9bb8a0f7
* FSets/Msets: some renaming of module params to simplify the task of the ↵Gravatar letouzey2010-07-05
| | | | | | extraction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13239 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sorting library: export as hints only lemmas that obviously simplifyGravatar herbelin2010-07-02
| | | | | | | | | | | | the size of the problem to solve. This is still more powerful than what 8.2 provided since no hints were exported yet when Permutation was in List.v in 8.2. Whether no hints should be exported at all, and whether hints should be exported in a specific database or not is unclear. At least, the contribs apparently supported the extra added power of auto introduced in r12585 (date of the revision of the Sorting library), so let's continue with it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13231 85f007b7-540e-0410-9357-904b9bb8a0f7
* QArith: typo in name of hint db (fix #2346)Gravatar letouzey2010-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13220 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation by replacing some "auto with zarith" with "ring"Gravatar glondu2010-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13212 85f007b7-540e-0410-9357-904b9bb8a0f7
* clear/revert dependent: restrict to hyp(h) instead of ident(h)Gravatar letouzey2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13169 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report fixes from FSetDecide to MSetDecideGravatar letouzey2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13164 85f007b7-540e-0410-9357-904b9bb8a0f7
* fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix ↵Gravatar letouzey2010-06-18
| | | | | | #2281) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13163 85f007b7-540e-0410-9357-904b9bb8a0f7
* fsetdec: clear dependent hypothesis before anything else (fix #2136).Gravatar letouzey2010-06-17
| | | | | | | | | Since the tactic fsetdec is doing lots of "clear" and also "subst" on equalities, things may go wrong in case of dependencies amongst hypothesis. For the moment, we clear all hypothesis that mention other hypothesis of sort Prop. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13162 85f007b7-540e-0410-9357-904b9bb8a0f7
* New tactic "clear dependent", for the moment in ltac in Init/TacticsGravatar letouzey2010-06-17
| | | | | | | | | | | for the moment, only one hypothesis name is accepted after clear dependent (seems to be also the case for generalize dependent). Btw, added an alternative name "revert dependent" for "generalize dependent", since this tactics remove hypothesis from the context. To be documentated later... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13161 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetInterface: no induction principle about a Record (nicer extraction)Gravatar letouzey2010-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13159 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and ↵Gravatar letouzey2010-06-15
| | | | | | tree_case git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13156 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing definition of set_map (bug report #2111) which was actually alreadyGravatar herbelin2010-06-13
| | | | | | incorrect when it was introduced in 1998. Proofs about it remain to be done... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative fix for bug #2226: put inj_pair2 and eq_dep_eq hints in aGravatar msozeau2010-06-09
| | | | | | | different (eqdep) database. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing commit r13090 (forgot to commit the file generating Nmake_gen.v).Gravatar herbelin2010-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13095 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
| | | | | | | people use the undocumented "Lemma foo x : t" feature in a way incompatible with this activation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unfolding tactic for well-founded Programs.Gravatar msozeau2010-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ascii: simplier ascii_of_pos, conversion from/to N, proofs about ↵Gravatar letouzey2010-06-04
| | | | | | | | | | | nat-->ascii-->nat - ascii_of_pos isn't tail-recursive anymore, but recursivity is at most of depth 8. - (brutal) proof that N_of_ascii (ascii_of_N n) = n for all n<256, same for nat. Ideally, we could say someday that N_of_ascii (ascii_of_N n) = n mod 256 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13077 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction program_simplify. Devrait corriger certaines contribs.Gravatar aspiwack2010-05-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13031 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized the formulation of classic_set in propositional contextsGravatar herbelin2010-05-28
| | | | | | (consequence of classical unique choice) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added UIP_dec on suggestion of Eelis on #coq irc.Gravatar herbelin2010-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
| | | | | | Ocaml 3.10.0 is already three year old... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13015 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13005 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
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a fairly large commit (around 140 files and 7000 lines of code impacted), it will cause some troubles for sure (I've listed the know regressions below, there is bound to be more). At this state of developpement it brings few features to the user, as the old tactics were ported with no change. Changes are on the side of the developer mostly. Here comes a list of the major changes. I will stay brief, but the code is hopefully well documented so that it is reasonably easy to infer the details from it. Feature developer-side: * Primitives for a "real" refine tactic (generating a goal for each evar). * Abstract type of tactics, goals and proofs * Tactics can act on several goals (formally all the focused goals). An interesting consequence of this is that the tactical (. ; [ . | ... ]) can be separated in two tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for this particular syntax). We can also imagine a tactic to reorder the goals. * Possibility for a tactic to pass a value to following tactics (a typical example is an intro function which tells the following tactics which name it introduced). * backtracking primitives for tactics (it is now possible to implement a tactical '+' with (a+b);c equivalent to (a;c+b;c) (itself equivalent to (a;c||b;c)). This is a valuable tool to implement tactics like "auto" without nowing of the implementation of tactics. * A notion of proof modes, which allows to dynamically change the parser for tactics. It is controlled at user level with the keywords Set Default Proof Mode (this is the proof mode which is loaded at the start of each proof) and Proof Mode (switches the proof mode of the current proof) to control them. * A new primitive Evd.fold_undefined which operates like an Evd.fold, except it only goes through the evars whose body is Evar_empty. This is a common operation throughout the code, some of the fold-and-test-if-empty occurences have been replaced by fold_undefined. For now, it is only implemented as a fold-and-test, but we expect to have some optimisations coming some day, as there can be a lot of evars in an evar_map with this new implementation (I've observed a couple of thousands), whereas there are rarely more than a dozen undefined ones. Folding being a linear operation, this might result in a significant speed-up. * The declarative mode has been moved into the plugins. This is made possible by the proof mode feature. I tried to document it so that it can serve as a tutorial for a tactic mode plugin. Features user-side: * Unfocus does not go back to the root of the proof if several Focus-s have been performed. It only goes back to the point where it was last focused. * experimental (non-documented) support of keywords BeginSubproof/EndSubproof: BeginSubproof focuses on first goal, one can unfocus only with EndSubproof, and only if the proof is completed for that goal. * experimental (non-documented) support for bullets ('+', '-' and '*') they act as hierarchical BeginSubproof/EndSubproof: First time one uses '+' (for instance) it focuses on first goal, when the subproof is completed, one can use '+' again which unfocuses and focuses on next first goal. Meanwhile, one cas use '*' (for instance) to focus more deeply. Known regressions: * The xml plugin had some functions related to proof trees. As the structure of proof changed significantly, they do not work anymore. * I do not know how to implement info or show script in this new engine. Actually I don't even know what they were suppose to actually mean in earlier versions either. I wager they would require some calm thinking before going back to work. * Declarative mode not entirely working (in particular proofs by induction need to be restored). * A bug in the inversion tactic (observed in some contributions) * A bug in Program (observed in some contributions) * Minor change in the 'old' type of tactics causing some contributions to fail. * Compilation time takes about 10-15% longer for unknown reasons (I suspect it might be linked to the fact that I don't perform any reduction at QED-s, and also to some linear operations on evar_map-s (see Evd.fold_undefined above)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 14:19:15 +0000