Library Stdlib.micromega.Lra

From Stdlib Require Import RMicromega.
From Stdlib Require Import QMicromega.
From Stdlib Require Import Rdefinitions.
From Stdlib Require Import RingMicromega.
From Stdlib Require Import VarMap.
From Stdlib.micromega Require Tauto.
From Stdlib Require Import Rregisternames.


Ltac rchange :=
  let __wit := fresh "__wit" in
  let __varmap := fresh "__varmap" in
  let __ff := fresh "__ff" in
  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.

Ltac lra := unfold Rdiv in * ; xlra_R rchecker.

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).