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
.