From 97bec684eb514700879778c0da9b05e4264a99f6 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 6 Jan 2020 11:57:11 +0100
Subject: [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.
---
 plugins/micromega/ZifyInst.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'plugins/micromega/ZifyInst.v')

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.
-- 
cgit v1.2.3