proposition: Lemma valid_check_bbOp pos1 pos2 lres: C.valid rho (check_bbOp pos1 pos2 lres).
proof: Proof. unfold check_bbOp. case_eq (S.get s pos1); [intros _|intros l1 [ |l] Heq1]; try now apply C.interp_true. case_eq (S.get s pos2); [intros _|intros l2 [ |l] Heq2]; 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 l2); intro Heq4; 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 l2]); try (intros; now apply C.interp_true). intros a2 bs2 Heq7. 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 [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ] a1' a2' Heq9; try (intros; now apply C.interp_true). - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( check_symopp bs1 bs2 bsres (BO_BVand N) && (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. unfold Atom.interp_form_hatom_bv at 2, Atom.interp_hatom. rewrite Atom.t_interp_wf; trivial. rewrite Heq9. simpl. rewrite Atom.t_interp_wf; trivial. rewrite Atom.t_interp_wf; trivial. 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. destruct H0. unfold get_type' in H2, H3. unfold v_type in H2, H3. case_eq (t_interp .[ a1']). intros v_typea1 v_vala1 Htia1. rewrite Htia1 in H3. case_eq (t_interp .[ a2']). intros v_typea2 v_vala2 Htia2. rewrite Htia2 in H2. rewrite Atom.t_interp_wf in Htia1; trivial. rewrite Atom.t_interp_wf in Htia2; trivial. unfold apply_binop. rewrite Htia1, Htia2. apply Typ.eqb_spec in H2. apply Typ.eqb_spec in H3. 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 i j Hv. rewrite Hv in H0. now contradict H0. intros i Hv. rewrite Hv in H0. now contradict H0. intros Hv. rewrite Hv in H0. now contradict H0. intros Hv. rewrite Hv in H0. now contradict H0. intros Hv. rewrite Hv in H0. now contradict H0. intros n Hv. rewrite Hv in H0. apply N.eqb_eq in H0. rewrite <- H0 in *. revert v_vala Htia. rewrite Hv. intros v_vala Htia. generalize (Hs pos1). 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. generalize (Hs pos2). intro HSp2. unfold C.valid in HSp2. rewrite Heq2 in HSp2. unfold C.interp in HSp2. unfold existsb in HSp2. rewrite orb_false_r in HSp2. unfold Lit.interp in HSp2. rewrite Heq4 in HSp2. unfold Var.interp in HSp2. rewrite rho_interp in HSp2. rewrite Heq7 in HSp2. simpl in HSp2. revert v_vala1 Htia1 v_vala2 Htia2. rewrite H2, H3. unfold bvtrue. rewrite Typ.cast_refl. intros v_vala1 Htia1 v_vala2 Htia2. rewrite orb_true_iff in Heq10. do 2 rewrite andb_true_iff in Heq10. destruct Heq10 as [Heq10 | Heq10]; destruct Heq10 as (Heq10a1 & Heq10a2); rewrite eqb_spec in Heq10a1, Heq10a2. rewrite Heq10a1, Heq10a2 in *. apply BITVECTOR_LIST.bv_eq_reflect in HSp2. apply BITVECTOR_LIST.bv_eq_reflect in HSp1. assert (interp_form_hatom_bv a1' = interp_bv t_i (interp_atom (t_atom .[a1']))). { 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. rewrite Htia1 in HSp1. assert (interp_form_hatom_bv a2' = interp_bv t_i (interp_atom (t_atom .[a2']))). { rewrite Htia2. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia2. easy. } rewrite H5 in HSp2. simpl in HSp2. rewrite Htia2 in HSp2. apply BITVECTOR_LIST.bv_eq_reflect. unfold Bval, interp_bv. rewrite (@check_symopp_bvand_nl bs1 bs2 bsres N). assert ( H100: (N.of_nat (Datatypes.length (RAWBITVECTOR_LIST.map2 andb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)))) = N). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. specialize (@RAWBITVECTOR_LIST.map2_and_length (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)). intros. rewrite <- H6. now rewrite map_length. apply check_symopp_bvand_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). now rewrite !map_length, Heq11a, Heq11b. } unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. generalize ( BITVECTOR_LIST.of_bits_size (RAWBITVECTOR_LIST.map2 andb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)) ). rewrite H100. rewrite Typ.cast_refl. intros. unfold BITVECTOR_LIST.bv_and, RAWBITVECTOR_LIST.bv_and. unfold RAWBITVECTOR_LIST.size. unfold RAWBITVECTOR_LIST.bits. unfold interp_bv in HSp1, HSp2. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits in HSp1, HSp2. assert ( H101: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs2))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). apply check_symopp_bvand_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). rewrite <- Heq11a in Heq11b. rewrite <- Heq11b in Heq11r. rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp2. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs2) ). rewrite H101. intros. assert ( H102: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs1))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp1. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs1) ). rewrite H102. intros. rewrite Typ.cast_refl in *. rewrite HSp1, HSp2. simpl. apply eq_rec. simpl. rewrite H101, H102. rewrite N.eqb_compare, N.compare_refl. easy. rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). exact Heq11. rewrite Heq10a1, Heq10a2 in *. apply BITVECTOR_LIST.bv_eq_reflect in HSp2. apply BITVECTOR_LIST.bv_eq_reflect in HSp1. assert (interp_form_hatom_bv a1' = interp_bv t_i (interp_atom (t_atom .[a1']))). { rewrite Htia1. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia1. easy. } rewrite H4 in HSp2. rewrite Htia1 in HSp2. assert (interp_form_hatom_bv a2' = interp_bv t_i (interp_atom (t_atom .[a2']))). { rewrite Htia2. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia2. easy. } rewrite H5 in HSp1. simpl in HSp1. rewrite Htia2 in HSp1. apply BITVECTOR_LIST.bv_eq_reflect. unfold Bval, interp_bv. rewrite (@check_symopp_bvand_nl bs1 bs2 bsres N). assert ( H100: (N.of_nat (Datatypes.length (RAWBITVECTOR_LIST.map2 andb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)))) = N). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. specialize (@RAWBITVECTOR_LIST.map2_and_length (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)). intros. rewrite <- H6. apply check_symopp_bvand_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). now rewrite map_length. apply check_symopp_bvand_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). now rewrite !map_length, Heq11a, Heq11b. } unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. generalize ( BITVECTOR_LIST.of_bits_size (RAWBITVECTOR_LIST.map2 andb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)) ). rewrite H100. rewrite Typ.cast_refl. intros. unfold BITVECTOR_LIST.bv_and, RAWBITVECTOR_LIST.bv_and. unfold RAWBITVECTOR_LIST.size. unfold RAWBITVECTOR_LIST.bits. unfold interp_bv in HSp1, HSp2. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits in HSp1, HSp2. assert ( H101: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs2))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). apply check_symopp_bvand_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). rewrite <- Heq11a in Heq11b. rewrite <- Heq11b in Heq11r. rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp2. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs2) ). rewrite H101. intros. assert ( H102: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs1))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp1. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs1) ). rewrite H102. intros. rewrite Typ.cast_refl in *. rewrite HSp1, HSp2. simpl. apply eq_rec. simpl. rewrite H101, H102. rewrite N.eqb_compare, N.compare_refl. now rewrite RAWBITVECTOR_LIST.map2_and_comm. rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). exact Heq11. - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( check_symopp bs1 bs2 bsres (BO_BVor N) && (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. unfold Atom.interp_form_hatom_bv at 2, Atom.interp_hatom. rewrite Atom.t_interp_wf; trivial. rewrite Heq9. simpl. rewrite Atom.t_interp_wf; trivial. rewrite Atom.t_interp_wf; trivial. 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. destruct H0. unfold get_type' in H2, H3. unfold v_type in H2, H3. case_eq (t_interp .[ a1']). intros v_typea1 v_vala1 Htia1. rewrite Htia1 in H3. case_eq (t_interp .[ a2']). intros v_typea2 v_vala2 Htia2. rewrite Htia2 in H2. rewrite Atom.t_interp_wf in Htia1; trivial. rewrite Atom.t_interp_wf in Htia2; trivial. unfold apply_binop. rewrite Htia1, Htia2. apply Typ.eqb_spec in H2. apply Typ.eqb_spec in H3. 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 i j Hv. rewrite Hv in H0. now contradict H0. intros i Hv. rewrite Hv in H0. now contradict H0. intros Hv. rewrite Hv in H0. now contradict H0. intros Hv. rewrite Hv in H0. now contradict H0. intros Hv. rewrite Hv in H0. now contradict H0. intros n Hv. rewrite Hv in H0. apply N.eqb_eq in H0. rewrite <- H0 in *. revert v_vala Htia. rewrite Hv. intros v_vala Htia. generalize (Hs pos1). 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. generalize (Hs pos2). intro HSp2. unfold C.valid in HSp2. rewrite Heq2 in HSp2. unfold C.interp in HSp2. unfold existsb in HSp2. rewrite orb_false_r in HSp2. unfold Lit.interp in HSp2. rewrite Heq4 in HSp2. unfold Var.interp in HSp2. rewrite rho_interp in HSp2. rewrite Heq7 in HSp2. simpl in HSp2. revert v_vala1 Htia1 v_vala2 Htia2. rewrite H2, H3. unfold bvtrue. rewrite Typ.cast_refl. intros v_vala1 Htia1 v_vala2 Htia2. rewrite orb_true_iff in Heq10. do 2 rewrite andb_true_iff in Heq10. destruct Heq10 as [Heq10 | Heq10]; destruct Heq10 as (Heq10a1 & Heq10a2); rewrite eqb_spec in Heq10a1, Heq10a2. rewrite Heq10a1, Heq10a2 in *. apply BITVECTOR_LIST.bv_eq_reflect in HSp2. apply BITVECTOR_LIST.bv_eq_reflect in HSp1. assert (interp_form_hatom_bv a1' = interp_bv t_i (interp_atom (t_atom .[a1']))). { 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. rewrite Htia1 in HSp1. assert (interp_form_hatom_bv a2' = interp_bv t_i (interp_atom (t_atom .[a2']))). { rewrite Htia2. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia2. easy. } rewrite H5 in HSp2. simpl in HSp2. rewrite Htia2 in HSp2. apply BITVECTOR_LIST.bv_eq_reflect. unfold Bval, interp_bv. rewrite (@check_symopp_bvor_nl bs1 bs2 bsres N). assert ( H100: (N.of_nat (Datatypes.length (RAWBITVECTOR_LIST.map2 orb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)))) = N). rewrite andb_true_iff in Heq11. { destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. specialize (@RAWBITVECTOR_LIST.map2_or_length (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)). intros. rewrite <- H6. now rewrite map_length. apply check_symopp_bvor_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). now rewrite !map_length, Heq11a, Heq11b. } unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. generalize ( BITVECTOR_LIST.of_bits_size (RAWBITVECTOR_LIST.map2 orb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)) ). rewrite H100. rewrite Typ.cast_refl. intros. unfold BITVECTOR_LIST.bv_or, RAWBITVECTOR_LIST.bv_or. unfold RAWBITVECTOR_LIST.size. unfold RAWBITVECTOR_LIST.bits. unfold interp_bv in HSp1, HSp2. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits in HSp1, HSp2. assert ( H101: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs2))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). apply check_symopp_bvor_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). rewrite <- Heq11a in Heq11b. rewrite <- Heq11b in Heq11r. rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp2. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs2) ). rewrite H101. intros. assert ( H102: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs1))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp1. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs1) ). rewrite H102. intros. rewrite Typ.cast_refl in *. rewrite HSp1, HSp2. simpl. apply eq_rec. simpl. rewrite H101, H102. rewrite N.eqb_compare, N.compare_refl. easy. rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). exact Heq11. rewrite Heq10a1, Heq10a2 in *. apply BITVECTOR_LIST.bv_eq_reflect in HSp2. apply BITVECTOR_LIST.bv_eq_reflect in HSp1. assert (interp_form_hatom_bv a1' = interp_bv t_i (interp_atom (t_atom .[a1']))). { rewrite Htia1. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia1. easy. } rewrite H4 in HSp2. rewrite Htia1 in HSp2. assert (interp_form_hatom_bv a2' = interp_bv t_i (interp_atom (t_atom .[a2']))). { rewrite Htia2. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia2. easy. } rewrite H5 in HSp1. simpl in HSp1. rewrite Htia2 in HSp1. apply BITVECTOR_LIST.bv_eq_reflect. unfold Bval, interp_bv. rewrite (@check_symopp_bvor_nl bs1 bs2 bsres N). assert ( H100: (N.of_nat (Datatypes.length (RAWBITVECTOR_LIST.map2 orb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)))) = N). rewrite andb_true_iff in Heq11. { destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. specialize (@RAWBITVECTOR_LIST.map2_or_length (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)). intros. rewrite <- H6. apply check_symopp_bvor_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). now rewrite map_length. apply check_symopp_bvor_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). now rewrite !map_length, Heq11a, Heq11b. } unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. generalize ( BITVECTOR_LIST.of_bits_size (RAWBITVECTOR_LIST.map2 orb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)) ). rewrite H100. rewrite Typ.cast_refl. intros. unfold BITVECTOR_LIST.bv_or, RAWBITVECTOR_LIST.bv_or. unfold RAWBITVECTOR_LIST.size. unfold RAWBITVECTOR_LIST.bits. unfold interp_bv in HSp1, HSp2. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits in HSp1, HSp2. assert ( H101: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs2))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). apply check_symopp_bvor_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). rewrite <- Heq11a in Heq11b. rewrite <- Heq11b in Heq11r. rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp2. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs2) ). rewrite H101. intros. assert ( H102: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs1))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp1. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs1) ). rewrite H102. intros. rewrite Typ.cast_refl in *. rewrite HSp1, HSp2. simpl. apply eq_rec. simpl. rewrite H101, H102. rewrite N.eqb_compare, N.compare_refl. now rewrite RAWBITVECTOR_LIST.map2_or_comm. rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). exact Heq11. - case_eq ((a1 =? a1') && (a2 =? a2') || (a1 =? a2') && (a2 =? a1')); simpl; intros Heq10; try (now apply C.interp_true). case_eq ( check_symopp bs1 bs2 bsres (BO_BVxor N) && (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. unfold Atom.interp_form_hatom_bv at 2, Atom.interp_hatom. rewrite Atom.t_interp_wf; trivial. rewrite Heq9. simpl. rewrite Atom.t_interp_wf; trivial. rewrite Atom.t_interp_wf; trivial. 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. destruct H0. unfold get_type' in H2, H3. unfold v_type in H2, H3. case_eq (t_interp .[ a1']). intros v_typea1 v_vala1 Htia1. rewrite Htia1 in H3. case_eq (t_interp .[ a2']). intros v_typea2 v_vala2 Htia2. rewrite Htia2 in H2. rewrite Atom.t_interp_wf in Htia1; trivial. rewrite Atom.t_interp_wf in Htia2; trivial. unfold apply_binop. rewrite Htia1, Htia2. apply Typ.eqb_spec in H2. apply Typ.eqb_spec in H3. 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 i j Hv. rewrite Hv in H0. now contradict H0. intros i Hv. rewrite Hv in H0. now contradict H0. intros Hv. rewrite Hv in H0. now contradict H0. intros Hv. rewrite Hv in H0. now contradict H0. intros Hv. rewrite Hv in H0. now contradict H0. intros n Hv. rewrite Hv in H0. apply N.eqb_eq in H0. rewrite <- H0 in *. revert v_vala Htia. rewrite Hv. intros v_vala Htia. generalize (Hs pos1). 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. generalize (Hs pos2). intro HSp2. unfold C.valid in HSp2. rewrite Heq2 in HSp2. unfold C.interp in HSp2. unfold existsb in HSp2. rewrite orb_false_r in HSp2. unfold Lit.interp in HSp2. rewrite Heq4 in HSp2. unfold Var.interp in HSp2. rewrite rho_interp in HSp2. rewrite Heq7 in HSp2. simpl in HSp2. revert v_vala1 Htia1 v_vala2 Htia2. rewrite H2, H3. unfold bvtrue. rewrite Typ.cast_refl. intros v_vala1 Htia1 v_vala2 Htia2. rewrite orb_true_iff in Heq10. do 2 rewrite andb_true_iff in Heq10. destruct Heq10 as [Heq10 | Heq10]; destruct Heq10 as (Heq10a1 & Heq10a2); rewrite eqb_spec in Heq10a1, Heq10a2. rewrite Heq10a1, Heq10a2 in *. apply BITVECTOR_LIST.bv_eq_reflect in HSp2. apply BITVECTOR_LIST.bv_eq_reflect in HSp1. assert (interp_form_hatom_bv a1' = interp_bv t_i (interp_atom (t_atom .[a1']))). { 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. rewrite Htia1 in HSp1. assert (interp_form_hatom_bv a2' = interp_bv t_i (interp_atom (t_atom .[a2']))). { rewrite Htia2. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia2. easy. } rewrite H5 in HSp2. simpl in HSp2. rewrite Htia2 in HSp2. apply BITVECTOR_LIST.bv_eq_reflect. unfold Bval, interp_bv. rewrite (@check_symopp_bvxor_nl bs1 bs2 bsres N). assert ( H100: (N.of_nat (Datatypes.length (RAWBITVECTOR_LIST.map2 xorb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)))) = N). rewrite andb_true_iff in Heq11. { destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. specialize (@RAWBITVECTOR_LIST.map2_xor_length (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)). intros. rewrite <- H6. now rewrite map_length. apply check_symopp_bvxor_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). now rewrite !map_length, Heq11a, Heq11b. } unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. generalize ( BITVECTOR_LIST.of_bits_size (RAWBITVECTOR_LIST.map2 xorb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)) ). rewrite H100. rewrite Typ.cast_refl. intros. unfold BITVECTOR_LIST.bv_xor, RAWBITVECTOR_LIST.bv_xor. unfold RAWBITVECTOR_LIST.size. unfold RAWBITVECTOR_LIST.bits. unfold interp_bv in HSp1, HSp2. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits in HSp1, HSp2. assert ( H101: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs2))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). apply check_symopp_bvxor_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). rewrite <- Heq11a in Heq11b. rewrite <- Heq11b in Heq11r. rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp2. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs2) ). rewrite H101. intros. assert ( H102: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs1))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp1. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs1) ). rewrite H102. intros. rewrite Typ.cast_refl in *. rewrite HSp1, HSp2. simpl. apply eq_rec. simpl. rewrite H101, H102. rewrite N.eqb_compare, N.compare_refl. easy. rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). exact Heq11. rewrite Heq10a1, Heq10a2 in *. apply BITVECTOR_LIST.bv_eq_reflect in HSp2. apply BITVECTOR_LIST.bv_eq_reflect in HSp1. assert (interp_form_hatom_bv a1' = interp_bv t_i (interp_atom (t_atom .[a1']))). { rewrite Htia1. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia1. easy. } rewrite H4 in HSp2. rewrite Htia1 in HSp2. assert (interp_form_hatom_bv a2' = interp_bv t_i (interp_atom (t_atom .[a2']))). { rewrite Htia2. unfold Atom.interp_form_hatom_bv. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Htia2. easy. } rewrite H5 in HSp1. simpl in HSp1. rewrite Htia2 in HSp1. apply BITVECTOR_LIST.bv_eq_reflect. unfold Bval, interp_bv. rewrite (@check_symopp_bvxor_nl bs1 bs2 bsres N). assert ( H100: (N.of_nat (Datatypes.length (RAWBITVECTOR_LIST.map2 xorb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)))) = N). rewrite andb_true_iff in Heq11. { destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. specialize (@RAWBITVECTOR_LIST.map2_xor_length (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)). intros. rewrite <- H6. apply check_symopp_bvxor_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). now rewrite map_length. apply check_symopp_bvxor_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). now rewrite !map_length, Heq11a, Heq11b. } unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. generalize ( BITVECTOR_LIST.of_bits_size (RAWBITVECTOR_LIST.map2 xorb (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2)) ). rewrite H100. rewrite Typ.cast_refl. intros. unfold BITVECTOR_LIST.bv_xor, RAWBITVECTOR_LIST.bv_xor. unfold RAWBITVECTOR_LIST.size. unfold RAWBITVECTOR_LIST.bits. unfold interp_bv in HSp1, HSp2. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits in HSp1, HSp2. assert ( H101: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs2))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). apply check_symopp_bvxor_length2 in Heq11. destruct Heq11 as (Heq11a, Heq11b). rewrite <- Heq11a in Heq11b. rewrite <- Heq11b in Heq11r. rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp2. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs2) ). rewrite H101. intros. assert ( H102: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs1))) = N ). { rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). rewrite N.eqb_eq in Heq11r. now rewrite map_length. } revert HSp1. generalize ( BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs1) ). rewrite H102. intros. rewrite Typ.cast_refl in *. rewrite HSp1, HSp2. simpl. apply eq_rec. simpl. rewrite H101, H102. rewrite N.eqb_compare, N.compare_refl. now rewrite RAWBITVECTOR_LIST.map2_xor_comm. rewrite andb_true_iff in Heq11. destruct Heq11 as (Heq11, Heq11r). exact Heq11. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance