proposition: Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl (eval_nformula env) l False.
proof: Proof. intros w; induction w as [w H] using (well_founded_ind (well_founded_ltof _ bdepth)). destruct w as [ | w pf | w pf | p pf1 pf2 | w1 w2 pf | x pf]. - simpl. discriminate. - simpl. intros l. case_eq (eval_Psatz l w) ; [| discriminate]. intros f Hf. case_eq (Zunsat f). + intros H0 ? ?. apply (checker_nf_sound Zsor ZSORaddon l w). unfold check_normalised_formulas. unfold eval_Psatz in Hf. rewrite Hf. unfold Zunsat in H0. assumption. + intros H0 H1 env. assert (make_impl (eval_nformula env) (f::l) False) as H2. { apply H with (2:= H1). unfold ltof. simpl. auto with arith. } destruct f. rewrite <- make_conj_impl in H2. rewrite make_conj_cons in H2. rewrite <- make_conj_impl. intro. apply H2. split ; auto. apply eval_Psatz_sound with (2:= Hf) ; assumption. - simpl. intros l. case_eq (eval_Psatz l w) ; [ | discriminate]. intros f' Hlc. case_eq (genCuttingPlane f'). + intros p H0 H1 env. assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False) as H2. { eapply (H pf) ; auto. unfold ltof. simpl. auto with arith. } rewrite <- make_conj_impl in H2. rewrite make_conj_cons in H2. rewrite <- make_conj_impl. intro. apply H2. split ; auto. apply (eval_Psatz_sound env) in Hlc. * apply cutting_plane_sound with (1:= Hlc) (2:= H0). * auto. + intros H0 H1 env. rewrite <- make_conj_impl. intros H2. apply eval_Psatz_sound with (2:= Hlc) in H2. apply genCuttingPlaneNone with (2:= H2) ; auto. - intros l. cbn - [genCuttingPlane]. case_eq (genCuttingPlane (p, NonStrict)) ; [| discriminate]. case_eq (genCuttingPlane (popp p, NonStrict)) ; [| discriminate]. intros cp1 GCP1 cp2 GCP2 ZC1 env. flatten_bool. match goal with [ H' : ZChecker _ pf1 = true |- _ ] => rename H' into H0 end. match goal with [ H' : ZChecker _ pf2 = true |- _ ] => rename H' into H1 end. destruct (eval_nformula_split env p). + apply (fun H' ck => H _ H' _ ck env) in H0. * rewrite <- make_conj_impl in *. intro ; apply H0. rewrite make_conj_cons. split; auto. apply (cutting_plane_sound _ (p,NonStrict)) ; auto. * apply ltof_bdepth_split_l. + apply (fun H' ck => H _ H' _ ck env) in H1. * rewrite <- make_conj_impl in *. intro ; apply H1. rewrite make_conj_cons. split; auto. apply (cutting_plane_sound _ (popp p,NonStrict)) ; auto. * apply ltof_bdepth_split_r. - intros l. simpl. case_eq (eval_Psatz l w1) ; [ | discriminate]. case_eq (eval_Psatz l w2) ; [ | discriminate]. intros f1 Hf1 f2 Hf2. case_eq (genCuttingPlane f2). + intros p; destruct p as [ [p1 z1] op1]. case_eq (genCuttingPlane f1). * intros p; destruct p as [ [p2 z2] op2]. case_eq (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd p1 p2)). -- intros Hcond. flatten_bool. match goal with [ H1 : is_pol_Z0 (padd p1 p2) = true |- _ ] => rename H1 into HZ0 end. match goal with [ H2 : valid_cut_sign op1 = true |- _ ] => rename H2 into Hop1 end. match goal with [ H3 : valid_cut_sign op2 = true |- _ ] => rename H3 into Hop2 end. intros HCutL HCutR Hfix env. rewrite <- make_conj_impl. intro H0. assert (-z1 <= eval_pol env p1 <= z2) as H1. { split. - apply (eval_Psatz_sound env) in Hf2 ; auto. apply cutting_plane_sound with (1:= Hf2) in HCutR. unfold nformula_of_cutting_plane in HCutR. unfold eval_nformula in HCutR. unfold RingMicromega.eval_nformula in HCutR. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutR. unfold eval_op1 in HCutR. destruct op1 ; simpl in Hop1 ; try discriminate; rewrite eval_pol_add in HCutR; simpl in HCutR. + rewrite Z.add_move_0_l in HCutR; rewrite HCutR, Z.opp_involutive; reflexivity. + now apply Z.le_sub_le_add_r in HCutR. - apply (fun H => is_pol_Z0_eval_pol _ H env) in HZ0. rewrite eval_pol_add, Z.add_move_r, Z.sub_0_l in HZ0. rewrite HZ0. apply (eval_Psatz_sound env) in Hf1 ; auto. apply cutting_plane_sound with (1:= Hf1) in HCutL. unfold nformula_of_cutting_plane in HCutL. unfold eval_nformula in HCutL. unfold RingMicromega.eval_nformula in HCutL. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutL. unfold eval_op1 in HCutL. rewrite eval_pol_add in HCutL. simpl in HCutL. destruct op2 ; simpl in Hop2 ; try discriminate. + rewrite Z.add_move_r, Z.sub_0_l in HCutL. now rewrite HCutL, Z.opp_involutive. + now rewrite <- Z.le_sub_le_add_l in HCutL. } revert Hfix. match goal with | |- context[?F pf (-z1) z2 = true] => set (FF := F) end. intros Hfix. assert (HH :forall x, -z1 <= x <= z2 -> exists pr, (In pr pf /\ ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z). { clear HZ0 Hop1 Hop2 HCutL HCutR H0 H1. revert Hfix. generalize (-z1). clear z1. intro z1. revert z1 z2. induction pf as [|a pf IHpf];simpl ;intros z1 z2 Hfix x **. - revert Hfix. now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zlt_not_le _ _ LT); transitivity x. - flatten_bool. match goal with [ H' : _ <= x <= _ |- _ ] => rename H' into H0 end. match goal with [ H' : FF pf (z1 + 1) z2 = true |- _ ] => rename H' into H2 end. destruct (Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ]. 2: exists a; auto. rewrite <- Z.le_succ_l in LT. assert (LE: (Z.succ z1 <= x <= z2)%Z) by intuition. elim IHpf with (2:=H2) (3:= LE). + intros x0 ?. exists x0 ; split;tauto. + intros until 1. apply H ; auto. unfold ltof in *. simpl in *. Zify.zify. intuition subst. * assumption. * eapply Z.lt_le_trans. -- eassumption. -- apply Z.add_le_mono_r. assumption. } destruct (HH _ H1) as [pr [Hin Hcheker]]. assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False) as H2. { eapply (H pr) ;auto. apply in_bdepth ; auto. } rewrite <- make_conj_impl in H2. apply H2. rewrite make_conj_cons. split ;auto. unfold eval_nformula. unfold RingMicromega.eval_nformula. simpl. rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). unfold eval_pol. ring. -- discriminate. * intros H0 H1 H2 env. rewrite <- make_conj_impl. intros H3. apply eval_Psatz_sound with (2:= Hf1) in H3. apply genCuttingPlaneNone with (2:= H3) ; auto. + intros H0 H1 env. rewrite <- make_conj_impl. intros H2. apply eval_Psatz_sound with (2:= Hf2) in H2. apply genCuttingPlaneNone with (2:= H2) ; auto. - intros l. unfold ZChecker. fold ZChecker. set (fr := (max_var_nformulae l)%positive). set (z1 := (Pos.succ fr)) in *. set (t1 := (Pos.succ z1)) in *. destruct (x <=? fr)%positive eqn:LE ; [|congruence]. intros H0 env. set (env':= fun v => if Pos.eqb v z1 then if Z.leb (env x) 0 then 0 else env x else if Pos.eqb v t1 then if Z.leb (env x) 0 then -(env x) else 0 else env v). apply (fun H' ck => H _ H' _ ck env') in H0. + rewrite <- make_conj_impl in *. intro H1. rewrite !make_conj_cons in H0. apply H0 ; repeat split. * apply eval_nformula_mk_eq_pos. unfold env'. rewrite! Pos.eqb_refl. replace (x=?z1)%positive with false. 1:replace (x=?t1)%positive with false. 1:replace (t1=?z1)%positive with false. 1:destruct (env x <=? 0); ring. { unfold t1. pos_tac; normZ. lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)). } { unfold t1, z1. pos_tac; normZ. lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.succ (Z.pos fr))) ltac:(assumption))). } { unfold z1. pos_tac; normZ. lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.pos fr)) ltac:(assumption))). } * apply eval_nformula_bound_var. unfold env'. rewrite! Pos.eqb_refl. destruct (env x <=? 0) eqn:EQ. -- compute. congruence. -- rewrite Z.leb_gt in EQ. normZ. lia (Add (Hyp EQ) (Hyp (e := 0 - (env x + 1)) ltac:(assumption))). * apply eval_nformula_bound_var. unfold env'. rewrite! Pos.eqb_refl. replace (t1 =? z1)%positive with false. -- destruct (env x <=? 0) eqn:EQ. ++ rewrite Z.leb_le in EQ. normZ. lia (Add (Hyp EQ) (Hyp (e := 0 - (- env x + 1)) ltac:(assumption))). ++ compute; congruence. -- unfold t1. clear. pos_tac; normZ. lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)). * rewrite (agree_env_eval_nformulae _ env') in H1;auto. unfold agree_env; intros x0 H2. unfold env'. replace (x0 =? z1)%positive with false. 1:replace (x0 =? t1)%positive with false. 1:reflexivity. { unfold t1, z1. unfold fr in *. apply Pos2Z.pos_le_pos in H2. pos_tac; normZ. lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.succ (Z.pos (max_var_nformulae l)))) ltac:(assumption))). } { unfold z1, fr in *. apply Pos2Z.pos_le_pos in H2. pos_tac; normZ. lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.pos (max_var_nformulae l))) ltac:(assumption))). } + unfold ltof. simpl. apply Nat.lt_succ_diag_r. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat