proposition: Lemma valid_check_bbNeg pos lres : C.valid rho (check_bbNeg pos lres).
proof: Proof. unfold check_bbNeg. case_eq (S.get s pos); [intros _|intros l1 [ |l] Heq1]; try now apply C.interp_true. case_eq (Lit.is_pos l1); intro Heq3; simpl; try now apply C.interp_true. case_eq (Lit.is_pos lres); intro Heq5; simpl; try now apply C.interp_true. case_eq (t_form .[ Lit.blit l1]); try (intros; now apply C.interp_true). intros a1 bs1 Heq6. case_eq (t_form .[ Lit.blit lres]); try (intros; now apply C.interp_true). intros a bsres Heq8. case_eq (t_atom .[ a]); try (intros; now apply C.interp_true). intros [ | | | | | | | | | | ] a1' Heq9; try now apply C.interp_true. case_eq ((a1 =? a1') && check_neg bs1 bsres && (N.of_nat (Datatypes.length bs1) =? n)%N); simpl; intros Heq11; try (now apply C.interp_true). unfold C.valid. simpl. rewrite orb_false_r. unfold Lit.interp. rewrite Heq5. unfold Var.interp. rewrite wf_interp_form; trivial. rewrite Heq8. simpl. apply BITVECTOR_LIST.bv_eq_reflect. generalize wt_t_atom. unfold Atom.wt. unfold is_true. rewrite aforallbi_spec;intros. pose proof (H a). assert (a <? PArray.length t_atom). { apply PArray.get_not_default_lt. rewrite def_t_atom. rewrite Heq9. easy. } specialize (@H0 H1). rewrite Heq9 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 .[ a]). intros v_typea v_vala Htia. rewrite Htia in H0. case_eq (v_typea); intros; rewrite H3 in H0; try (now contradict H0). rename H3 into Hv. generalize (Hs pos). intros HSp1. unfold C.valid in HSp1. rewrite Heq1 in HSp1. unfold C.interp in HSp1. unfold existsb in HSp1. rewrite orb_false_r in HSp1. unfold Lit.interp in HSp1. rewrite Heq3 in HSp1. unfold Var.interp in HSp1. rewrite rho_interp in HSp1. rewrite Heq6 in HSp1. simpl in HSp1. apply BITVECTOR_LIST.bv_eq_reflect in HSp1. unfold get_type' in H2. unfold v_type in H2. case_eq (t_interp .[ a1']). intros v_typea1 v_vala1 Htia1. rewrite Htia1 in H2. rewrite Atom.t_interp_wf in Htia1; trivial. unfold apply_binop. apply Typ.eqb_spec in H2. do 2 rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq10, Heq11). destruct Heq10 as (Heq10a1 & Heq10a2). rewrite Int63.eqb_spec in Heq10a1; rewrite Heq10a1 in *. assert (interp_form_hatom_bv a = interp_bv t_i (interp_atom (t_atom .[a]))). { rewrite !Atom.t_interp_wf in Htia; trivial. rewrite Htia. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia. easy. } rewrite H3. rewrite Heq9. simpl. unfold interp_bv. unfold apply_binop. rewrite !Atom.t_interp_wf; trivial. revert v_vala1 Htia1. rewrite H2. intros. rewrite Htia1. unfold apply_unop. rewrite Typ.cast_refl. unfold Bval. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. assert (H100: (N.of_nat (Datatypes.length (map (Lit.interp rho) bsres))) = n). { apply check_neg_length in Heq10a2. rewrite N.eqb_eq in Heq11. rewrite Heq10a2 in Heq11. now rewrite map_length. } generalize (BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bsres)). rewrite H100. rewrite Typ.cast_refl. intros. unfold BITVECTOR_LIST.bv_neg. apply eq_rec. simpl. assert (interp_form_hatom_bv a1' = interp_bv t_i (interp_atom (t_atom .[a1']))). { rewrite !Atom.t_interp_wf in Htia; trivial. rewrite Htia1. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia1. easy. } rewrite H4 in HSp1. unfold interp_bv in HSp1. rewrite Htia1 in HSp1. unfold interp_bv in HSp1. revert HSp1. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. assert (H101: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs1))) = n). { rewrite N.eqb_eq in Heq11. now rewrite map_length. } generalize (BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs1)). rewrite H101. rewrite Typ.cast_refl. intros. rewrite HSp1. simpl. specialize(@prop_check_neg bs1 bsres). intros. apply H5 with n. now rewrite N.eqb_eq in Heq11. pose proof Heq10a2 as Heq10a3. apply check_neg_length in Heq10a3. rewrite <- Heq10a3. now rewrite N.eqb_eq in Heq11. easy. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance