Library Coq.micromega.RMicromega
Require Import OrderedRing.
Require Import RingMicromega.
Require Import Refl.
Require Import Raxioms RIneq Rpow_def DiscrR.
Require Import QArith.
Require Import Qfield.
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.
Definition IQR :=
fun x :
Q => (
IZR (
Qnum x)
* / IZR (
' Qden x))%
R.
Lemma Rinv_elim :
forall x y z,
y <> 0
-> (z * y = x <-> x * / y = z).
Ltac INR_nat_of_P :=
match goal with
|
H :
context[
INR (
Pos.to_nat ?
X)] |-
_ =>
revert H ;
let HH :=
fresh in
assert (
HH :=
pos_INR_nat_of_P X) ;
revert HH ;
generalize (
INR (
Pos.to_nat X))
| |-
context[
INR (
Pos.to_nat ?
X)] =>
let HH :=
fresh in
assert (
HH :=
pos_INR_nat_of_P X) ;
revert HH ;
generalize (
INR (
Pos.to_nat X))
end.
Ltac add_eq expr val :=
set (
temp :=
expr) ;
generalize (
eq_refl temp) ;
unfold temp at 1 ;
generalize temp ;
intro val ;
clear temp.
Ltac Rinv_elim :=
match goal with
| |-
context[?
x * / ?y] =>
let z :=
fresh "v"
in
add_eq (
x * / y)
z ;
let H :=
fresh in intro H ;
rewrite <-
Rinv_elim in H
end.
Lemma Rlt_neq :
forall r , 0
< r -> r <> 0.
Lemma Rinv_1 :
forall x,
x * / 1
= x.
Lemma Qeq_true :
forall x y,
Qeq_bool x y = true ->
IQR x = IQR y.
Lemma Qeq_false :
forall x y,
Qeq_bool x y = false -> IQR x <> IQR y.
Lemma Qle_true :
forall x y :
Q,
Qle_bool x y = true -> IQR x <= IQR y.
Lemma IQR_0 :
IQR 0
= 0.
Lemma IQR_1 :
IQR 1
= 1.
Lemma IQR_plus :
forall x y,
IQR (
x + y)
= IQR x + IQR y.
Lemma IQR_opp :
forall x,
IQR (
- x)
= - IQR x.
Lemma IQR_minus :
forall x y,
IQR (
x - y)
= IQR x - IQR y.
Lemma IQR_mult :
forall x y,
IQR (
x * y)
= IQR x * IQR y.
Lemma IQR_inv_lt :
forall x, (0
< x)%
Q ->
IQR (
/ x)
= / IQR x.
Lemma Qinv_opp :
forall x, (
- (/ x) = / ( -x))%
Q.
Lemma Qopp_involutive_strong :
forall x, (
- - x = x)%
Q.
Lemma Ropp_0 :
forall r ,
- r = 0
-> r = 0.
Lemma IQR_x_0 :
forall x,
IQR x = 0
-> x == 0%
Q.
Lemma IQR_inv_gt :
forall x, (0
> x)%
Q ->
IQR (
/ x)
= / IQR x.
Lemma IQR_inv :
forall x,
~ x == 0
->
IQR (
/ x)
= / IQR x.
Lemma IQR_inv_ext :
forall x,
IQR (
/ x)
= (if Qeq_bool x 0
then 0
else / IQR 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
IQR 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)
|
CInv (
r :
Rcst)
|
COpp (
r :
Rcst).
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)
|
CInv r =>
Qinv (
Q_of_Rcst r)
|
COpp r =>
Qopp (
Q_of_Rcst r)
end.
Fixpoint R_of_Rcst (
r :
Rcst) :
R :=
match r with
|
C0 =>
R0
|
C1 =>
R1
|
CZ z =>
IZR z
|
CQ q =>
IQR 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)
|
CInv r =>
if Qeq_bool (
Q_of_Rcst r) (0
# 1)
then R0
else Rinv (
R_of_Rcst r)
|
COpp r =>
- (R_of_Rcst r)
end.
Lemma Q_of_RcstR :
forall c,
IQR (
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 IQR 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 IQR.
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 Tauto.
Definition Rnormalise := @
cnf_normalise Q 0%
Q 1%
Q Qplus Qmult Qminus Qopp Qeq_bool.
Definition Rnegate := @
cnf_negate Q 0%
Q 1%
Q Qplus Qmult Qminus Qopp Qeq_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)
runsat rdeduce
Rnormalise Rnegate
RWitness RWeakChecker (
map_bformula (
map_Formula Q_of_Rcst)
f)
w.
Lemma RTautoChecker_sound :
forall f w,
RTautoChecker f w = true -> forall env,
eval_f (
Reval_formula env)
f.