proposition: Lemma afold_right_impb p a : (forall x, p (Lit.neg x) = negb (p x)) -> (PArray.length a =? 0) = false -> (afold_right bool true implb (amap p a)) = List.existsb p (to_list (or_of_imp a)).
proof: Proof. intros Hp Hl. case_eq (afold_right bool true implb (amap p a)); intro Heq; symmetry. - apply afold_right_implb_true_inv in Heq. rewrite length_amap in Heq. destruct Heq as [Heq|[[i [Hi Heq]]|Heq]]. + rewrite Heq in Hl. discriminate. + rewrite get_amap in Heq. rewrite existsb_exists. exists (Lit.neg (a .[ i])). split. * { apply (to_list_In_eq _ i). - rewrite length_or_of_imp. apply (ltb_trans _ (PArray.length a - 1)); auto. now apply minus_1_lt. - now rewrite get_or_of_imp. } * now rewrite Hp, Heq. * apply (ltb_trans _ (PArray.length a - 1)); auto. now apply minus_1_lt. + rewrite existsb_exists. exists (a.[(PArray.length a) - 1]). split. * { apply (to_list_In_eq _ (PArray.length a - 1)). - rewrite length_or_of_imp. now apply minus_1_lt. - symmetry. apply get_or_of_imp2; auto. unfold is_true. rewrite ltb_spec. rewrite eqb_false_spec in Hl. assert (0%Z <> [|PArray.length a|]) by (change 0%Z with [|0|]; intro H; apply to_Z_inj in H; auto). destruct (to_Z_bounded (PArray.length a)) as [H1 _]. clear -H H1. change [|0|] with 0%Z. lia. } * { specialize (Heq (PArray.length a - 1)); rewrite get_amap in Heq by now apply minus_1_lt. apply Heq. now apply minus_1_lt. } - apply afold_right_implb_false_inv in Heq. destruct Heq as [H1 [H2 H3]]. rewrite length_amap in H1, H3. case_eq (List.existsb p (to_list (or_of_imp a))); auto. rewrite existsb_exists. intros [x [H4 H5]]. apply In_to_list in H4. destruct H4 as [i [H4 ->]]. case_eq (i <? PArray.length a - 1); intro Heq. + specialize (H2 i). rewrite length_amap in H2. assert (H6 := H2 Heq). rewrite get_amap in H6. now rewrite (get_or_of_imp Heq), Hp, H6 in H5. apply (ltb_trans _ (PArray.length a - 1)); auto. now apply minus_1_lt. + assert (H6:i = PArray.length a - 1). { clear -H4 Heq H1. rewrite length_or_of_imp in H4. apply to_Z_inj. rewrite (to_Z_sub_1 _ 0); auto. rewrite ltb_spec in H4; auto. rewrite ltb_negb_geb in Heq. case_eq (PArray.length a - 1 <=? i); intro H2; rewrite H2 in Heq; try discriminate. clear Heq. rewrite leb_spec in H2. rewrite (to_Z_sub_1 _ 0) in H2; auto. lia. } rewrite get_or_of_imp2 in H5; auto. rewrite get_amap in H3 by now apply minus_1_lt. rewrite H6, H3 in H5. discriminate. Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList