Library Coq.micromega.RMicromega


Require Import OrderedRing.
Require Import RingMicromega.
Require Import Refl.
Require Import Raxioms Rfunctions RIneq Rpow_def.
Require Import QArith.
Require Import Qfield.
Require Import Qreals.
Require Import DeclConstant.
Require Import Ztac.

Require Setoid.

Definition Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R).

Local Open Scope R_scope.

Lemma Rsor : SOR R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt.

Lemma Rinv_1 : forall x, x * / 1 = x.

Lemma Qeq_true : forall x y, Qeq_bool x y = true -> Q2R x = Q2R y.

Lemma Qeq_false : forall x y, Qeq_bool x y = false -> Q2R x <> Q2R y.

Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> Q2R x <= Q2R y.

Lemma Q2R_0 : Q2R 0 = 0.

Lemma Q2R_1 : Q2R 1 = 1.

Lemma Q2R_inv_ext : forall x,
  Q2R (/ x) = (if Qeq_bool x 0 then 0 else / Q2R x).

Notation to_nat := N.to_nat.

Lemma QSORaddon :
  @SORaddon R
  R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle
  Q 0%Q 1%Q Qplus Qmult Qminus Qopp
  Qeq_bool Qle_bool
  Q2R nat to_nat pow.


Inductive Rcst :=
  | C0
  | C1
  | CQ (r : Q)
  | CZ (r : Z)
  | CPlus (r1 r2 : Rcst)
  | CMinus (r1 r2 : Rcst)
  | CMult (r1 r2 : Rcst)
  | CPow (r1 : Rcst) (z:Z+nat)
  | CInv (r : Rcst)
  | COpp (r : Rcst).

Definition z_of_exp (z : Z + nat) :=
  match z with
  | inl z => z
  | inr n => Z.of_nat n
  end.

Fixpoint Q_of_Rcst (r : Rcst) : Q :=
  match r with
    | C0 => 0 # 1
    | C1 => 1 # 1
    | CZ z => z # 1
    | CQ q => q
    | CPlus r1 r2 => Qplus (Q_of_Rcst r1) (Q_of_Rcst r2)
    | CMinus r1 r2 => Qminus (Q_of_Rcst r1) (Q_of_Rcst r2)
    | CMult r1 r2 => Qmult (Q_of_Rcst r1) (Q_of_Rcst r2)
    | CPow r1 z => Qpower (Q_of_Rcst r1) (z_of_exp z)
    | CInv r => Qinv (Q_of_Rcst r)
    | COpp r => Qopp (Q_of_Rcst r)
  end.

Definition is_neg (z: Z+nat) :=
  match z with
  | inl (Zneg _) => true
  | _ => false
  end.

Lemma is_neg_true : forall z, is_neg z = true -> (z_of_exp z < 0)%Z.

Lemma is_neg_false : forall z, is_neg z = false -> (z_of_exp z >= 0)%Z.

Definition CInvR0 (r : Rcst) := Qeq_bool (Q_of_Rcst r) (0 # 1).

Definition CPowR0 (z : Z) (r : Rcst) :=
  Z.ltb z Z0 && Qeq_bool (Q_of_Rcst r) (0 # 1).

Fixpoint R_of_Rcst (r : Rcst) : R :=
  match r with
    | C0 => R0
    | C1 => R1
    | CZ z => IZR z
    | CQ q => Q2R q
    | CPlus r1 r2 => (R_of_Rcst r1) + (R_of_Rcst r2)
    | CMinus r1 r2 => (R_of_Rcst r1) - (R_of_Rcst r2)
    | CMult r1 r2 => (R_of_Rcst r1) * (R_of_Rcst r2)
    | CPow r1 z =>
      match z with
      | inl z =>
        if CPowR0 z r1
        then R0
        else powerRZ (R_of_Rcst r1) z
      | inr n => pow (R_of_Rcst r1) n
      end
    | CInv r =>
      if CInvR0 r then R0
      else Rinv (R_of_Rcst r)
    | COpp r => - (R_of_Rcst r)
  end.

Add Morphism Q2R with signature Qeq ==> @eq R as Q2R_m.
Qed.

Lemma Q2R_pow_pos : forall q p,
    Q2R (pow_pos Qmult q p) = pow_pos Rmult (Q2R q) p.

Lemma Q2R_pow_N : forall q n,
  Q2R (pow_N 1%Q Qmult q n) = pow_N 1 Rmult (Q2R q) n.

Lemma Qmult_integral : forall q r, q * r == 0 -> q == 0 \/ r == 0.

Lemma Qpower_positive_eq_zero : forall q p,
    Qpower_positive q p == 0 -> q == 0.

Lemma Qpower_positive_zero : forall p,
    Qpower_positive 0 p == 0%Q.

Lemma Q2RpowerRZ :
  forall q z
         (DEF : not (q == 0)%Q \/ (z >= Z0)%Z),
    Q2R (q ^ z) = powerRZ (Q2R q) z.

Lemma Qpower0 : forall z, (z <> 0)%Z -> (0 ^ z == 0)%Q.

Lemma Q_of_RcstR : forall c, Q2R (Q_of_Rcst c) = R_of_Rcst c.

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 R_of_Rcst N.to_nat 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 Rcst) :=
  let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs).

Definition Reval_formula' :=
  eval_sformula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt N.to_nat pow R_of_Rcst.

Definition QReval_formula :=
  eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R N.to_nat pow .

Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f.

Definition Qeval_nformula :=
  eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt Q2R.

Lemma Reval_nformula_dec : forall env d, (Qeval_nformula env d) \/ ~ (Qeval_nformula env d).

Definition RWitness := Psatz Q.

Definition RWeakChecker := check_normalised_formulas 0%Q 1%Q Qplus Qmult Qeq_bool Qle_bool.

Require Import List.

Lemma RWeakChecker_sound : forall (l : list (NFormula Q)) (cm : RWitness),
  RWeakChecker l cm = true ->
  forall env, make_impl (Qeval_nformula env) l False.

Require Import Coq.micromega.Tauto.

Definition Rnormalise := @cnf_normalise Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool Qle_bool.
Definition Rnegate := @cnf_negate Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool Qle_bool.

Definition runsat := check_inconsistent 0%Q Qeq_bool Qle_bool.

Definition rdeduce := nformula_plus_nformula 0%Q Qplus Qeq_bool.

Definition RTautoChecker (f : BFormula (Formula Rcst)) (w: list RWitness) : bool :=
  @tauto_checker (Formula Q) (NFormula Q)
  unit runsat rdeduce
  (Rnormalise unit) (Rnegate unit)
  RWitness (fun cl => RWeakChecker (List.map fst cl)) (map_bformula (map_Formula Q_of_Rcst) f) w.

Lemma RTautoChecker_sound : forall f w, RTautoChecker f w = true -> forall env, eval_bf (Reval_formula env) f.