proposition: Lemma get_or_of_imp : forall args i, i <? (PArray.length args) - 1 -> (or_of_imp args).[i] = Lit.neg (args.[i]).
proof: Proof. unfold or_of_imp; intros args i H; case_eq (0 <? PArray.length args). intro Heq; rewrite get_amapi. replace (i =? PArray.length args - 1) with false; auto; symmetry; rewrite eqb_false_spec; intro; subst i; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; lia. rewrite ltb_spec; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; lia. rewrite ltb_negb_geb; case_eq (PArray.length args <=? 0); try discriminate; intros Heq _; assert (H1: PArray.length args = 0). apply to_Z_inj; rewrite leb_spec in Heq; destruct (to_Z_bounded (PArray.length args)) as [H1 _]; change [|0|] with 0%Z in *; lia. rewrite !get_outofbound. rewrite default_amapi, H1; auto. rewrite H1; case_eq (i <? 0); auto; intro H2; eelim ltb_0; eassumption. rewrite length_amapi, H1; case_eq (i <? 0); auto; intro H2; eelim ltb_0; eassumption. Qed.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList