# Library Coq.micromega.ZMicromega

Require Import OrderedRing.
Require Import RingMicromega.
Require Import ZCoeff.
Require Import Refl.
Require Import ZArith.
Require Import List.
Require Import Bool.
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.
Require Import EnvRing.
Open Scope Z_scope.
Lemma Zsor : SOR 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt.
Lemma ZSORaddon :
SORaddon 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle
0%Z 1%Z Zplus Zmult Zminus Zopp
Zeq_bool Zle_bool
(fun x => x) (fun x => x) (pow_N 1 Zmult).
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 => Zpower (Zeval_expr env e1) (Z_of_N n)
| PEsub e1 e2 => (Zeval_expr env e1) - (Zeval_expr env e2)
| PEopp e => Zopp (Zeval_expr env e)
end.
Definition eval_expr := eval_pexpr Zplus Zmult Zminus Zopp (fun x => x) (fun x => x) (pow_N 1 Zmult).
Lemma ZNpower : forall r n, r ^ Z_of_N n = pow_N 1 Zmult 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 => Zle
| OpGe => Zge
| OpLt => Zlt
| OpGt => Zgt
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 Zplus Zmult Zminus Zopp (@eq Z) Zle Zlt (fun x => x) (fun x => x) (pow_N 1 Zmult).
Lemma Zeval_formula_compat : forall env f, Zeval_formula env f <-> Zeval_formula' env f.
Definition eval_nformula :=
eval_nformula 0 Zplus Zmult (@eq Z) Zle Zlt (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 Zplus Zmult Zeq_bool Zle_bool.
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 Zplus Zminus Zopp Zeq_bool.
Definition padd := padd Z0 Zplus Zeq_bool.
Definition norm := norm 0 1 Zplus Zmult Zminus Zopp Zeq_bool.
Definition eval_pol := eval_pol 0 Zplus Zmult (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_norm : forall env e, eval_expr env e = eval_pol env (norm e) .
Definition xnormalise (t:Formula Z) : list (NFormula Z) :=
let (lhs,o,rhs) := t in
let lhs := norm lhs in
let rhs := norm rhs in
match o with
| OpEq =>
((psub lhs (padd rhs (Pc 1))),NonStrict)::((psub rhs (padd lhs (Pc 1))),NonStrict)::nil
| OpNEq => (psub lhs rhs,Equal) :: nil
| OpGt => (psub rhs lhs,NonStrict) :: nil
| OpLt => (psub lhs rhs,NonStrict) :: nil
| OpGe => (psub rhs (padd lhs (Pc 1)),NonStrict) :: nil
| OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil
end.
Require Import Tauto.
Definition normalise (t:Formula Z) : cnf (NFormula Z) :=
List.map (fun x => x::nil) (xnormalise t).
Lemma normalise_correct : forall env t, eval_cnf (eval_nformula env) (normalise t) <-> Zeval_formula env t.
Opaque padd.
Transparent padd.
Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z) :=
let (lhs,o,rhs) := t in
let lhs := norm lhs in
let rhs := norm rhs in
match o with
| OpEq => (psub lhs rhs,Equal) :: nil
| OpNEq => ((psub lhs (padd rhs (Pc 1))),NonStrict)::((psub rhs (padd lhs (Pc 1))),NonStrict)::nil
| OpGt => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil
| OpLt => (psub rhs (padd lhs (Pc 1)),NonStrict) :: nil
| OpGe => (psub lhs rhs,NonStrict) :: nil
| OpLe => (psub rhs lhs,NonStrict) :: nil
end.
Definition negate (t:RingMicromega.Formula Z) : cnf (NFormula Z) :=
List.map (fun x => x::nil) (xnegate t).
Lemma negate_correct : forall env t, eval_cnf (eval_nformula env) (negate t) <-> ~ Zeval_formula env t.
Opaque padd.
Transparent padd.
Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool :=
@tauto_checker (Formula Z) (NFormula Z) normalise negate ZWitness ZWeakChecker f w.
Require Import Zdiv.
Open Scope Z_scope.
Definition ceiling (a b:Z) : Z :=
let (q,r) := Zdiv_eucl a b in
match r with
| Z0 => q
| _ => q + 1
end.
Lemma narrow_interval_lower_bound : forall 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 : Type :=
| DoneProof
| RatProof : ZWitness -> ZArithProof -> ZArithProof
| CutProof : ZWitness -> ZArithProof -> ZArithProof
| EnumProof : ZWitness -> ZWitness -> list 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) := Zmax (Zgcd 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 (Zdiv 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 ) -> (Zgcd a b | c).
Lemma Zdivide_pol_sub : forall p a b,
0 < Zgcd a b ->
Zdivide_pol a (PsubC Zminus p b) ->
Zdivide_pol (Zgcd a b) p.
Lemma Zdivide_pol_sub_0 : forall p a,
Zdivide_pol a (PsubC Zminus p 0) ->
Zdivide_pol a p.
Lemma Zgcd_pol_div : forall p g c,
Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Zminus 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 Zminus p c) g)) + c.
Definition makeCuttingPlane (p : PolC Z) : PolC Z * Z :=
let (g,c) := Zgcd_pol p in
if Zgt_bool g Z0
then (Zdiv_pol (PsubC Zminus p c) g , Zopp (ceiling (Zopp 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 (Zgt_bool g Z0) (andb (Zgt_bool c Z0) (negb (Zeq_bool (Zgcd g c) g)))
then None
else Some (e, Z0,op)
| NonEqual => Some (e,Z0,op)
| Strict => let (p,c) := makeCuttingPlane (PsubC Zminus 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 Zplus Zmult Zeq_bool Zle_bool.
Definition check_inconsistent := check_inconsistent 0 Zeq_bool Zle_bool.
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 check_inconsistent 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
| 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) =>
match op1 , op2 with
| NonStrict , NonStrict =>
if is_pol_Z0 (padd e1 e2)
then
(fix label (pfs:list ZArithProof) :=
fun lb ub =>
match pfs with
| nil => if Zgt_bool lb ub then true else false
| pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Zplus lb 1%Z) ub)
end)
pf (Zopp z1) z2
else false
| _ , _ => false
end
| _ , _ => false
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 => Max.max (bdepth pf) x) O l)
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_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 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) normalise negate ZArithProof ZChecker f w.
Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_f (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
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.Node Z.
Definition empty := @VarMap.Empty Z.
Definition leaf := @VarMap.Leaf Z.
Definition coneMember := ZWitness.
Definition eval := eval_formula.
Definition prod_pos_nat := prod positive nat.
Definition n_of_Z (z:Z) : BinNat.N :=
match z with
| Z0 => N0
| Zpos p => Npos p
| Zneg p => N0
end.