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_pop2 (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_bop2 (o : Op2) : Z -> Z -> bool :=
match o with
| OpEq => Z.eqb
| OpNEq => fun x y => negb (Z.eqb x y)
| OpLe => Z.leb
| OpGe => Z.geb
| OpLt => Z.ltb
| OpGt => Z.gtb
end.
Lemma pop2_bop2 :
forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2.
Definition Zeval_op2 (k: Tauto.kind) : Op2 -> Z -> Z -> Tauto.rtyp k:=
if k as k0 return (Op2 -> Z -> Z -> Tauto.rtyp k0)
then Zeval_pop2 else Zeval_bop2.
Lemma Zeval_op2_hold : forall k op q1 q2,
Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2.
Definition Zeval_formula (env : PolEnv Z) (k: Tauto.kind) (f : Formula Z):=
let (lhs, op, rhs) := f in
(Zeval_op2 k 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 k f, Tauto.hold k (Zeval_formula env k f) <-> Zeval_formula env Tauto.isProp f.
Lemma Zeval_formula_compat' : forall env f, Zeval_formula env Tauto.isProp 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 Tauto.isProp 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 Tauto.isProp 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 Tauto.isProp t.
Definition cnfZ (Annot: Type) (TX : Tauto.kind -> Type) (AF : Type) (k: Tauto.kind) (f : TFormula (Formula Z) Annot TX AF k) :=
rxcnf Zunsat Zdeduce normalise negate true f.
Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z) Tauto.isProp) : 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) Tauto.isProp) (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
Definition make_impl := Refl.make_impl.
Definition make_conj := Refl.make_conj.
Require VarMap.
Definition env := PolEnv Z.
Definition node := @VarMap.Branch Z.
Definition empty := @VarMap.Empty Z.
Definition leaf := @VarMap.Elt Z.
Definition coneMember := ZWitness.
Definition eval := eval_formula.
Definition prod_pos_nat := prod positive nat.
Notation n_of_Z := Z.to_N (only parsing).
Definition make_conj := Refl.make_conj.
Require VarMap.
Definition env := PolEnv Z.
Definition node := @VarMap.Branch Z.
Definition empty := @VarMap.Empty Z.
Definition leaf := @VarMap.Elt Z.
Definition coneMember := ZWitness.
Definition eval := eval_formula.
Definition prod_pos_nat := prod positive nat.
Notation n_of_Z := Z.to_N (only parsing).