Library Coq.micromega.Lra
Require Import RMicromega.
Require Import QMicromega.
Require Import Rdefinitions.
Require Import RingMicromega.
Require Import VarMap.
Require Coq.micromega.Tauto.
Require Import Rregisternames.
Ltac rchange :=
intros ?__wit ?__varmap ?__ff ;
change (Tauto.eval_bf (Reval_formula (@find R 0%R __varmap)) __ff) ;
apply (RTautoChecker_sound __ff __wit).
Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.
Ltac rchecker_abstract := rchange ; vm_cast_no_check (eq_refl true).
Ltac rchecker := rchecker_no_abstract.
Here, lra stands for linear real arithmetic
Here, nra stands for non-linear real arithmetic
Ltac nra := unfold Rdiv in * ; xnra_R rchecker.
Ltac xpsatz dom d :=
let tac := lazymatch dom with
| R =>
(xsos_R rchecker) || (xpsatz_R d rchecker)
| _ => fail "Unsupported domain"
end in tac.
Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
Ltac xpsatz dom d :=
let tac := lazymatch dom with
| R =>
(xsos_R rchecker) || (xpsatz_R d rchecker)
| _ => fail "Unsupported domain"
end in tac.
Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).