From 8193ca191cc435c108a4842ae38a11d74c7c20a5 Mon Sep 17 00:00:00 2001
From: BESSON Frederic
Date: Wed, 31 Mar 2021 22:16:50 +0200
Subject: [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
---
 theories/micromega/Zify.v        |  5 +++--
 theories/micromega/ZifyClasses.v |  1 +
 theories/micromega/ZifyInst.v    | 39 ++++++++++-----------------------------
 3 files changed, 14 insertions(+), 31 deletions(-)

(limited to 'theories/micromega')

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.
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index a08a56b20e..019d11d951 100644
--- a/theories/micromega/ZifyClasses.v
+++ b/theories/micromega/ZifyClasses.v
@@ -274,3 +274,4 @@ Register impl_morph as ZifyClasses.impl_morph.
 Register not as ZifyClasses.not.
 Register not_morph as ZifyClasses.not_morph.
 Register True as ZifyClasses.True.
+Register I as ZifyClasses.I.
diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v
index dd31b998d4..8dee70be45 100644
--- a/theories/micromega/ZifyInst.v
+++ b/theories/micromega/ZifyInst.v
@@ -480,39 +480,20 @@ Add Zify UnOpSpec ZabsSpec.
 
 (** Saturate positivity constraints *)
 
-Instance SatProd : Saturate Z.mul :=
-  {|
-    PArg1 := fun x => 0 <= x;
-    PArg2 := fun y => 0 <= y;
-    PRes  := fun r => 0 <= r;
-    SatOk := Z.mul_nonneg_nonneg
-  |}.
-Add Zify Saturate SatProd.
-
-Instance SatProdPos : Saturate Z.mul :=
+Instance SatPowPos : Saturate Z.pow :=
   {|
     PArg1 := fun x => 0 < x;
-    PArg2 := fun y => 0 < y;
+    PArg2 := fun y => 0 <= y;
     PRes  := fun r => 0 < r;
-    SatOk := Z.mul_pos_pos
+    SatOk := Z.pow_pos_nonneg
   |}.
-Add Zify Saturate SatProdPos.
-
-Lemma pow_pos_strict :
-  forall a b,
-    0 < a -> 0 < b -> 0 < a ^ b.
-Proof.
-  intros.
-  apply Z.pow_pos_nonneg; auto.
-  apply Z.lt_le_incl;auto.
-Qed.
-
+Add Zify Saturate SatPowPos.
 
-Instance SatPowPos : Saturate Z.pow :=
+Instance SatPowNonneg : Saturate Z.pow :=
   {|
-    PArg1 := fun x => 0 < x;
-    PArg2 := fun y => 0 < y;
-    PRes  := fun r => 0 < r;
-    SatOk := pow_pos_strict
+    PArg1 := fun x => 0 <= x;
+    PArg2 := fun y => True;
+    PRes  := fun r => 0 <= r;
+    SatOk := fun a b Ha _ => @Z.pow_nonneg a b Ha
   |}.
-Add Zify Saturate SatPowPos.
+Add Zify Saturate SatPowNonneg.
-- 
cgit v1.2.3