proposition: Lemma prop_checkbb: forall (a: int) (bs: list _lit) (i n: nat), (length bs = (n - i))%nat -> (check_bb a bs i n = true) -> (forall i0, (i <= i0 < n )%nat -> Lit.interp rho (nth (i0 - i) bs 1) = (@BITVECTOR_LIST.bitOf (N.of_nat n) i0 (interp_form_hatom_bv a (N.of_nat n)))).
proof: Proof. intros a bs. revert a. induction bs as [ | b ys IHys]. - intros. simpl in H. cut (i = n). intro Hn. rewrite Hn in H1. contradict H1. lia. lia. - intros. simpl in H0. case_eq (Lit.is_pos b). intros Heq0. rewrite Heq0 in H0. case_eq (t_form .[ Lit.blit b] ). intros i1 Heq1. rewrite Heq1 in H0. case_eq (t_atom .[ i1]). intros c Heq2. rewrite Heq2 in H0; now contradict H0. intros u i2 Heq2. rewrite Heq2 in H0. case_eq u; try (intro Heq'; rewrite Heq' in H0; now contradict H0). intros. rewrite H2 in H0. case_eq ((a =? i2) && Nat.eqb i n1 && Nat.eqb n (N.to_nat n0)). intros Hif. rewrite Hif in H0. do 2 rewrite andb_true_iff in Hif. destruct Hif as ((Hif0 & Hif1) & Hif2). specialize (@IHys a (S i) n). inversion H. cut (Datatypes.length ys = (n - S i)%nat). intro HSi. specialize (@IHys HSi H0). cut (((S i) <= i0 < n)%nat \/ i = i0). intro Hd. destruct Hd as [Hd | Hd]. inversion Hd. induction i0 as [ | k IHk]. now contradict H3. specialize (@IHys (S k)). cut ((S k - i)%nat = S (k - i)%nat). intro ISk. rewrite ISk. rewrite (@nth_eq1 (k - i) b ys). cut ((S k - S i)%nat = (k - i)%nat). intro ISki. specialize (@IHys Hd). now rewrite ISki in IHys. now simpl. lia. rewrite Hd. cut ((i0 - i0 = 0)%nat). intro Hi0. rewrite Hi0. simpl. unfold Lit.interp. rewrite Heq0. unfold Var.interp. rewrite rho_interp. rewrite Heq1. rewrite Lit.eqb_spec in Hif0. rewrite Hif0. rewrite <- Hd. generalize wt_t_atom. unfold Atom.wt. unfold is_true. rewrite aforallbi_spec;intros. assert (i1 <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite Heq2. now rewrite def_t_atom. } specialize (@H3 i1 H5). rewrite Heq2 in H3. simpl in H3. rewrite H2 in H3. simpl in H3. rewrite !andb_true_iff in H3. decompose [and] H3. clear H3. simpl in H7. unfold get_type' in H6, H7. unfold v_type in H6, H7. case_eq (t_interp .[ i1]). intros. rewrite H3 in H6. simpl in H6. case_eq (v_type0); intros; try (rewrite H8 in H6; now contradict H6). simpl. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_form_hatom. unfold Atom.interp_hatom. rewrite Atom.t_interp_wf; trivial. rewrite Heq2. simpl. rewrite H2. simpl. cut (i = n1). intro Hin1. rewrite Hin1. cut (n = (N.to_nat n0)). intro Hnn0. rewrite Hnn0. rewrite id''. case_eq (t_interp .[ i2]). intros. rewrite H9 in H7. rewrite <- H9. case_eq v_type1; intros; rewrite H10 in H7; try (now contradict H7). cut (n2 = n0)%N. intros Hn2n0. rewrite Hn2n0 in H10. rewrite H9. simpl. unfold interp_bool. case_eq (Typ.cast v_type1 (Typ.TBV n0)). split. rewrite H10. simpl. rewrite Typ.N_cast_refl. intros. contradict H11. easy. apply Typ.eqb_spec in H7. inversion H7. easy. now apply Nat.eqb_eq in Hif2. now apply Nat.eqb_eq in Hif1. lia. destruct H1. specialize (@le_le_S_eq i i0). intros H11. specialize (@H11 H1). destruct H11. left. split. exact H5. exact H3. right. exact H5. lia. intro H3. rewrite H3 in H0. now contradict H0. intros n0 Hn. rewrite Hn in H0. now contradict H0. intros n0 Hn. rewrite Hn in H0. now contradict H0. intros i3 n0 n1 Heq. rewrite Heq in H0. now contradict H0. intros n0 i3 Heq. rewrite Heq in H0. now contradict H0. intros n0 i3 Heq. rewrite Heq in H0. now contradict H0. intros b0 i2 i3 Heq. rewrite Heq in H0. now contradict H0. intros t i2 i3 i4 Heq. rewrite Heq in H0. now contradict H0. intros n0 l Heq. rewrite Heq in H0. now contradict H0. intros i2 l Heq. rewrite Heq in H0. now contradict H0. intros Heq. rewrite Heq in H0. now contradict H0. intros Heq. rewrite Heq in H0. now contradict H0. intros i1 i2 Heq. rewrite Heq in H0. now contradict H0. intros a0 Heq. rewrite Heq in H0. now contradict H0. intros a0 Heq. rewrite Heq in H0. now contradict H0. intros a0 Heq. rewrite Heq in H0. now contradict H0. intros i1 i2 Heq. rewrite Heq in H0. now contradict H0. intros i1 i2 Heq. rewrite Heq in H0. now contradict H0. intros i1 i2 i3 Heq. rewrite Heq in H0. now contradict H0. intros i1 l Heq. rewrite Heq in H0. now contradict H0. intros Heq. rewrite Heq in H0. now contradict H0. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance