Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.

If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.

1 files changed, 15 insertions, 58 deletions

diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index b1f242f58..c81c025a5 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -21,50 +21,30 @@ Require Import Rdefinitions.
 Require Import RingMicromega.
 Require Import VarMap.
 Require Coq.micromega.Tauto.
-Declare ML Module "micromega_plugin".
+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 || 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) ;
+    try Lra.rchecker
+  | 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)))
+    try  Lqa.rchecker
   | _ => fail "Unsupported domain"
   end in tac.
 
@@ -73,41 +53,18 @@ Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
 
 Ltac psatzl dom :=
   let tac := lazymatch dom with
-  | Z => lia
-  | Q =>
-    lra_Q ;
-      (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 * ; 
-    lra_R ;
-    (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))))
-| _ => fail "Unsupported domain"
+  | Z => Lia.lia
+  | Q => Lqa.lra
+  | R => Lra.lra
+  | _ => fail "Unsupported domain"
   end in tac.
 
 
 Ltac lra := 
   first [ psatzl R | psatzl Q ].
 
-Ltac nra_R := 
-  unfold Rdiv in * ; 
-  xnra ;     
-  abstract 
-    (intros __wit __varmap __ff ;
-      change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-      apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
-
-Ltac nra_Q := 
-  xnqa ;
-  (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))).
-
 Ltac nra := 
-  first [ nra_R | nra_Q ].  
+  first [ Lra.nra | Lqa.nra ].  
 
 
 (* Local Variables: *)