| Age | Commit message (Collapse) | Author |
|---|
|
The role of the `zify_saturate` tactic is to augment the goal with
positivity constraints. The premisses were previously obtained from
the context. If they are not present, we instantiate the saturation
lemma anyway.
Also,
- Remove saturation rules for Z.mul, the reasoning is performed by lia/nia
- Run zify_saturate after zify_to_euclidean_division_equations
- Better lemma for Z.power
- Ensure that lemma are generated once
Co-authored-by: Andrej Dudenhefner <mrhaandi>
Closes #12184, #11656
|
|
|
|
Changes to the test-suite were backported from PR #11288.
|
|
Compared to the original proposition (59a594b in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
|
------------------------------------------------
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7849 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5150 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5132 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dependances, il n'y a pas de garantie de pouvoir les effacer pour garder le meme nom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5131 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
ces hypothèses étaient dépendantes dans d'autres hypothèses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3178 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2764 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2759 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2438 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2420 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2417 85f007b7-540e-0410-9357-904b9bb8a0f7
|
