aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/micromega/Lia.v32
-rw-r--r--plugins/micromega/Lqa.v27
-rw-r--r--plugins/micromega/Lra.v27
-rw-r--r--plugins/micromega/Psatz.v73
-rw-r--r--test-suite/micromega/zomicron.v11
5 files changed, 67 insertions, 103 deletions
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 52bf5ed3d..6974f8d99 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -8,7 +8,7 @@
(* *)
(* Micromega: A reflexive tactic using the Positivstellensatz *)
(* *)
-(* Frédéric Besson (Irisa/Inria) 2013 *)
+(* Frédéric Besson (Irisa/Inria) 2013-2016 *)
(* *)
(************************************************************************)
@@ -19,24 +19,24 @@ Require Import VarMap.
Require Coq.micromega.Tauto.
Declare ML Module "micromega_plugin".
+
Ltac preprocess :=
zify ; unfold Z.succ in * ; unfold Z.pred in *.
-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 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 zchange :=
+ intros __wit __varmap __ff ;
+ change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
+ apply (ZTautoChecker_sound __ff __wit).
+
+Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity.
+
+Ltac zchecker_abstract := abstract (zchange ; vm_cast_no_check (eq_refl true)).
+
+Ltac zchecker := zchecker_abstract || zchecker_no_abstract .
+
+Ltac lia := preprocess; xlia ; zchecker.
+
+Ltac nia := preprocess; xnlia ; zchecker.
(* Local Variables: *)
diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v
index 0055600a0..e3414b849 100644
--- a/plugins/micromega/Lqa.v
+++ b/plugins/micromega/Lqa.v
@@ -19,18 +19,21 @@ Require Import VarMap.
Require Coq.micromega.Tauto.
Declare ML Module "micromega_plugin".
+Ltac rchange :=
+ intros __wit __varmap __ff ;
+ change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
+ apply (QTautoChecker_sound __ff __wit).
+
+Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.
+Ltac rchecker_abstract := abstract (rchange ; vm_cast_no_check (eq_refl true)).
+
+Ltac rchecker := (rchecker_abstract || rchecker_no_abstract).
+
(** Here, lra stands for linear rational arithmetic *)
-Ltac lra := 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))).
+Ltac lra := lra_Q ; rchecker.
(** Here, nra stands for non-linear rational arithmetic *)
-Ltac nra :=
- 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 := xnqa ; rchecker.
Ltac xpsatz dom d :=
let tac := lazymatch dom with
@@ -38,9 +41,7 @@ Ltac xpsatz dom d :=
(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 rchecker
| _ => fail "Unsupported domain"
end in tac.
@@ -48,8 +49,6 @@ Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
-
-
(* Local Variables: *)
(* coding: utf-8 *)
(* End: *)
diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v
index 7ffe1e4ed..4d9cf22dd 100644
--- a/plugins/micromega/Lra.v
+++ b/plugins/micromega/Lra.v
@@ -20,20 +20,21 @@ Require Import VarMap.
Require Coq.micromega.Tauto.
Declare ML Module "micromega_plugin".
+Ltac rchange :=
+ intros __wit __varmap __ff ;
+ change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
+ apply (RTautoChecker_sound __ff __wit).
+
+Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.
+Ltac rchecker_abstract := abstract (rchange ; vm_cast_no_check (eq_refl true)).
+
+Ltac rchecker := rchecker_abstract || rchecker_no_abstract.
+
(** Here, lra stands for linear real arithmetic *)
-Ltac lra :=
- 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)))).
+Ltac lra := unfold Rdiv in * ; lra_R ; rchecker.
(** Here, nra stands for non-linear real arithmetic *)
-Ltac nra :=
- xnra ;
- (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)))).
+Ltac nra := unfold Rdiv in * ; xnra ; rchecker.
Ltac xpsatz dom d :=
let tac := lazymatch dom with
@@ -41,9 +42,7 @@ Ltac xpsatz dom d :=
(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)))
+ try rchecker
| _ => fail "Unsupported domain"
end in tac.
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: *)
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 0ec1dbfbc..1f148becc 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -33,4 +33,13 @@ Lemma compact_proof : forall z,
Proof.
intros.
lia.
-Qed. \ No newline at end of file
+Qed.
+
+Lemma dummy_ex : exists (x:Z), x = x.
+Proof.
+ eexists.
+ lia.
+ Unshelve.
+ exact Z0.
+Qed.
+ \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 16:51:08 +0000