proposition: Lemma cutting_plane_sound : forall env f p, eval_nformula env f -> genCuttingPlane f = Some p -> eval_nformula env (nformula_of_cutting_plane p).
proof: Proof. unfold genCuttingPlane. intros env f; destruct f as [e op]. destruct op. - intros p; destruct p as [[e' z] op]. case_eq (Zgcd_pol e) ; intros g c. case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))) ; [discriminate|]. case_eq (makeCuttingPlane e). intros ? ? H H0 H1 H2 H3. inv H3. unfold makeCuttingPlane in H. rewrite H1 in H. revert H. change (eval_pol env e = 0) in H2. case_eq (Z.gtb g 0). + intros H H3. rewrite <- Zgt_is_gt_bool in H. rewrite Zgcd_pol_correct_lt with (1:= H1) in H2. 2: auto using Z.gt_lt. unfold nformula_of_cutting_plane. change (eval_pol env (padd e' (Pc z)) = 0). inv H3. rewrite eval_pol_add. set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub e c) g)) in *; clearbody x. simpl. rewrite andb_false_iff in H0. destruct H0 as [H0|H0]. * rewrite Zgt_is_gt_bool in H ; congruence. * rewrite andb_false_iff in H0. destruct H0 as [H0|H0]. -- rewrite negb_false_iff in H0. apply Zeq_bool_eq in H0. subst. simpl. rewrite Z.add_0_r, Z.mul_eq_0 in H2. intuition subst; easy. -- rewrite negb_false_iff in H0. apply Zeq_bool_eq in H0. assert (HH := Zgcd_is_gcd g c). rewrite H0 in HH. destruct HH as [H3 H4 ?]. apply Zdivide_opp_r in H4. rewrite Zdivide_ceiling ; auto. apply Z.sub_move_0_r. apply Z.div_unique_exact. ++ now intros ->. ++ now rewrite Z.add_move_0_r in H2. + intros H H3. unfold nformula_of_cutting_plane. inv H3. change (eval_pol env (padd e' (Pc 0)) = 0). rewrite eval_pol_add. simpl. now rewrite Z.add_0_r. - intros ? H H0. inv H0. unfold eval_nformula in *. unfold RingMicromega.eval_nformula in *. unfold nformula_of_cutting_plane. unfold eval_op1 in *. rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon). simpl. now rewrite Z.add_0_r. - intros p; destruct p as [[e' z] op]. case_eq (makeCuttingPlane (PsubC Z.sub e 1)). intros ? ? H H0 H1. inv H1. apply (makeCuttingPlane_ns_sound env) with (2:= H). simpl in *. rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). now apply Z.lt_le_pred. - intros p; destruct p as [[e' z] op]. case_eq (makeCuttingPlane e). intros ? ? H H0 H1. inv H1. apply (makeCuttingPlane_ns_sound env) with (2:= H). assumption. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat