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.