Library Coq.micromega.ZMicromega
Require Import List.
Require Import Bool.
Require Import OrderedRing.
Require Import RingMicromega.
Require Import ZCoeff.
Require Import Refl.
Require Import ZArith_base.
Require Import ZArithRing.
Require Import Ztac.
Require PreOmega.
Local Open Scope Z_scope.
Ltac flatten_bool :=
repeat match goal with
[
id : (
_ && _)%
bool = true |-
_ ] =>
destruct (
andb_prop _ _ id);
clear id
| [
id : (
_ || _)%
bool = true |-
_ ] =>
destruct (
orb_prop _ _ id);
clear id
end.
Ltac inv H :=
inversion H ;
try subst ;
clear H.
Lemma eq_le_iff :
forall x, 0
= x <-> (0
<= x /\ x <= 0
).
Lemma lt_le_iff :
forall x,
0
< x <-> 0
<= x - 1.
Lemma le_0_iff :
forall x y,
x <= y <-> 0
<= y - x.
Lemma le_neg :
forall x,
((0
<= x) -> False) <-> 0
< -x.
Lemma eq_cnf :
forall x,
(0
<= x - 1
-> False) /\ (0
<= -1
- x -> False) <-> x = 0.
Require Import EnvRing.
Lemma Zsor :
SOR 0 1
Z.add Z.mul Z.sub Z.opp (@
eq Z)
Z.le Z.lt.
Lemma ZSORaddon :
SORaddon 0 1
Z.add Z.mul Z.sub Z.opp (@
eq Z)
Z.le
0%
Z 1%
Z Z.add Z.mul Z.sub Z.opp
Zeq_bool Z.leb
(
fun x =>
x) (
fun x =>
x) (
pow_N 1
Z.mul).
Fixpoint Zeval_expr (
env :
PolEnv Z) (
e:
PExpr Z) :
Z :=
match e with
|
PEc c =>
c
|
PEX x =>
env x
|
PEadd e1 e2 =>
Zeval_expr env e1 + Zeval_expr env e2
|
PEmul e1 e2 =>
Zeval_expr env e1 * Zeval_expr env e2
|
PEpow e1 n =>
Z.pow (
Zeval_expr env e1) (
Z.of_N n)
|
PEsub e1 e2 =>
(Zeval_expr env e1) - (Zeval_expr env e2)
|
PEopp e =>
Z.opp (
Zeval_expr env e)
end.
Definition eval_expr :=
eval_pexpr Z.add Z.mul Z.sub Z.opp (
fun x =>
x) (
fun x =>
x) (
pow_N 1
Z.mul).
Fixpoint Zeval_const (
e:
PExpr Z) :
option Z :=
match e with
|
PEc c =>
Some c
|
PEX x =>
None
|
PEadd e1 e2 =>
map_option2 (
fun x y =>
Some (
x + y))
(
Zeval_const e1) (
Zeval_const e2)
|
PEmul e1 e2 =>
map_option2 (
fun x y =>
Some (
x * y))
(
Zeval_const e1) (
Zeval_const e2)
|
PEpow e1 n =>
map_option (
fun x =>
Some (
Z.pow x (
Z.of_N n)))
(
Zeval_const e1)
|
PEsub e1 e2 =>
map_option2 (
fun x y =>
Some (
x - y))
(
Zeval_const e1) (
Zeval_const e2)
|
PEopp e =>
map_option (
fun x =>
Some (
Z.opp x)) (
Zeval_const e)
end.
Lemma ZNpower :
forall r n,
r ^ Z.of_N n = pow_N 1
Z.mul r n.
Lemma Zeval_expr_compat :
forall env e,
Zeval_expr env e = eval_expr env e.
Definition Zeval_op2 (
o :
Op2) :
Z -> Z -> Prop :=
match o with
|
OpEq => @
eq Z
|
OpNEq =>
fun x y =>
~ x = y
|
OpLe =>
Z.le
|
OpGe =>
Z.ge
|
OpLt =>
Z.lt
|
OpGt =>
Z.gt
end.
Definition Zeval_formula (
env :
PolEnv Z) (
f :
Formula Z):=
let (
lhs,
op,
rhs) :=
f in
(
Zeval_op2 op) (
Zeval_expr env lhs) (
Zeval_expr env rhs).
Definition Zeval_formula' :=
eval_formula Z.add Z.mul Z.sub Z.opp (@
eq Z)
Z.le Z.lt (
fun x =>
x) (
fun x =>
x) (
pow_N 1
Z.mul).
Lemma Zeval_formula_compat' :
forall env f,
Zeval_formula env f <-> Zeval_formula' env f.
Definition eval_nformula :=
eval_nformula 0
Z.add Z.mul (@
eq Z)
Z.le Z.lt (
fun x =>
x) .
Definition Zeval_op1 (
o :
Op1) :
Z -> Prop :=
match o with
|
Equal =>
fun x :
Z =>
x = 0
|
NonEqual =>
fun x :
Z =>
x <> 0
|
Strict =>
fun x :
Z => 0
< x
|
NonStrict =>
fun x :
Z => 0
<= x
end.
Lemma Zeval_nformula_dec :
forall env d,
(eval_nformula env d) \/ ~ (eval_nformula env d).
Definition ZWitness :=
Psatz Z.
Definition ZWeakChecker :=
check_normalised_formulas 0 1
Z.add Z.mul Zeq_bool Z.leb.
Lemma ZWeakChecker_sound :
forall (
l :
list (
NFormula Z)) (
cm :
ZWitness),
ZWeakChecker l cm = true ->
forall env,
make_impl (
eval_nformula env)
l False.
Definition psub :=
psub Z0 Z.add Z.sub Z.opp Zeq_bool.
Definition padd :=
padd Z0 Z.add Zeq_bool.
Definition pmul :=
pmul 0 1
Z.add Z.mul Zeq_bool.
Definition normZ :=
norm 0 1
Z.add Z.mul Z.sub Z.opp Zeq_bool.
Definition eval_pol :=
eval_pol Z.add Z.mul (
fun x =>
x).
Lemma eval_pol_sub :
forall env lhs rhs,
eval_pol env (
psub lhs rhs)
= eval_pol env lhs - eval_pol env rhs.
Lemma eval_pol_add :
forall env lhs rhs,
eval_pol env (
padd lhs rhs)
= eval_pol env lhs + eval_pol env rhs.
Lemma eval_pol_mul :
forall env lhs rhs,
eval_pol env (
pmul lhs rhs)
= eval_pol env lhs * eval_pol env rhs.
Lemma eval_pol_norm :
forall env e,
eval_expr env e = eval_pol env (
normZ e) .
Definition Zunsat :=
check_inconsistent 0
Zeq_bool Z.leb.
Definition Zdeduce :=
nformula_plus_nformula 0
Z.add Zeq_bool.
Lemma Zunsat_sound :
forall f,
Zunsat f = true -> forall env,
eval_nformula env f -> False.
Definition xnnormalise (
t :
Formula Z) :
NFormula Z :=
let (
lhs,
o,
rhs) :=
t in
let lhs :=
normZ lhs in
let rhs :=
normZ rhs in
match o with
|
OpEq =>
(psub rhs lhs, Equal)
|
OpNEq =>
(psub rhs lhs, NonEqual)
|
OpGt =>
(psub lhs rhs, Strict)
|
OpLt =>
(psub rhs lhs, Strict)
|
OpGe =>
(psub lhs rhs, NonStrict)
|
OpLe =>
(psub rhs lhs, NonStrict)
end.
Lemma xnnormalise_correct :
forall env f,
eval_nformula env (
xnnormalise f)
<-> Zeval_formula env f.
Definition xnormalise (
f:
NFormula Z) :
list (
NFormula Z) :=
let (
e,
o) :=
f in
match o with
|
Equal =>
(psub e (
Pc 1)
,NonStrict) :: (psub (
Pc (-1))
e, NonStrict) :: nil
|
NonStrict => (
(psub (
Pc (-1))
e,NonStrict)::nil)
|
Strict =>
((
psub (
Pc 0))
e, NonStrict)::nil
|
NonEqual =>
(e, Equal)::nil
end.
Lemma eval_pol_Pc :
forall env z,
eval_pol env (
Pc z)
= z.
Ltac iff_ring :=
match goal with
| |- ?
F 0 ?
X <-> ?
F 0 ?
Y =>
replace X with Y by ring ;
tauto
end.
Lemma xnormalise_correct :
forall env f,
(make_conj (
fun x =>
eval_nformula env x -> False) (
xnormalise f)
) <-> eval_nformula env f.
Require Import Coq.micromega.Tauto BinNums.
Definition cnf_of_list {
T:
Type} (
tg :
T) (
l :
list (
NFormula Z)) :=
List.fold_right (
fun x acc =>
if Zunsat x then acc else ((x,tg)::nil)::acc)
(
cnf_tt _ _)
l.
Lemma cnf_of_list_correct :
forall {
T :
Type} (
tg:
T) (
f :
list (
NFormula Z))
env,
eval_cnf eval_nformula env (
cnf_of_list tg f)
<->
make_conj (
fun x :
NFormula Z =>
eval_nformula env x -> False)
f.
Definition normalise {
T :
Type} (
t:
Formula Z) (
tg:
T) :
cnf (
NFormula Z)
T :=
let f :=
xnnormalise t in
if Zunsat f then cnf_ff _ _
else cnf_of_list tg (
xnormalise f).
Lemma normalise_correct :
forall (
T:
Type)
env t (
tg:
T),
eval_cnf eval_nformula env (
normalise t tg)
<-> Zeval_formula env t.
Definition xnegate (
f:
NFormula Z) :
list (
NFormula Z) :=
let (
e,
o) :=
f in
match o with
|
Equal =>
(e,Equal) :: nil
|
NonEqual =>
(psub e (
Pc 1)
,NonStrict) :: (psub (
Pc (-1))
e, NonStrict) :: nil
|
NonStrict =>
(e,NonStrict)::nil
|
Strict =>
(psub e (
Pc 1)
,NonStrict)::nil
end.
Definition negate {
T :
Type} (
t:
Formula Z) (
tg:
T) :
cnf (
NFormula Z)
T :=
let f :=
xnnormalise t in
if Zunsat f then cnf_tt _ _
else cnf_of_list tg (
xnegate f).
Lemma xnegate_correct :
forall env f,
(make_conj (
fun x =>
eval_nformula env x -> False) (
xnegate f)
) <-> ~ eval_nformula env f.
Lemma negate_correct :
forall T env t (
tg:
T),
eval_cnf eval_nformula env (
negate t tg)
<-> ~ Zeval_formula env t.
Definition cnfZ (
Annot:
Type) (
TX :
Type) (
AF :
Type) (
f :
TFormula (
Formula Z)
Annot TX AF) :=
rxcnf Zunsat Zdeduce normalise negate true f.
Definition ZweakTautoChecker (
w:
list ZWitness) (
f :
BFormula (
Formula Z)) :
bool :=
@
tauto_checker (
Formula Z) (
NFormula Z)
unit Zunsat Zdeduce normalise negate ZWitness (
fun cl =>
ZWeakChecker (
List.map fst cl))
f w.
Require Import Zdiv.
Local Open Scope Z_scope.
Definition ceiling (
a b:
Z) :
Z :=
let (
q,
r) :=
Z.div_eucl a b in
match r with
|
Z0 =>
q
|
_ =>
q + 1
end.
Require Import Znumtheory.
Lemma Zdivide_ceiling :
forall a b,
(b | a) -> ceiling a b = Z.div a b.
Lemma narrow_interval_lower_bound a b x :
a > 0
-> a * x >= b -> x >= ceiling b a.
NB: narrow_interval_upper_bound is Zdiv.Zdiv_le_lower_bound
Require Import QArith.
Inductive ZArithProof :=
|
DoneProof
|
RatProof :
ZWitness -> ZArithProof -> ZArithProof
|
CutProof :
ZWitness -> ZArithProof -> ZArithProof
|
EnumProof :
ZWitness -> ZWitness -> list ZArithProof -> ZArithProof
|
ExProof :
positive -> ZArithProof -> ZArithProof
.
Require Import Znumtheory.
Definition isZ0 (
x:
Z) :=
match x with
|
Z0 =>
true
|
_ =>
false
end.
Lemma isZ0_0 :
forall x,
isZ0 x = true <-> x = 0.
Lemma isZ0_n0 :
forall x,
isZ0 x = false <-> x <> 0.
Definition ZgcdM (
x y :
Z) :=
Z.max (
Z.gcd x y) 1.
Fixpoint Zgcd_pol (
p :
PolC Z) : (
Z * Z) :=
match p with
|
Pc c =>
(0
,c)
|
Pinj _ p =>
Zgcd_pol p
|
PX p _ q =>
let (
g1,
c1) :=
Zgcd_pol p in
let (
g2,
c2) :=
Zgcd_pol q in
(ZgcdM (
ZgcdM g1 c1)
g2 , c2)
end.
Fixpoint Zdiv_pol (
p:
PolC Z) (
x:
Z) :
PolC Z :=
match p with
|
Pc c =>
Pc (
Z.div c x)
|
Pinj j p =>
Pinj j (
Zdiv_pol p x)
|
PX p j q =>
PX (
Zdiv_pol p x)
j (
Zdiv_pol q x)
end.
Inductive Zdivide_pol (
x:
Z):
PolC Z -> Prop :=
|
Zdiv_Pc :
forall c,
(x | c) -> Zdivide_pol x (
Pc c)
|
Zdiv_Pinj :
forall p,
Zdivide_pol x p -> forall j,
Zdivide_pol x (
Pinj j p)
|
Zdiv_PX :
forall p q,
Zdivide_pol x p -> Zdivide_pol x q -> forall j,
Zdivide_pol x (
PX p j q).
Lemma Zdiv_pol_correct :
forall a p, 0
< a -> Zdivide_pol a p ->
forall env,
eval_pol env p = a * eval_pol env (
Zdiv_pol p a).
Lemma Zgcd_pol_ge :
forall p,
fst (
Zgcd_pol p)
>= 0.
Lemma Zdivide_pol_Zdivide :
forall p x y,
Zdivide_pol x p -> (y | x) -> Zdivide_pol y p.
Lemma Zdivide_pol_one :
forall p,
Zdivide_pol 1
p.
Lemma Zgcd_minus :
forall a b c,
(a | c - b ) -> (Z.gcd a b | c).
Lemma Zdivide_pol_sub :
forall p a b,
0
< Z.gcd a b ->
Zdivide_pol a (
PsubC Z.sub p b)
->
Zdivide_pol (
Z.gcd a b)
p.
Lemma Zdivide_pol_sub_0 :
forall p a,
Zdivide_pol a (
PsubC Z.sub p 0)
->
Zdivide_pol a p.
Lemma Zgcd_pol_div :
forall p g c,
Zgcd_pol p = (g, c) -> Zdivide_pol g (
PsubC Z.sub p c).
Lemma Zgcd_pol_correct_lt :
forall p env g c,
Zgcd_pol p = (g,c) -> 0
< g -> eval_pol env p = g * (eval_pol env (
Zdiv_pol (
PsubC Z.sub p c)
g)
) + c.
Definition makeCuttingPlane (
p :
PolC Z) :
PolC Z * Z :=
let (
g,
c) :=
Zgcd_pol p in
if Z.gtb g Z0
then (Zdiv_pol (
PsubC Z.sub p c)
g , Z.opp (
ceiling (
Z.opp c)
g)
)
else (p,Z0).
Definition genCuttingPlane (
f :
NFormula Z) :
option (
PolC Z * Z * Op1) :=
let (
e,
op) :=
f in
match op with
|
Equal =>
let (
g,
c) :=
Zgcd_pol e in
if andb (
Z.gtb g Z0) (
andb (
negb (
Zeq_bool c Z0)) (
negb (
Zeq_bool (
Z.gcd g c)
g)))
then None
else
let (
p,
c) :=
makeCuttingPlane e in
Some (p,c,Equal)
|
NonEqual =>
Some (e,Z0,op)
|
Strict =>
let (
p,
c) :=
makeCuttingPlane (
PsubC Z.sub e 1)
in
Some (p,c,NonStrict)
|
NonStrict =>
let (
p,
c) :=
makeCuttingPlane e in
Some (p,c,NonStrict)
end.
Definition nformula_of_cutting_plane (
t :
PolC Z * Z * Op1) :
NFormula Z :=
let (
e_z,
o) :=
t in
let (
e,
z) :=
e_z in
(padd e (
Pc z)
, o).
Definition is_pol_Z0 (
p :
PolC Z) :
bool :=
match p with
|
Pc Z0 =>
true
|
_ =>
false
end.
Lemma is_pol_Z0_eval_pol :
forall p,
is_pol_Z0 p = true -> forall env,
eval_pol env p = 0.
Definition eval_Psatz :
list (
NFormula Z)
-> ZWitness -> option (
NFormula Z) :=
eval_Psatz 0 1
Z.add Z.mul Zeq_bool Z.leb.
Definition valid_cut_sign (
op:
Op1) :=
match op with
|
Equal =>
true
|
NonStrict =>
true
|
_ =>
false
end.
Definition bound_var (
v :
positive) :
Formula Z :=
Build_Formula (
PEX v)
OpGe (
PEc 0).
Definition mk_eq_pos (
x :
positive) (
y:
positive) (
t :
positive) :
Formula Z :=
Build_Formula (
PEX x)
OpEq (
PEsub (
PEX y) (
PEX t)).
Fixpoint vars (
jmp :
positive) (
p :
Pol Z) :
list positive :=
match p with
|
Pc c =>
nil
|
Pinj j p =>
vars (
Pos.add j jmp)
p
|
PX p j q =>
jmp::(vars jmp p)++vars (
Pos.succ jmp)
q
end.
Fixpoint max_var (
jmp :
positive) (
p :
Pol Z) :
positive :=
match p with
|
Pc _ =>
jmp
|
Pinj j p =>
max_var (
Pos.add j jmp)
p
|
PX p j q =>
Pos.max (
max_var jmp p) (
max_var (
Pos.succ jmp)
q)
end.
Lemma pos_le_add :
forall y x,
(
x <= y + x)%
positive.
Lemma max_var_le :
forall p v,
(
v <= max_var v p)%
positive.
Lemma max_var_correct :
forall p j v,
In v (
vars j p)
-> Pos.le v (
max_var j p).
Definition max_var_nformulae (
l :
list (
NFormula Z)) :=
List.fold_left (
fun acc f =>
Pos.max acc (
max_var xH (
fst f)))
l xH.
Section MaxVar.
Definition F (
acc :
positive) (
f :
Pol Z * Op1) :=
Pos.max acc (
max_var 1 (
fst f)).
Lemma max_var_nformulae_mono_aux :
forall l v acc,
(
v <= acc ->
v <= fold_left F l acc)%
positive.
Lemma max_var_nformulae_mono_aux' :
forall l acc acc',
(
acc <= acc' ->
fold_left F l acc <= fold_left F l acc')%
positive.
Lemma max_var_nformulae_correct_aux :
forall l p o v,
In (p,o) l -> In v (
vars xH p)
-> Pos.le v (
fold_left F l 1)%
positive.
End MaxVar.
Lemma max_var_nformalae_correct :
forall l p o v,
In (p,o) l -> In v (
vars xH p)
-> Pos.le v (
max_var_nformulae l)%
positive.
Fixpoint max_var_psatz (
w :
Psatz Z) :
positive :=
match w with
|
PsatzIn _ n =>
xH
|
PsatzSquare p =>
max_var xH (
Psquare 0 1
Z.add Z.mul Zeq_bool p)
|
PsatzMulC p w =>
Pos.max (
max_var xH p) (
max_var_psatz w)
|
PsatzMulE w1 w2 =>
Pos.max (
max_var_psatz w1) (
max_var_psatz w2)
|
PsatzAdd w1 w2 =>
Pos.max (
max_var_psatz w1) (
max_var_psatz w2)
|
_ =>
xH
end.
Fixpoint max_var_prf (
w :
ZArithProof) :
positive :=
match w with
|
DoneProof =>
xH
|
RatProof w pf |
CutProof w pf =>
Pos.max (
max_var_psatz w) (
max_var_prf pf)
|
EnumProof w1 w2 l =>
List.fold_left (
fun acc prf =>
Pos.max acc (
max_var_prf prf))
l
(
Pos.max (
max_var_psatz w1) (
max_var_psatz w2))
|
ExProof _ pf =>
max_var_prf pf
end.
Fixpoint ZChecker (
l:
list (
NFormula Z)) (
pf :
ZArithProof) {
struct pf} :
bool :=
match pf with
|
DoneProof =>
false
|
RatProof w pf =>
match eval_Psatz l w with
|
None =>
false
|
Some f =>
if Zunsat f then true
else ZChecker (
f::l)
pf
end
|
CutProof w pf =>
match eval_Psatz l w with
|
None =>
false
|
Some f =>
match genCuttingPlane f with
|
None =>
true
|
Some cp =>
ZChecker (
nformula_of_cutting_plane cp::l)
pf
end
end
|
ExProof x prf =>
let fr :=
max_var_nformulae l in
if Pos.leb x fr then
let z :=
Pos.succ fr in
let t :=
Pos.succ z in
let nfx :=
xnnormalise (
mk_eq_pos x z t)
in
let posz :=
xnnormalise (
bound_var z)
in
let post :=
xnnormalise (
bound_var t)
in
ZChecker (
nfx::posz::post::l)
prf
else false
|
EnumProof w1 w2 pf =>
match eval_Psatz l w1 ,
eval_Psatz l w2 with
|
Some f1 ,
Some f2 =>
match genCuttingPlane f1 ,
genCuttingPlane f2 with
|
Some (e1,z1,op1) ,
Some (e2,z2,op2) =>
if (
valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (
padd e1 e2))
then
(
fix label (
pfs:
list ZArithProof) :=
fun lb ub =>
match pfs with
|
nil =>
if Z.gtb lb ub then true else false
|
pf::rsr =>
andb (
ZChecker (
(psub e1 (
Pc lb)
, Equal) :: l)
pf) (
label rsr (
Z.add lb 1%
Z)
ub)
end)
pf (
Z.opp z1)
z2
else false
|
_ ,
_ =>
true
end
|
_ ,
_ =>
false
end
end.
Fixpoint bdepth (
pf :
ZArithProof) :
nat :=
match pf with
|
DoneProof =>
O
|
RatProof _ p =>
S (
bdepth p)
|
CutProof _ p =>
S (
bdepth p)
|
EnumProof _ _ l =>
S (
List.fold_right (
fun pf x =>
Nat.max (
bdepth pf)
x)
O l)
|
ExProof _ p =>
S (
bdepth p)
end.
Require Import Wf_nat.
Lemma in_bdepth :
forall l a b y,
In y l -> ltof ZArithProof bdepth y (
EnumProof a b l).
Lemma eval_Psatz_sound :
forall env w l f',
make_conj (
eval_nformula env)
l ->
eval_Psatz l w = Some f' -> eval_nformula env f'.
Lemma makeCuttingPlane_ns_sound :
forall env e e' c,
eval_nformula env (e, NonStrict) ->
makeCuttingPlane e = (e',c) ->
eval_nformula env (
nformula_of_cutting_plane (e', c, NonStrict)).
Lemma cutting_plane_sound :
forall env f p,
eval_nformula env f ->
genCuttingPlane f = Some p ->
eval_nformula env (
nformula_of_cutting_plane p).
Lemma genCuttingPlaneNone :
forall env f,
genCuttingPlane f = None ->
eval_nformula env f -> False.
Lemma eval_nformula_mk_eq_pos :
forall env x z t,
env x = env z - env t ->
eval_nformula env (
xnnormalise (
mk_eq_pos x z t)).
Lemma eval_nformula_bound_var :
forall env x,
env x >= 0
->
eval_nformula env (
xnnormalise (
bound_var x)).
Definition agree_env (
fr :
positive) (
env env' :
positive -> Z) :
Prop :=
forall x,
Pos.le x fr -> env x = env' x.
Lemma agree_env_subset :
forall v1 v2 env env',
agree_env v1 env env' ->
Pos.le v2 v1 ->
agree_env v2 env env'.
Lemma agree_env_jump :
forall fr j env env',
agree_env (
fr + j)
env env' ->
agree_env fr (
Env.jump j env) (
Env.jump j env').
Lemma agree_env_tail :
forall fr env env',
agree_env (
Pos.succ fr)
env env' ->
agree_env fr (
Env.tail env) (
Env.tail env').
Lemma max_var_acc :
forall p i j,
(
max_var (
i + j)
p = max_var i p + j)%
positive.
Lemma agree_env_eval_nformula :
forall env env' e
(
AGREE :
agree_env (
max_var xH (
fst e))
env env'),
eval_nformula env e <-> eval_nformula env' e.
Lemma agree_env_eval_nformulae :
forall env env' l
(
AGREE :
agree_env (
max_var_nformulae l)
env env'),
make_conj (
eval_nformula env)
l <->
make_conj (
eval_nformula env')
l.
Lemma eq_true_iff_eq :
forall b1 b2 :
bool,
(b1 = true <-> b2 = true) <-> b1 = b2.
Ltac pos_tac :=
repeat
match goal with
| |-
false = _ =>
symmetry
| |-
Pos.eqb ?
X ?
Y = false =>
rewrite Pos.eqb_neq ;
intro
|
H : @
eq positive ?
X ?
Y |-
_ =>
apply Zpos_eq in H
|
H :
context[
Z.pos (
Pos.succ ?
X)] |-
_ =>
rewrite (
Pos2Z.inj_succ X)
in H
|
H :
Pos.leb ?
X ?
Y = true |-
_ =>
rewrite Pos.leb_le in H ;
apply (
Pos2Z.pos_le_pos X Y)
in H
end.
Lemma ZChecker_sound :
forall w l,
ZChecker l w = true -> forall env,
make_impl (
eval_nformula env)
l False.
Definition ZTautoChecker (
f :
BFormula (
Formula Z)) (
w:
list ZArithProof):
bool :=
@
tauto_checker (
Formula Z) (
NFormula Z)
unit Zunsat Zdeduce normalise negate ZArithProof (
fun cl =>
ZChecker (
List.map fst cl))
f w.
Lemma ZTautoChecker_sound :
forall f w,
ZTautoChecker f w = true -> forall env,
eval_bf (
Zeval_formula env)
f.
Fixpoint xhyps_of_pt (
base:
nat) (
acc :
list nat) (
pt:
ZArithProof) :
list nat :=
match pt with
|
DoneProof =>
acc
|
RatProof c pt =>
xhyps_of_pt (
S base ) (
xhyps_of_psatz base acc c)
pt
|
CutProof c pt =>
xhyps_of_pt (
S base ) (
xhyps_of_psatz base acc c)
pt
|
EnumProof c1 c2 l =>
let acc :=
xhyps_of_psatz base (
xhyps_of_psatz base acc c2)
c1 in
List.fold_left (
xhyps_of_pt (
S base))
l acc
|
ExProof _ pt =>
xhyps_of_pt (
S (
S (
S base )))
acc pt
end.
Definition hyps_of_pt (
pt :
ZArithProof) :
list nat :=
xhyps_of_pt 0
nil pt.
Open Scope Z_scope.
To ease bindings from ml code