proposition: Lemma valid_check_bbNot pos lres : C.valid rho (check_bbNot pos lres).
proof: Proof. unfold check_bbNot. case_eq (S.get s pos); [ (intros; now apply C.interp_true) | ]. intros l ls Hpos. case_eq ls; [ | (intros; now apply C.interp_true) ]. intro Hnil. case_eq (Lit.is_pos l && Lit.is_pos lres); [ | (intros; now apply C.interp_true) ]. intro Hpos'. case_eq (t_form .[ Lit.blit l]); try (intros; now apply C.interp_true). intros a bs HBl. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros r br HBr. case_eq (t_atom .[ r]); try (intros; now apply C.interp_true). intros u a'. case_eq u; try (intros; now apply C.interp_true). intros n Huot Hr. case_eq ((a =? a') && check_not bs br && (N.of_nat (Datatypes.length bs) =? n)%N); try (intros; now apply C.interp_true). intro Hc. rewrite !andb_true_iff in Hc. destruct Hc as ((Ha, Hcheck), Hlen). rewrite N.eqb_eq in Hlen. apply Int63.eqb_spec in Ha. generalize (Hs pos). rewrite Hpos, Hnil. unfold C.valid, C.interp; simpl; rewrite !orb_false_r. unfold Lit.interp, Var.interp. rewrite andb_true_iff in Hpos'. destruct Hpos' as (Hposl, Hposlres). rewrite Hposl, Hposlres. rewrite !rho_interp. rewrite HBl, HBr. simpl. intro Heqa. apply BITVECTOR_LIST.bv_eq_reflect in Heqa. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. rewrite aforallbi_spec;intros. pose proof (H r). assert (r <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Hr. easy. } specialize (@H0 H1). rewrite Hr in H0. simpl in H0. rewrite !andb_true_iff in H0. destruct H0. unfold get_type' in H0. unfold v_type in H0. case_eq (t_interp .[ r]). intros v_typer v_valr Htir. rewrite Htir in H0. case_eq (v_typer); intros; rewrite H3 in H0; try (now contradict H1). rename H3 into Hv. assert (interp_form_hatom_bv r = interp_bv t_i (interp_atom (t_atom .[r]))). { unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. } rewrite H3, Hr. simpl. unfold interp_bv. apply Typ.eqb_spec in H2. unfold get_type' in H2. unfold v_type in H2. case_eq (t_interp .[ a']). intros. rewrite H4 in H2. simpl. revert v_val0 H4. rewrite H2. intros. rewrite Typ.cast_refl. simpl. assert ( (N.of_nat (Datatypes.length (map (Lit.interp rho) br))) = n). { apply check_not_length in Hcheck. rewrite Hcheck in Hlen. now rewrite map_length. } unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) br) ). rewrite H5. intros. rewrite Typ.N_cast_refl. unfold BITVECTOR_LIST.bv_not, RAWBITVECTOR_LIST.bv_not. apply eq_rec. simpl. rewrite <- Ha in *. assert (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 H6 in Heqa. unfold interp_bv in Heqa. rewrite <- !Atom.t_interp_wf in Heqa; trivial. rewrite H4 in Heqa. revert Heqa . assert ( (N.of_nat (Datatypes.length (map (Lit.interp rho) bs))) = n). { now rewrite map_length. } unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs) ). rewrite H7. rewrite Typ.cast_refl. intros. rewrite Heqa. simpl. specialize (@prop_check_not bs br). intros. symmetry. unfold RAWBITVECTOR_LIST.bits. rewrite map_map; apply H8; auto. now apply check_not_length in Hcheck. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance