Rify + lra solves Mixed Integer Programs

test-suite/bugs/bug_16803.v

@@ -1,6 +1,6 @@
 From Stdlib Require Import Lia.
 From Stdlib Require Import ZArith.
-Import ZifyClasses.
+Import TifyClasses.
 
 Module Test1.
 

test-suite/bugs/bug_18151.v

@@ -3,25 +3,25 @@ From Stdlib Require Import Zify ZifyClasses.
 Import Z.
 Open Scope Z_scope.
 
-#[global] Instance sat_mod_le : ZifyClasses.Saturate BinIntDef.Z.modulo :=
+#[global] Instance sat_mod_le : Saturate BinIntDef.Z.modulo :=
   {|
-    ZifyClasses.PArg1 := fun a => 0 <= a;
-    ZifyClasses.PArg2 := fun b => 0 < b;
-    ZifyClasses.PRes := fun a b ab => ab <= a;
-    ZifyClasses.SatOk := mod_le
+    PArg1 := fun a => 0 <= a;
+    PArg2 := fun b => 0 < b;
+    PRes := fun a b ab => ab <= a;
+    SatOk := mod_le
   |}.
 Add Zify Saturate sat_mod_le.
 
 Lemma shiftr_lbound a n:
    0 <= a -> True -> 0 <= (Z.shiftr a n).
 Proof. now intros; apply Z.shiftr_nonneg. Qed.
 
-#[global] Instance sat_shiftr_lbound : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
+#[global] Instance sat_shiftr_lbound : Saturate BinIntDef.Z.shiftr :=
   {|
-    ZifyClasses.PArg1 := fun a => 0 <= a;
-    ZifyClasses.PArg2 := fun b => True;
-    ZifyClasses.PRes := fun a b ab => 0 <= ab;
-    ZifyClasses.SatOk := shiftr_lbound
+    PArg1 := fun a => 0 <= a;
+    PArg2 := fun b => True;
+    PRes := fun a b ab => 0 <= ab;
+    SatOk := shiftr_lbound
   |}.
 Add Zify Saturate sat_shiftr_lbound.
 

test-suite/micromega/bug_18158.v

@@ -40,42 +40,42 @@ Proof.
   intros; apply shiftr_ubound; assumption.
 Qed.
 
-#[global] Instance sat_shiftr_lbound : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
+#[global] Instance sat_shiftr_lbound : TifyClasses.Saturate BinIntDef.Z.shiftr :=
   {|
-    ZifyClasses.PArg1 := fun a => 0 <= a;
-    ZifyClasses.PArg2 := fun b => True;
-    ZifyClasses.PRes := fun a b ab => 0 <= ab;
-    ZifyClasses.SatOk := shiftr_lbound
+    TifyClasses.PArg1 := fun a => 0 <= a;
+    TifyClasses.PArg2 := fun b => True;
+    TifyClasses.PRes := fun a b ab => 0 <= ab;
+    TifyClasses.SatOk := shiftr_lbound
   |}.
-Add Zify Saturate sat_shiftr_lbound.
+Add Tify Saturate sat_shiftr_lbound.
 
-#[global] Instance sat_shiftr_contr_8 : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
+#[global] Instance sat_shiftr_contr_8 : TifyClasses.Saturate BinIntDef.Z.shiftr :=
   {|
-    ZifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 8;
-    ZifyClasses.PArg2 := fun b => 0 <= b;
-    ZifyClasses.PRes := fun a b ab => ab < 2 ^ 8;
-    ZifyClasses.SatOk := shiftrContractive8
+    TifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 8;
+    TifyClasses.PArg2 := fun b => 0 <= b;
+    TifyClasses.PRes := fun a b ab => ab < 2 ^ 8;
+    TifyClasses.SatOk := shiftrContractive8
   |}.
-Add Zify Saturate sat_shiftr_contr_8.
+Add Tify Saturate sat_shiftr_contr_8.
 
-#[global] Instance sat_shiftr_contr_16 : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
+#[global] Instance sat_shiftr_contr_16 : TifyClasses.Saturate BinIntDef.Z.shiftr :=
   {|
-    ZifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 16;
-    ZifyClasses.PArg2 := fun b => 0 <= b;
-    ZifyClasses.PRes := fun a b ab => ab < 2 ^ 16;
-    ZifyClasses.SatOk := shiftrContractive16
+    TifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 16;
+    TifyClasses.PArg2 := fun b => 0 <= b;
+    TifyClasses.PRes := fun a b ab => ab < 2 ^ 16;
+    TifyClasses.SatOk := shiftrContractive16
   |}.
-Add Zify Saturate sat_shiftr_contr_16.
+Add Tify Saturate sat_shiftr_contr_16.
 
 
-#[global] Instance sat_shiftr_contr_32 : ZifyClasses.Saturate BinIntDef.Z.shiftr :=
+#[global] Instance sat_shiftr_contr_32 : TifyClasses.Saturate BinIntDef.Z.shiftr :=
   {|
-    ZifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 32;
-    ZifyClasses.PArg2 := fun b => 0 <= b;
-    ZifyClasses.PRes := fun a b ab => ab < 2 ^ 32;
-    ZifyClasses.SatOk := shiftrContractive32
+    TifyClasses.PArg1 := fun a => 0 <= a < 2 ^ 32;
+    TifyClasses.PArg2 := fun b => 0 <= b;
+    TifyClasses.PRes := fun a b ab => ab < 2 ^ 32;
+    TifyClasses.SatOk := shiftrContractive32
   |}.
-Add Zify Saturate sat_shiftr_contr_32.
+Add Tify Saturate sat_shiftr_contr_32.
 
 
 Goal forall x y ,
@@ -85,7 +85,7 @@ Goal forall x y ,
     -> Z.le (Z.shiftr y 8) 255
     -> Z.le (Z.shiftr x 24) 255.
   intros.
-  Zify.zify_saturate.
+  Tify.tify_saturate.
   (* [xlia zchecker] used to raise a [Stack overflow] error. It is supposed to fail normally. *)
   assert_fails (xlia zchecker).
 Abort.

test-suite/micromega/milp.v

@@ -0,0 +1,253 @@
+Require Import Rbase Rify isZ Lra Zfloor.
+Local Open Scope R_scope.
+
+Unset Lra Cache.
+
+Lemma up0 : up 0%R = 1%Z.
+Proof. intros. lra. Qed.
+
+Lemma up_succ r : up (r + 1)%R = (up r + 1)%Z.
+Proof. intros. lra. Qed.
+
+Lemma up_IZR z : up (IZR z) = (z + 1)%Z.
+Proof.
+  lra.
+Qed.
+
+Lemma up_shiftz r z : up (r + IZR z)%R = (up r + z)%Z.
+Proof.
+  lra.
+Qed.
+
+Lemma div_inv : forall y  x,
+   1 = 1 + (y - x) / x ->
+   (y - x) * / x = 0.
+Proof. intros. lra. Qed.
+
+Goal forall (x1 : R) (x2 : R) (x3 : R) (x4 : R) (x5 : R) (x6 : R)
+(H0 : -x2 + x6 = R0)
+(H1 : x6 + -x4 = R0)
+(H2 : x2*x3 + -x1*x3 = R0)
+(H3 : x4 + -x2*x5 = R0)
+(H5 : x2*x3 + -x1*x3 > R0)
+, False
+.
+Proof.
+  intros.
+  lra.
+Qed.
+
+Goal forall (x1 : R) (x2 : R) (x3 : R) (x4 : R)
+(H0 : x4 >= 0)
+(H1 : 1 + -x4 > 0)
+(H2 : -x4 + x1 > 0)
+(H3 : 1 + -x1 > 0)
+(H4 : x2 + -x3 = 0)
+(H5 : -x1 > 0)
+, False
+.
+Proof.
+  intros.
+  lra.
+Qed.
+
+
+Goal forall (x1 : R) (x2 : R) (x3 : R) (x4 : R)
+(H0 : x4 >= 0)
+(H1 : 1 + -x4 > 0)
+(H2 : -x4 + x1 > 0)
+(H3 : 1 + -x1 > 0)
+(H4 : x2 + -x3 = 0)
+(H5 : -x1 > 0)
+, False
+.
+Proof.
+  intros.
+  lra.
+Qed.
+
+
+
+
+Goal forall (x1 : R) (x2 : R) (x3 : R) (x4 : R) (x5 : R) (x6 : R)
+(H0 : -x2 + x6 = R0)
+(H1 : x6 + -x4 = R0)
+(H2 : x2*x3 + -x1*x3 = R0)
+(H3 : x4 + -x2*x5 = R0)
+(H5 : x2*x3 + -x1*x3 > R0)
+, False
+.
+Proof.
+  lra.
+Qed.
+
+Lemma up_succ2 r n : Zfloor (r + IZR n) = (Zfloor r + n)%Z.
+Proof.
+  lra.
+Qed.
+
+Goal forall x1 x2 x3  x5 x6
+    (H: -x2 > 0)
+    (H0: x3 >= 0)
+    (H1: -x1 + x5 + x6 = 0)
+    (H2: x1 + -x5 + x6 = 0)
+    (H4: -x1 > 0)
+    (H6: x2 + -x3 = 0)
+    (H7: 3 + 3*x1 = 0),
+    False.
+Proof.
+  intros.
+  lra.
+Qed.
+
+
+Lemma spurious_isZ : forall
+    (x l X : R)
+    (delta : R)
+    (iZ1    : isZ x)
+    (H13 :  - (X - l) <= 0)
+    (iZ2    : isZ X)
+    (H4 : l > 0)
+    (iZ2    : isZ X)
+    (H9 : delta / 2 <> 0)
+    (iZ2    : isZ X)
+    (H11 : 0 < delta / 2)
+    (iZ1    : isZ x)
+    (H10 : (X <= 0)),
+    False.
+Proof.
+  intros.
+  lra.
+Qed.
+
+Goal forall (k x:R) (P:Prop)
+            (Hyp : 0 <= k < 1)
+            (H2 : k < x < 1 /\ P)
+            (H3 : k < x < 1),
+  0 < x.
+Proof.
+  intros.
+  lra.
+Qed.
+
+
+  Ltac cnf := match goal with
+              | |- Tauto.cnf_checker  _ ?F _ = true =>
+                  let f:= fresh "f" in
+                  set(f:=F); compute in f; unfold f;clear f
+              end.
+
+  Ltac collect :=
+    match goal with
+      | |- context [ RMicromega.xcollect_isZ ?A ?B ?F] =>
+        let f := fresh "f" in
+        set (f:= RMicromega.xcollect_isZ A B F) ; compute in f ; unfold f; clear f
+    end.
+
+
+Goal forall (x y:R)
+    (H : x <= y)
+    (Hlt : x < y),
+    y - x = 0 -> False.
+Proof.
+  intros.
+  lra.
+Qed.
+
+Lemma two_x_1 : forall (x:R)
+            (IZ : isZ x)
+            (H : 2 * x + 1 =  0),
+    False.
+Proof.
+  intros.
+  lra.
+Qed.
+
+Goal forall x1 x2 x3 x4,
+    isZ x1 ->
+    isZ x2 ->
+    isZ x3 ->
+    isZ x4 ->
+    - x1 + x2 - x3 + x4 >= 0 ->
+    x1 - x2 + x3 - x4 + 1 > 0 ->
+    - x1 + x2 - x3 + x4  >  0 ->
+    False.
+Proof.
+  intros. lra.
+Qed.
+
+
+
+Goal forall z1 z2 z3, Zfloor (IZR z1 - IZR z2 + IZR z3)%R = (z1 - z2 + z3)%Z.
+Proof.
+  intros.
+  rify.
+  (** Now, some work over isZ *)
+  lra.
+Qed.
+
+Goal forall (z : Z) x, IZR z <= x -> (z <= Zfloor x)%Z.
+Proof.
+  rify.
+  lra.
+Qed.
+
+
+
+Goal forall (z : Z) x,  IZR z <= x < IZR z + 1 -> Zfloor x = z.
+Proof.
+  intros.
+  rify.
+  lra.
+Qed.
+
+
+Goal R1 + (R1 + R1) = 3.
+Proof.
+  intros.
+  rify.
+  reflexivity.
+Qed.
+
+Goal forall x,
+    x * 3 = 1 ->
+    False.
+Proof.
+  intros.
+  Fail lra.
+Abort.
+
+Goal forall x,
+    isZ x ->
+    x * 3 = 1 ->
+    False.
+Proof.
+  intros.
+  lra.
+Qed.
+
+
+
+Require Import Rfunctions R_sqrt.
+
+Goal forall e x
+            (He : 0 < e)
+            (ef := Rmin (e / (3 * (Rabs (x) + 1))) (sqrt (e / 3)) : R)
+            (H : sqrt (e / 3) > 0)
+            (H0 : 3 * (Rabs ( x) + 1) >= 1),
+            0 < ef.
+Proof.
+  intros.
+  nra.
+Qed.
+
+
+Goal forall x v,
+            v * (3  * x) = 1 ->
+            x >= 1 ->
+            v = 1 / (3 * x).
+Proof.
+  intros.
+  nra.
+Qed.
+

test-suite/micromega/rexample.v

@@ -75,11 +75,12 @@ Proof.
   lra.
 Qed.
 
-Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
+(*Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
 Proof.
   intros.
   psatz R 3.
 Qed.
+ *)
 
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
 Proof.

test-suite/micromega/witness_tactics.v

@@ -1,6 +1,6 @@
 From Stdlib Require Import ZArith QArith.
 From Stdlib.micromega Require Import RingMicromega EnvRing Tauto.
-From Stdlib.micromega Require Import ZMicromega QMicromega.
+From Stdlib.micromega Require Import ZMicromega QMicromega MMicromega.
 
 Declare ML Module "rocq-runtime.plugins.micromega".