Library Coq.micromega.QMicromega
Require Import OrderedRing.
Require Import RingMicromega.
Require Import Refl.
Require Import QArith.
Require Import Qfield.
Lemma Qsor :
SOR 0 1
Qplus Qmult Qminus Qopp Qeq Qle Qlt.
Lemma QSORaddon :
SORaddon 0 1
Qplus Qmult Qminus Qopp Qeq Qle
0 1
Qplus Qmult Qminus Qopp
Qeq_bool Qle_bool
(
fun x =>
x) (
fun x =>
x) (
pow_N 1
Qmult).
Require Import EnvRing.
Fixpoint Qeval_expr (
env:
PolEnv Q) (
e:
PExpr Q) :
Q :=
match e with
|
PEc c =>
c
|
PEX j =>
env j
|
PEadd pe1 pe2 =>
(Qeval_expr env pe1) + (Qeval_expr env pe2)
|
PEsub pe1 pe2 =>
(Qeval_expr env pe1) - (Qeval_expr env pe2)
|
PEmul pe1 pe2 =>
(Qeval_expr env pe1) * (Qeval_expr env pe2)
|
PEopp pe1 =>
- (Qeval_expr env pe1)
|
PEpow pe1 n =>
Qpower (
Qeval_expr env pe1) (
Z.of_N n)
end.
Lemma Qeval_expr_simpl :
forall env e,
Qeval_expr env e =
match e with
|
PEc c =>
c
|
PEX j =>
env j
|
PEadd pe1 pe2 =>
(Qeval_expr env pe1) + (Qeval_expr env pe2)
|
PEsub pe1 pe2 =>
(Qeval_expr env pe1) - (Qeval_expr env pe2)
|
PEmul pe1 pe2 =>
(Qeval_expr env pe1) * (Qeval_expr env pe2)
|
PEopp pe1 =>
- (Qeval_expr env pe1)
|
PEpow pe1 n =>
Qpower (
Qeval_expr env pe1) (
Z.of_N n)
end.
Definition Qeval_expr' :=
eval_pexpr Qplus Qmult Qminus Qopp (
fun x =>
x) (
fun x =>
x) (
pow_N 1
Qmult).
Lemma QNpower :
forall r n,
r ^ Z.of_N n = pow_N 1
Qmult r n.
Lemma Qeval_expr_compat :
forall env e,
Qeval_expr env e = Qeval_expr' env e.
Definition Qeval_pop2 (
o :
Op2) :
Q -> Q -> Prop :=
match o with
|
OpEq =>
Qeq
|
OpNEq =>
fun x y =>
~ x == y
|
OpLe =>
Qle
|
OpGe =>
fun x y =>
Qle y x
|
OpLt =>
Qlt
|
OpGt =>
fun x y =>
Qlt y x
end.
Definition Qlt_bool (
x y :
Q) :=
(
Qnum x * QDen y <? Qnum y * QDen x)%
Z.
Definition Qeval_bop2 (
o :
Op2) :
Q -> Q -> bool :=
match o with
|
OpEq =>
Qeq_bool
|
OpNEq =>
fun x y =>
negb (
Qeq_bool x y)
|
OpLe =>
Qle_bool
|
OpGe =>
fun x y =>
Qle_bool y x
|
OpLt =>
Qlt_bool
|
OpGt =>
fun x y =>
Qlt_bool y x
end.
Lemma Qlt_bool_iff :
forall q1 q2,
Qlt_bool q1 q2 = true <-> q1 < q2.
Lemma pop2_bop2 :
forall (
op :
Op2) (
q1 q2 :
Q),
is_true (
Qeval_bop2 op q1 q2)
<-> Qeval_pop2 op q1 q2.
Definition Qeval_op2 (
k:
Tauto.kind) :
Op2 -> Q -> Q -> Tauto.rtyp k:=
if k as k0 return (
Op2 -> Q -> Q -> Tauto.rtyp k0)
then Qeval_pop2 else Qeval_bop2.
Lemma Qeval_op2_hold :
forall k op q1 q2,
Tauto.hold k (
Qeval_op2 k op q1 q2)
<-> Qeval_pop2 op q1 q2.
Definition Qeval_formula (
e:
PolEnv Q) (
k:
Tauto.kind) (
ff :
Formula Q) :=
let (
lhs,
o,
rhs) :=
ff in Qeval_op2 k o (
Qeval_expr e lhs) (
Qeval_expr e rhs).
Definition Qeval_formula' :=
eval_formula Qplus Qmult Qminus Qopp Qeq Qle Qlt (
fun x =>
x) (
fun x =>
x) (
pow_N 1
Qmult).
Lemma Qeval_formula_compat :
forall env b f,
Tauto.hold b (
Qeval_formula env b f)
<-> Qeval_formula' env f.
Definition Qeval_nformula :=
eval_nformula 0
Qplus Qmult Qeq Qle Qlt (
fun x =>
x) .
Definition Qeval_op1 (
o :
Op1) :
Q -> Prop :=
match o with
|
Equal =>
fun x :
Q =>
x == 0
|
NonEqual =>
fun x :
Q =>
~ x == 0
|
Strict =>
fun x :
Q => 0
< x
|
NonStrict =>
fun x :
Q => 0
<= x
end.
Lemma Qeval_nformula_dec :
forall env d,
(Qeval_nformula env d) \/ ~ (Qeval_nformula env d).
Definition QWitness :=
Psatz Q.
Register QWitness as micromega.QWitness.type.
Definition QWeakChecker :=
check_normalised_formulas 0 1
Qplus Qmult Qeq_bool Qle_bool.
Require Import List.
Lemma QWeakChecker_sound :
forall (
l :
list (
NFormula Q)) (
cm :
QWitness),
QWeakChecker l cm = true ->
forall env,
make_impl (
Qeval_nformula env)
l False.
Require Import Coq.micromega.Tauto.
Definition Qnormalise := @
cnf_normalise Q 0 1
Qplus Qmult Qminus Qopp Qeq_bool Qle_bool.
Definition Qnegate := @
cnf_negate Q 0 1
Qplus Qmult Qminus Qopp Qeq_bool Qle_bool.
Definition qunsat :=
check_inconsistent 0
Qeq_bool Qle_bool.
Definition qdeduce :=
nformula_plus_nformula 0
Qplus Qeq_bool.
Definition normQ :=
norm 0 1
Qplus Qmult Qminus Qopp Qeq_bool.
Definition cnfQ (
Annot:
Type) (
TX:
Tauto.kind -> Type) (
AF:
Type) (
k:
Tauto.kind) (
f:
TFormula (
Formula Q)
Annot TX AF k) :=
rxcnf qunsat qdeduce (
Qnormalise Annot) (
Qnegate Annot)
true f.
Definition QTautoChecker (
f :
BFormula (
Formula Q)
Tauto.isProp) (
w:
list QWitness) :
bool :=
@
tauto_checker (
Formula Q) (
NFormula Q)
unit
qunsat qdeduce
(
Qnormalise unit)
(
Qnegate unit)
QWitness (
fun cl =>
QWeakChecker (
List.map fst cl))
f w.
Lemma QTautoChecker_sound :
forall f w,
QTautoChecker f w = true -> forall env,
eval_bf (
Qeval_formula env)
f.