proposition: Lemma build_var_correct : forall v vm vm' bf, build_var vm v = Some (vm', bf) -> wf_vmap vm -> wf_vmap vm' /\ (nat_of_P (fst vm) <= nat_of_P (fst vm'))%nat /\ (forall p, (nat_of_P p < nat_of_P (fst vm))%nat -> nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = nth_error (snd vm')(nat_of_P (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ (Var.interp rho v <-> eval_f (Zeval_formula (interp_vmap vm')) bf).
proof: Proof. unfold build_var; apply foldi_ind; try discriminate. apply leb_0. intros i cont _ Hlen Hrec v vm vm' bf; unfold is_true; intros H1 H2; replace (Var.interp rho v) with (Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form.[v])). apply (build_hform_correct cont); auto with smtcoq_core. unfold Var.interp; rewrite <- wf_interp_form; auto with smtcoq_core. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz