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.