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_op2 (
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 Qeval_formula (
e:
PolEnv Q) (
ff :
Formula Q) :=
let (
lhs,
o,
rhs) :=
ff in Qeval_op2 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 f,
Qeval_formula env 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.
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 TX AF:
Type) (
f:
TFormula (
Formula Q)
Annot TX AF) :=
rxcnf qunsat qdeduce (
Qnormalise Annot) (
Qnegate Annot)
true f.
Definition QTautoChecker (
f :
BFormula (
Formula Q)) (
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.