From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 plugins/micromega/Psatz.v | 71 ++++++++++++-----------------------------------
 1 file changed, 17 insertions(+), 54 deletions(-)

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

diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index a461b26a..8acf0ff8 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -8,7 +8,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2016                             *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -20,75 +20,36 @@ Require Import ZArith.
 Require Import Rdefinitions.
 Require Import RingMicromega.
 Require Import VarMap.
-Require Tauto.
-Declare ML Module "micromega_plugin".
+Require Coq.micromega.Tauto.
+Require Lia.
+Require Lra.
+Require Lqa.
 
-Ltac preprocess := 
-    zify ; unfold Z.succ in * ; unfold Z.pred in *.
+Declare ML Module "micromega_plugin".
 
-Ltac lia :=
-  preprocess;
-  xlia ;
-  abstract (
-  intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
+Ltac lia := Lia.lia.
 
-Ltac nia :=
-  preprocess;
-  xnlia ;
-  abstract (
-  intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
+Ltac nia := Lia.nia.
 
 
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
   | Z =>
-    (sos_Z || psatz_Z d) ;
-      abstract(
-    intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-    apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))
+    (sos_Z Lia.zchecker) || (psatz_Z d  Lia.zchecker)
   | R =>
-    (sos_R || psatz_R d) ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try (abstract(intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-        apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
-  | Q =>
-    (sos_Q || psatz_Q d) ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try  (abstract(intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
-        apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
+    (sos_R Lra.rchecker) || (psatz_R d Lra.rchecker)
+  | Q => (sos_Q Lqa.rchecker) || (psatz_Q d Lqa.rchecker) 
   | _ => fail "Unsupported domain"
   end in tac.
 
 Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
-Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1.
+Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
 
 Ltac psatzl dom :=
   let tac := lazymatch dom with
-  | Z => lia
-  | Q =>
-    psatzl_Q ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try (abstract(intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
-        apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
-  | R =>
-    unfold Rdiv in * ; 
-    psatzl_R ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try abstract((intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-        apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
+  | Z => Lia.lia
+  | Q => Lqa.lra
+  | R => Lra.lra
   | _ => fail "Unsupported domain"
   end in tac.
 
@@ -96,6 +57,8 @@ Ltac psatzl dom :=
 Ltac lra := 
   first [ psatzl R | psatzl Q ].
 
+Ltac nra := 
+  first [ Lra.nra | Lqa.nra ].  
 
 
 (* Local Variables: *)
-- 
cgit v1.2.3