proposition: Lemma build_clause_aux_correct : forall cl vm vm' bf, build_clause_aux 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 /\ (negb (C.interp rho cl) <-> eval_f (Zeval_formula (interp_vmap vm')) bf).
proof: Proof. induction cl;try discriminate. case_eq cl. intros _; simpl;intros;rewrite orb_false_r;apply build_nlit_correct;trivial. intros i l Heq vm vm' bf;rewrite <- Heq at 2. change (build_clause_aux vm (a :: i :: l) ) with ( match build_nlit vm a with | Some (vm0, bf1) => match build_clause_aux vm0 (i::l) with | Some (vm1, bf2) => Some (vm1, AND bf1 bf2) | None => None end | None => None end). case_eq (build_nlit vm a);try discriminate. intros (vm0, bf1) Heq1 Heq2 Hwf. rewrite <- Heq in Heq2. assert (W:= build_nlit_correct _ _ _ _ Heq1 Hwf). decompose [and] W;clear W. revert Heq2; case_eq (build_clause_aux vm0 cl);try discriminate. intros (vm1, fb2) Heq2 W;inversion W;clear W Heq;subst. assert (W:= IHcl _ _ _ Heq2 H);decompose [and] W;clear W. split;trivial. split. apply le_trans with (1:= H1);trivial. split. intros p Hlt;rewrite H0, H5;trivial. apply lt_le_trans with (1:= Hlt);trivial. split. simpl;rewrite H7, andb_true_r. apply bounded_bformula_le with (2:= H2);trivial. simpl. unfold is_true; rewrite <- (interp_bformula_le _ _ H5), <- H4, <- H9, negb_orb,andb_true_iff; tauto. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz