aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Same for FinGravatar pboutill2012-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15648 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vector equalities first stuffGravatar pboutill2012-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
| | | | | | | | | | | | After discovering a rewrite in Ergo that takes a loooong time due to a bad interaction with the instances of Permutation and PermutationA : - PermutationA is now in a separate file SetoidPermutation - File Permutation.v isn't Require'd by SetoidList anymore nor MergeSort.v, just the definitions in Sorted.v - Attempt to put a priority on these instances. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15584 85f007b7-540e-0410-9357-904b9bb8a0f7
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
| | | | | | | | | | | | | | | | | | The ugly syntax "destruct x as [ ]_eqn:H" is replaced by: destruct x eqn:H destruct x as [ ] eqn:H Some with induction. Of course, the pattern behind "as" is arbitrary. For an anonymous version, H could be replaced by ?. The old syntax with "_eqn" still works for the moment, by triggers a warning. For making this new syntax work, we had to change the seldom-used "induction x y z using foo" into "induction x, y, z using foo". Now, only one "using" can be used per command instead of one per comma-separated group earlier, but I doubt this will bother anyone. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Two adaptations after the changes of level of ->Gravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15541 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinPos/BinInt/BinNat : fix some argument scopesGravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15540 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore the compatibility notation Compare.not_eq_symGravatar letouzey2012-07-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
| | | | | | | | | One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some cleanup in recent proofs concerning piGravatar letouzey2012-07-05
| | | | | | | | Initial idea was to just avoid compat notations such as Z_of_nat --> Z.of_nat, but I ended trying to improve a few proofs... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15520 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetRBT : elementary arith proofs instead of calls to liaGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15519 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
| | | | | | | Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15517 85f007b7-540e-0410-9357-904b9bb8a0f7
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | - For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | | | | | Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ↵Gravatar pboutill2012-06-20
| | | | | | patch git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2695: infinite loop in dependent destruction.Gravatar msozeau2012-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15451 85f007b7-540e-0410-9357-904b9bb8a0f7
* BinInt: a forgotten scope for a notationGravatar letouzey2012-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15450 85f007b7-540e-0410-9357-904b9bb8a0f7
* These files are displaced from Rtrigo.v and Ranalysis_reg.vGravatar bertot2012-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15430 85f007b7-540e-0410-9357-904b9bb8a0f7
* finish the rearrangement for removing the sin_PI2 axiom. This new versionGravatar bertot2012-06-11
| | | | | | | | | | | | | | | - provides the atan function - shows that this function is equal between -1 and 1 to a function defined with power series - establishes the equality with the PI value as given by the alternated series constructed with PI_tg - provides a smarter theorem to compute approximations of PI, based on a formula in the same family as the one used by John Machin in 1706 Dependencies between files have been rearranged so that the new theorems are loaded with the library Reals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15429 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds the proof of PI_ineq, plus some other smarter ways to approximate PIGravatar bertot2012-06-11
| | | | | | | and of course, the definition of atan (the inverse of tan, from R to (-PI/2, PI/2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications and rearrangements to remove the action that sin (PI/2) = 1Gravatar bertot2012-06-05
| | | | | | Beware that the definition of PI changes in the process git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15425 85f007b7-540e-0410-9357-904b9bb8a0f7
* list_eq_dec now transparent (wish #2786)Gravatar letouzey2012-06-01
| | | | | | | The proof is also replaced by a mere "decide equality". Patch by Robbert Krebbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Functions *_beq aren't generated anymore, remove comments about themGravatar letouzey2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15402 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs revealed by playing with contribsGravatar pboutill2012-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15364 85f007b7-540e-0410-9357-904b9bb8a0f7
* Permutation: remove a compatibility notation which doesn't help MathClassesGravatar letouzey2012-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15341 85f007b7-540e-0410-9357-904b9bb8a0f7
* SetoidList: explicit the fact that InfA_compat won't use ltA_strorderGravatar letouzey2012-05-22
| | | | | | | | For that, we use the new "Proof using ...". This way, we're sure that a later change in the behavior of intuition or any other tactics will not create an artificial dependency again (cf. r15180). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15340 85f007b7-540e-0410-9357-904b9bb8a0f7
* List + Permutation : more results about nth_error and nthGravatar letouzey2012-05-18
| | | | | | | | | | In particular, characterisation of NoDup and Permutation in term of nth_error and nth Some of these results have been suggested last year by Bas Spitters (cf. MathClasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intuition: temporary(?) restore the unconditional unfolding of notGravatar letouzey2012-05-15
| | | | | | | | Let's check tomorrow the impact on contribs: are the recent build failures related to the "not" unfolding stategy or to the new handling of conjonction-like constructors ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vectors takes advantage of pattern matching compiler fixupGravatar pboutill2012-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2767Gravatar pboutill2012-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide highligthing is back (done by gtksourceview).Gravatar pboutill2012-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15269 85f007b7-540e-0410-9357-904b9bb8a0f7
* A notion of permutation for lists modulo a setoid equalityGravatar letouzey2012-05-02
| | | | | | Contribution by Robbert Krebbers (Nijmegen University). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15261 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove undocumented and scarcely-used tactic auto decompGravatar letouzey2012-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the Dp plugin.Gravatar gmelquio2012-04-17
| | | | | | | | | | | | | | | | | | Why2 has not been maintained for the last few years and the Why3 plugin should be a suitable replacement in most cases. Removed tactics: simplify, ergo, yices, cvc3, z3, cvcl, harvey, zenon, gwhy. Removed commands: Dp_hint, Dp_timeout, Dp_prelude, Dp_predefined, Dp_debug, Dp_trace. Note that the "admit" tactic was actually provided by the Dp plugin. It has been moved to extratactics.ml4. Ported from v8.4 r15186. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15189 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing typo in previous commit r15180.Gravatar herbelin2012-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15181 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - tauto/intuition now works uniformly on and, prod, or, sum, False, Empty_set, unit, True (and isomorphic copies of them), iff, ->, and on all inhabited singleton types with a no-arguments constructor such as "eq t t" (even though the last case goes out of propositional logic: this features is so often used that it is difficult to come back on it). - New dtauto and dintuition works on all inductive types with one constructors and no real arguments (for instance, they work on records such as "Equivalence"), in addition to -> and eq-like types. - Moreover, both of them no longer unfold inner negations (this is a souce of incompatibility for intuition and evaluation of the level of incompatibility on contribs still needs to be done). Incidentally, and amazingly, fixing bug #2680 made that constants InfA_compat and InfA_eqA in SetoidList.v lost one argument: old tauto had indeed destructed a section hypothesis "@StrictOrder A ltA@ thinking it was a conjunction, making this section hypothesis artificially necessary while it was not. Renouncing to the unfolding of inner negations made auto/eauto sometimes succeeding more, sometimes succeeding less. There is by the way a (standard) problem with not in auto/eauto: even when given as an "unfold hint", it works only in goals, not in hypotheses, so that auto is not able to solve something like "forall P, (forall x, ~ P x) -> P 0 -> False". Should we automatically add a lemma of type "HYPS -> A -> False" in the hint database everytime a lemma ""HYPS -> ~A" is declared (and "unfold not" is a hint), and similarly for all unfold hints? At this occasion, also re-did some proofs of Znumtheory. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15180 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetRBT : implementation of MSets via Red-Black treesGravatar letouzey2012-04-13
| | | | | | | | | | | | | | | | | | | Initial contribution by Andrew Appel, many ulterior modifications by myself. Interest: red-black trees maintain logarithmic depths as AVL, but they do not rely on integer height annotations as AVL, allowing interesting performance when computing in Coq or after standard extraction. More on this topic in the article by A. Appel. The common parts of MSetAVL and MSetRBT are shared in a new file MSetGenTree which include the definition of tree and functions such as mem fold elements compare subset. Note that the height of AVL trees is now the first arg of the Node constructor instead of the last one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation in the documentation: remove the use of 'coinductive' inGravatar aspiwack2012-04-13
| | | | | | favour of 'co-inductive'. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15162 85f007b7-540e-0410-9357-904b9bb8a0f7
* "A -> B" is a notation for "forall _ : A, B".Gravatar pboutill2012-04-12
| | | | | | | No good reason for that except uniformity so revert this commit if you find a reason against it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15146 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
| | | | | | | | | | | | | | | | | | | | | | | | - fixing missing spaces in the format of the exists' notations (Logic.v); - fixing wrong variable name in check_is_hole error message (topconstr.ml); - interpret expressions with open binders such as "forall x y, t" as "forall (x:_) (y:_),t" instead of "forall (x y:_),t" to avoid the "implicit type" of a variable being propagated to the type of another variable of different base name. An open question remains: when writing explicitly "forall (x y:_),t", should the types of x and y be the same or not. To avoid the "bug" that x and y have implicit types but the one of x takes precedences, I enforced the interpretation (in constrintern, not in parsing) that "forall (x y:_),t" means the same as "forall (x:_) (y:_),t". However, another choice could have been made. Then one would have to check that if x and y have implicit types, they are the same; also, glob_constr should ideally be changed to support a GProd and GLam with multiple names in the same type, especially if this type is an evar. On the contrary, one might also want e.g. "forall x y : list _, t" to mean "forall (x:list _) (y:list _), t" with distinct instanciations of "_" ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing printing level of Utf8 equivalent for ->.Gravatar herbelin2012-03-26
| | | | | | | Parsing with rhs at level 200 was already working thanks to I don't which unexpected magic from camlp4/5. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15096 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
| | | | | | by default typeclass resolution is not launched on goal evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turning proofs of well-ordering of lexicographic product transparentGravatar herbelin2012-03-20
| | | | | | (see discussion on coq-club 5-6 Feb 2012). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15059 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
| | | | | | | | | | | - reinstall (x : T | P) binder syntax extension. - fix a wrong Evd.define in coercion code. - Simplify interface of eterm_obligations to take a single evar_map. - Fix a slightly subtle bug related to resolvability of evars: some were marked unresolvable and never set back to resolvable across calls to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Final part of moving Program code inside the main code. Adapted ↵Gravatar msozeau2012-03-14
| | | | | | add_definition/fixpoint and parsing of the "Program" prefix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Everything compiles again.Gravatar msozeau2012-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove support for "abstract typing constraints" that requires unicity of ↵Gravatar msozeau2012-03-14
| | | | | | | | | | | solutions to unification. Only allow bidirectional checking of constructor applications, enabled by a program_mode flag: it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated with delta-equivalent but not syntactically equivalent terms. Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vector: missing injection lemmas and better impossible branchesGravatar pboutill2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unblocking code in dependent destruction due to zeta being used in ↵Gravatar msozeau2012-02-01
| | | | | | unfold now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "Tentative to fix bug #2628 by not letting intuition break records. ↵Gravatar msozeau2012-01-31
| | | | | | | | | Might be too much of a backwards-incompatible change" Indeed it is breaking too many scripts. This reverts commit 47e9afaaa4c08aca97d4f4b5a89cb40da76bd850. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14956 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 06:52:41 +0000