diff options
Diffstat (limited to 'plugins/micromega/Psatz.v')
| -rw-r--r-- | plugins/micromega/Psatz.v | 20 |
1 files changed, 17 insertions, 3 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index fde0f29a..7f6cf79b 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-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,7 +18,7 @@ Require Import RMicromega. Require Import QArith. Require Export Ring_normalize. Require Import ZArith. -Require Import Raxioms. +Require Import Rdefinitions. Require Export RingMicromega. Require Import VarMap. Require Tauto. @@ -66,6 +66,7 @@ Ltac psatzl dom := change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity) | 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'. *) @@ -75,12 +76,25 @@ Ltac psatzl dom := | _ => fail "Unsupported domain" end in tac. + +Ltac lra := + first [ psatzl R | psatzl Q ]. + Ltac lia := - xlia ; + zify ; unfold Zsucc in * ; + (*cbv delta - [Zplus Zminus Zopp Zmult Zpower Zgt Zge Zle Zlt 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 Zsucc 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: *) (* coding: utf-8 *) (* End: *) |