| Age | Commit message (Collapse) | Author |
|---|
|
By default Coq stdlib warnings raise an error, so this is really required.
|
|
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
- Improved reification for Micromega (support for #8764)
- Fixes #9268: Do not take universes into account in lia reification
Improve #9291 by threading the evar_map during reification.
Universes are unified.
- Remove (potentially cyclic) dependency over lra for Rle_abs
- Towards a complete simplex-based lia
fixes #9615
Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.
For scalability, nia is currently NOT performing this pre-processing.
- Lia is using the FSet library
manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
to work around a "leaked" hint breaking compatibility of eauto
|
|
Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).
|
|
|
|
The manual has long stated that these forms are deprecated. We add a
warning for them, as indeed `Add Morphism` is an "proof evil" [*]
command, and we may want to remove it in the future.
We've also fixed the stdlib not to emit the warning.
[*] https://ncatlab.org/nlab/show/principle+of+equivalence
|
|
- 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
|
|
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
|
|
- 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
|
|
In fact, this formula "fold ... = fold_right ... (rev (elements))"
was already frequently used, but without ever stating it explicitely.
Instead, we were always chaining two rewrites each time.
Thanks to A. Appel for mentionning this question of fold_right vs.
fold_left in the spec of fold.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14561 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- 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
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
pattern unification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12202 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- New functions: update (a kind of union), restrict (a kind of inter),
diff.
- New predicat Partition (and Disjoint), many results about Partition.
- Equivalence instead of obsolete Setoid_Theory (they are aliases).
refl_st, sym_st, trans_st aren't used anymore and marked as obsolete.
- Start using Morphism (E.eq==>...) instead of compat_...
This change (FMaps only) is incompatible with 8.2betaX, but it's really
better now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The induction principles for fold are due to S. Lescuyer
The better transpose hyp is a suggestion by P. Casteran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11711 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11698 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
DecidableType
After lots of hesitations, OrderedType now requires this "eq_dec" field, which
is redundant (can be deduced from "compare"), but allows the subtyping relation
DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly
extensions of weak sets. Of course this change introduces a last-minute
incompatibility, but:
- There is a clear gain in term of functionnality / simplicity.
- FSets 8.2 already needs some adaptations when compared with 8.1, so it's
the right time to push such incompatible changes.
- Transition shouldn't be too hard: the old OrderedType still exists under
the name MiniOrderedType, and functor MOT_to_OT allows to convert from
one to the other.
Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType
(resp. OrderedType), an eq_dec on sets is now required in these interfaces
and in the implementations. In pratice, it is really easy to build from
equal and equal_1 and equal_2.
Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun,
while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M).
Idem with WDecide, WProperties and WEqProperties.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11064 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10636 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10605 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
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
|
|
(from A. Bohannon)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10420 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
more general.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10295 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
See recent discussion in coq-club.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10243 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
FSetProperties)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9885 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* 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
|
|
(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
|
|
conséquences sur les .v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8815 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Du coup, factorisation d'une partie dans SetoidList. Ajout de
lemmes suggeres par Evelyne C. Un oubli dans FSetWeakInterface
concernant elements.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
des fichiers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8639 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8636 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8635 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8631 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8629 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
pas d'implementations par AVL, mais celles par lists, ainsi que les
foncteurs de proprietes.
Au passage, ajout de MoreList (complements de List) et SetoidList
(quelques relations sur des listes considerees modulo un eq ou lt
non standard.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8628 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4205 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4159 85f007b7-540e-0410-9357-904b9bb8a0f7
|
