[micromega] fix of bug #11191

- Add an instance to ZifyInst to instruct zify that
 0 < x -> 0 < y -> 0 < Z.pow x y

- More aggressive interval analysis to bound non-linear monomials.

1 files changed, 19 insertions, 0 deletions

diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v
index 97f6fe0613..edfb5a2a94 100644
--- a/plugins/micromega/ZifyInst.v
+++ b/plugins/micromega/ZifyInst.v
@@ -523,3 +523,22 @@ Instance SatProdPos : Saturate Z.mul :=
     SatOk := Z.mul_pos_pos
   |}.
 Add 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.
+
+
+Instance SatPowPos : Saturate Z.pow :=
+  {|
+    PArg1 := fun x => 0 < x;
+    PArg2 := fun y => 0 < y;
+    PRes  := fun r => 0 < r;
+    SatOk := pow_pos_strict
+  |}.
+Add Saturate SatPowPos.