fact: 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 | SplitProof p pf1 pf2 => match genCuttingPlane (p,NonStrict) , genCuttingPlane (popp p, NonStrict) with | None , _ | _ , None => false | Some cp1 , Some cp2 => ZChecker (nformula_of_cutting_plane cp1::l) pf1 && ZChecker (nformula_of_cutting_plane cp2::l) pf2 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.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory