Library Coq.micromega.RMicromega
Require Import OrderedRing.
Require Import QMicromega RingMicromega.
Require Import Refl.
Require Import Sumbool Raxioms Rfunctions RIneq Rpow_def.
Require Import QArith.
Require Import Qfield.
Require Import Qreals.
Require Import DeclConstant.
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).
Register Rcst as micromega.Rcst.type.
Register C0 as micromega.Rcst.C0.
Register C1 as micromega.Rcst.C1.
Register CQ as micromega.Rcst.CQ.
Register CZ as micromega.Rcst.CZ.
Register CPlus as micromega.Rcst.CPlus.
Register CMinus as micromega.Rcst.CMinus.
Register CMult as micromega.Rcst.CMult.
Register CPow as micromega.Rcst.CPow.
Register CInv as micromega.Rcst.CInv.
Register COpp as micromega.Rcst.COpp.
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_pop2 (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 sumboolb {A B : Prop} (x : @sumbool A B) : bool :=
if x then true else false.
Definition Reval_bop2 (o : Op2) : R -> R -> bool :=
match o with
| OpEq => fun x y => sumboolb (Req_dec_T x y)
| OpNEq => fun x y => negb (sumboolb (Req_dec_T x y))
| OpLe => fun x y => (sumboolb (Rle_lt_dec x y))
| OpGe => fun x y => (sumboolb (Rge_gt_dec x y))
| OpLt => fun x y => (sumboolb (Rlt_le_dec x y))
| OpGt => fun x y => (sumboolb (Rgt_dec x y))
end.
Lemma pop2_bop2 :
forall (op : Op2) (r1 r2 : R), is_true (Reval_bop2 op r1 r2) <-> Reval_pop2 op r1 r2.
Definition Reval_op2 (k: Tauto.kind) : Op2 -> R -> R -> Tauto.rtyp k:=
if k as k0 return (Op2 -> R -> R -> Tauto.rtyp k0)
then Reval_pop2 else Reval_bop2.
Lemma Reval_op2_hold : forall b op q1 q2,
Tauto.hold b (Reval_op2 b op q1 q2) <-> Reval_pop2 op q1 q2.
Definition Reval_formula (e: PolEnv R) (k: Tauto.kind) (ff : Formula Rcst) :=
let (lhs,o,rhs) := ff in Reval_op2 k 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.
Lemma Reval_pop2_eval_op2 : forall o e1 e2,
Reval_pop2 o e1 e2 <->
eval_op2 eq Rle Rlt o e1 e2.
Lemma Reval_formula_compat : forall env b f, Tauto.hold b (Reval_formula env b f) <-> Reval_formula' env f.
Definition QReval_expr := eval_pexpr Rplus Rmult Rminus Ropp Q2R to_nat pow.
Definition QReval_formula (e: PolEnv R) (k: Tauto.kind) (ff : Formula Q) :=
let (lhs,o,rhs) := ff in Reval_op2 k o (QReval_expr e lhs) (QReval_expr e rhs).
Definition QReval_formula' :=
eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R N.to_nat pow.
Lemma QReval_formula_compat : forall env b f, Tauto.hold b (QReval_formula env b f) <-> QReval_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) Tauto.isProp) (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.