proposition: Lemma build_not2_pos_correct : forall vm (f:GFormula isProp) l i, bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l -> bounded_bformula (fst vm) (build_not2 i f) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (build_not2 i f)).
proof: Proof. simpl; intros vm f l i H1 H2 H3; unfold build_not2. case (Z.le_gt_cases 1 [|i|]); [ intro Hle | intro Hlt ]. set (a := foldi _ _ _ _); set (b := foldi _ _ _ _); pattern i, a, b; subst a b; apply foldi_ind2. apply leb_0. unfold Lit.interp; rewrite H3; auto. intros j f' b _ _; rewrite negb_involutive; simpl. intros [ H H' ]; rewrite <- H'. unfold is_true; rewrite not_true_iff_false, not_false_iff_true; tauto. rewrite 2!foldi_ge by (rewrite leb_spec, to_Z_0; lia). unfold Lit.interp; rewrite H3; auto. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz