diff options
| author | BESSON Frederic | 2021-03-31 22:16:50 +0200 |
|---|---|---|
| committer | BESSON Frederic | 2021-04-12 22:03:30 +0200 |
| commit | 8193ca191cc435c108a4842ae38a11d74c7c20a5 (patch) | |
| tree | 3a80c743305718fe8f8aaf35524afee4dd3e542b /theories/micromega/Zify.v | |
| parent | b78e6cfcb412d1c4e5902fb895c5ecaa0cb177ac (diff) | |
[zify] More aggressive application of saturation rules
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
Diffstat (limited to 'theories/micromega/Zify.v')
| -rw-r--r-- | theories/micromega/Zify.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v index 01cc9ad810..3a50001b1f 100644 --- a/theories/micromega/Zify.v +++ b/theories/micromega/Zify.v @@ -33,5 +33,6 @@ Ltac zify := intros; zify_elim_let ; zify_op ; (zify_iter_specs) ; - zify_saturate ; - zify_to_euclidean_division_equations ; zify_post_hook. + zify_to_euclidean_division_equations ; + zify_post_hook; + zify_saturate. |