diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2016-08-31 19:12:15 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-08-31 19:12:15 +0200 |
| commit | 7d4b8108bc8fa6951e605cb9b42580ff6f8e583f (patch) | |
| tree | 38851b455ef429d861f46ef7fc4639233254bd1a /plugins/micromega/Lra.v | |
| parent | 985e83e60b6665d17b81830aea4fce3384fe2b5a (diff) | |
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.
Diffstat (limited to 'plugins/micromega/Lra.v')
| -rw-r--r-- | plugins/micromega/Lra.v | 27 |
1 files changed, 13 insertions, 14 deletions
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. |