# Library Coq.micromega.RMicromega

Require Import OrderedRing.
Require Import RingMicromega.
Require Import Refl.
Require Import Raxioms RIneq Rpow_def DiscrR.
Require Setoid.
Definition Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R).
Add Ring Rring : Rsrt.
Open Scope R_scope.
Lemma Rmult_neutral : forall x:R , 0 * x = 0.
Lemma Rsor : SOR R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt.
Require ZMicromega.
Lemma RZSORaddon :
SORaddon R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle
0%Z 1%Z Zplus Zmult Zminus Zopp
Zeq_bool Zle_bool
IZR Nnat.nat_of_N pow.
Require Import EnvRing.
Definition INZ (n:N) : R :=
match n with
| N0 => IZR 0%Z
| Npos p => IZR (Zpos p)
end.
Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp IZR Nnat.nat_of_N pow.
Definition Reval_op2 (o:Op2) : R -> R -> Prop :=
match o with
| OpEq => @eq R
| OpNEq => fun x y => ~ x = y
| OpLe => Rle
| OpGe => Rge
| OpLt => Rlt
| OpGt => Rgt
end.
Definition Reval_formula (e: PolEnv R) (ff : Formula Z) :=
let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs).
Definition Reval_formula' :=
eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow.
Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f.
Definition Reval_nformula :=
eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt IZR.
Lemma Reval_nformula_dec : forall env d, ( Reval_nformula env d ) \/ ~ ( Reval_nformula env d ).
Definition RWitness := Psatz Z.
Definition RWeakChecker := check_normalised_formulas 0%Z 1%Z Zplus Zmult Zeq_bool Zle_bool.
Require Import List.
Lemma RWeakChecker_sound : forall (l : list (NFormula Z)) (cm : RWitness),
RWeakChecker l cm = true ->
forall env, make_impl (Reval_nformula env) l False.
Require Import Tauto.
Definition Rnormalise := @cnf_normalise Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool.
Definition Rnegate := @cnf_negate Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool.
Definition RTautoChecker (f : BFormula (Formula Z)) (w: list RWitness) : bool :=
@tauto_checker (Formula Z) (NFormula Z)
Rnormalise Rnegate
RWitness RWeakChecker f w.
Lemma RTautoChecker_sound : forall f w, RTautoChecker f w = true -> forall env, eval_f (Reval_formula env) f.