diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2016-08-30 17:12:27 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-08-30 17:59:59 +0200 |
| commit | 721637c98514a77d05d080f53f226cab3a8da1e7 (patch) | |
| tree | 9a04e0482488764d39c0e24847e93f4b23f62cde /plugins/micromega/Psatz.v | |
| parent | 44ada644ef50563aa52cfcd7717d44bde29e5a20 (diff) | |
plugin micromega : nra also handles non-linear rational arithmetic over Q (Fixed #4985)
Lqa.v defines the tactics lra and nra working over Q.
Lra.v defines the tactics lra and nra working over R.
Diffstat (limited to 'plugins/micromega/Psatz.v')
| -rw-r--r-- | plugins/micromega/Psatz.v | 40 |
1 files changed, 22 insertions, 18 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index fafd8a5f2..b1f242f58 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 *) (* *) (************************************************************************) @@ -75,35 +75,39 @@ 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))) + 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 * ; - 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))) - | _ => fail "Unsupported domain" + 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" end in tac. Ltac lra := first [ psatzl R | psatzl Q ]. -Ltac nra := +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). - + 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 ]. (* Local Variables: *) |