diff options
Diffstat (limited to 'plugins/micromega/Psatz.v')
| -rw-r--r-- | plugins/micromega/Psatz.v | 63 |
1 files changed, 33 insertions, 30 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 42c65b5a..675321d9 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,35 +16,55 @@ Require Import ZMicromega. Require Import QMicromega. Require Import RMicromega. Require Import QArith. -Require Export Ring_normalize. Require Import ZArith. Require Import Rdefinitions. -Require Export RingMicromega. +Require Import RingMicromega. Require Import VarMap. Require 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 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_compute ; reflexivity + apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)) | 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 (intros __wit __varmap __ff ; + try (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) + 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 (intros __wit __varmap __ff ; + try (abstract(intros __wit __varmap __ff ; change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity) + apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) | _ => fail "Unsupported domain" end in tac. @@ -53,26 +73,22 @@ Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1. Ltac psatzl dom := let tac := lazymatch dom with - | Z => - psatzl_Z ; - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity + | 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 (intros __wit __varmap __ff ; + try (abstract(intros __wit __varmap __ff ; change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity) + 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 (intros __wit __varmap __ff ; + try 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) + apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) | _ => fail "Unsupported domain" end in tac. @@ -80,19 +96,6 @@ Ltac psatzl dom := Ltac lra := first [ psatzl R | psatzl Q ]. -Ltac lia := - zify ; unfold Z.succ in * ; - (*cbv delta - [Z.add Z.sub Z.opp Z.mul Z.pow Z.gt Z.ge Z.le Z.lt iff not] ;*) xlia ; - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. - -Ltac nia := - zify ; unfold Z.succ in * ; - xnlia ; - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. (* Local Variables: *) |