proposition: Lemma valid_check_ImmBuildProj : forall cid i, C.valid rho (check_ImmBuildProj cid i).
proof: Proof. unfold check_ImmBuildProj,C.valid;intros cid i. generalize (Hs cid);unfold C.valid. destruct (S.get s cid) as [ | l [ | _l _c]];auto using C.interp_true. simpl;unfold Lit.interp, Var.interp; rewrite !rho_interp; destruct (t_form.[Lit.blit l]);auto using C.interp_true; case_eq (i <? PArray.length a); intros Hlt;auto using C.interp_true; case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; rewrite !orb_false_r. - rewrite afold_left_and. rewrite forallb_forall;intros H;apply H;auto. apply to_list_In; auto. - rewrite negb_true_iff, <-not_true_iff_false, afold_left_or. unfold C.interp;rewrite existsb_exists, Lit.interp_neg. case_eq (Lit.interp rho (a .[ i]));trivial. intros Heq' Hex;elim Hex;exists (a.[i]);split;trivial. apply to_list_In; auto. - rewrite negb_true_iff, <-not_true_iff_false. assert (Hl:(PArray.length a =? 0) = false) by (rewrite eqb_false_spec; intro H; rewrite H in Hlt; now apply (ltb_0 i)). rewrite (afold_right_impb (Lit.interp_neg _) Hl). case_eq (i =? PArray.length a - 1);intros Heq';simpl; unfold C.interp;simpl;try rewrite Lit.interp_neg;rewrite orb_false_r, existsb_exists;case_eq (Lit.interp rho (a .[ i]));trivial; intros Heq2 Hex;elim Hex. exists (a.[i]);split;trivial. assert (H1: 0 <? PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63.eqb_spec in Heq'; rewrite <- (get_or_of_imp2 H1 Heq'); apply to_list_In; rewrite length_or_of_imp; auto. exists (Lit.neg (a.[i]));rewrite Lit.interp_neg, Heq2;split;trivial. assert (H1: i <? PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; assert (H1: [|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; lia); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList