proposition: Lemma build_clause_correct : forall cl vm vm' bf, build_clause vm cl = 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 /\ (C.interp rho cl <-> eval_f (Zeval_formula (interp_vmap vm')) bf).
proof: Proof. unfold build_clause;intros cl vm vm' bf. case_eq (build_clause_aux vm cl);try discriminate. intros (vm1, bf1) Heq W Hwf;inversion W;clear W;subst. assert (W:= build_clause_aux_correct _ _ _ _ Heq Hwf). decompose [and] W;clear W. repeat (split;[trivial;fail | ]). split;simpl. rewrite H2;reflexivity. unfold is_true in *; destruct (C.interp rho cl);split;simpl;trivial;try discriminate; try tauto. intros _ HH;destruct H4. apply H4 in HH;discriminate. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz