proposition: Lemma valid_check_BuildProj : forall l i, C.valid rho (check_BuildProj l i).
proof: Proof. unfold check_BuildProj,C.valid;intros l i. case_eq (t_form.[Lit.blit l]);intros;auto using C.interp_true; case_eq (i <? PArray.length a);intros Hlt;auto using C.interp_true;simpl. - rewrite Lit.interp_nlit;unfold Var.interp;rewrite rho_interp, orb_false_r, H. simpl;rewrite afold_left_and. case_eq (List.forallb (Lit.interp rho) (to_list a));trivial. rewrite forallb_forall;intros Heq;rewrite Heq;trivial. apply to_list_In; auto. - rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, orb_false_r, H. simpl;rewrite afold_left_or. unfold C.interp;case_eq (List.existsb (Lit.interp rho) (to_list a));trivial. rewrite <-not_true_iff_false, 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. - assert (Hl : (PArray.length a =? 0) = false) by (rewrite eqb_false_spec; intro H1; rewrite H1 in Hlt; now elim (ltb_0 i)). case_eq (i =? PArray.length a - 1);intros Heq;simpl; rewrite Lit.interp_lit;unfold Var.interp;rewrite rho_interp, H;simpl. + rewrite Lit.interp_neg, orb_false_r. rewrite (afold_right_impb (Lit.interp_neg _) Hl). case_eq (Lit.interp rho (a .[ i])); intro Hi. * rewrite orb_false_r, existsb_exists. exists (a .[ i]). split; auto. { apply (to_list_In_eq _ i). - now rewrite length_or_of_imp. - symmetry. apply get_or_of_imp2. + clear -Hl. rewrite eqb_false_spec in Hl. unfold is_true. rewrite ltb_spec. change [|0|] with 0%Z. assert (H:[|PArray.length a|] <> 0%Z) by (intro H; apply Hl; now apply to_Z_inj). destruct (to_Z_bounded (PArray.length a)) as [H1 _]. lia. + now rewrite Int63.eqb_spec in Heq. } * now rewrite orb_true_r. + rewrite orb_false_r. case_eq (Lit.interp rho (a .[ i])); intro Hi. * now rewrite orb_true_r. * rewrite (afold_right_impb (Lit.interp_neg _) Hl). rewrite orb_false_r, existsb_exists. exists (Lit.neg (a .[ i])). { split. - apply (to_list_In_eq _ i). + now rewrite length_or_of_imp. + symmetry. apply get_or_of_imp. clear -Hlt Heq. unfold is_true. rewrite ltb_spec. rewrite (to_Z_sub_1 _ i); auto. rewrite eqb_false_spec in Heq. assert (H:[|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H; apply Heq, to_Z_inj; rewrite (to_Z_sub_1 _ i); auto). clear Heq. rewrite ltb_spec in Hlt. lia. - now rewrite Lit.interp_neg, Hi. } Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList