proposition: Lemma valid_check_bbConst lres : C.valid rho (check_bbConst lres).
proof: Proof. unfold check_bbConst. case_eq (Lit.is_pos lres); intro Heq1; [ |now apply C.interp_true]. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bs Heq0. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros c Ha. case_eq c; try (intros; now apply C.interp_true). intros l N Hc. case_eq (check_bbc l bs && (N.of_nat (Datatypes.length l) =? N)%N); try (intros; now apply C.interp_true). intro Hcheck. unfold C.valid. simpl. rewrite orb_false_r. unfold Lit.interp. rewrite Heq1. unfold Var.interp. rewrite wf_interp_form; trivial. rewrite Heq0. simpl. assert (Hinterpa: (interp_form_hatom_bv a = interp_bv t_i (interp_atom (t_atom .[a])))). { unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. } rewrite Hinterpa. rewrite Ha, Hc. simpl. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. assert ((N.of_nat (Datatypes.length (map (Lit.interp rho) bs))) = N). { rewrite andb_true_iff in Hcheck. destruct Hcheck as (Hcheck1 & Hcheck2). apply check_bbc_length in Hcheck1. rewrite N.eqb_eq in Hcheck2. rewrite Hcheck1 in Hcheck2. now rewrite map_length. } generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs) ). rewrite H. intros. rewrite Typ.N_cast_refl. unfold BITVECTOR_LIST.bv_eq, RAWBITVECTOR_LIST.bv_eq. simpl. unfold RAWBITVECTOR_LIST.size, RAWBITVECTOR_LIST._of_bits. rewrite andb_true_iff in Hcheck. destruct Hcheck as (Hcheck1 & Hcheck2). pose proof Hcheck1. apply check_bbc_length in Hcheck1. rewrite N.eqb_eq in Hcheck2. rewrite Hcheck2. rewrite N.eqb_refl. rewrite Hcheck1, map_length, N.eqb_refl. unfold RAWBITVECTOR_LIST.bits. now apply prop_check_bbc2. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance