proposition: Lemma valid_check_bbUlt pos1 pos2 lres : C.valid rho (check_bbUlt pos1 pos2 lres).
proof: Proof. unfold check_bbUlt. 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 (Bool.eqb (Lit.is_pos a) (Lit.is_pos bsres)); try (intros; now apply C.interp_true). intros Heq12. case_eq (t_form .[ Lit.blit a]); try (intros; now apply C.interp_true). intros a3 Heq10. case_eq (t_atom .[ a3]); try (intros; now apply C.interp_true). intros [ | | | | | | | [ A B | A | | | | ]|N|N|N|N|N|N|N|N| | | | ]; try (intros; now apply C.interp_true). intros a1' a2' Heq9. case_eq ((a1 =? a1') && (a2 =? a2')); simpl; intros Heq15; try (now apply C.interp_true). case_eq (check_ult bs1 bs2 bsres && (N.of_nat (Datatypes.length bs1) =? N)%N && (N.of_nat (Datatypes.length bs2) =? N)%N); simpl; intros Heq16; 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. generalize wt_t_atom. unfold Atom.wt. unfold is_true. rewrite aforallbi_spec;intros. pose proof (H a3). assert (a3 <? 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 H0. unfold v_type in H0. case_eq (t_interp .[ a3]). intros v_typea3 v_vala3 Htia3. rewrite Htia3 in H0. case_eq (v_typea3); intros; rewrite H4 in H0; try (now contradict H0). rename H4 into Hv. 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. 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. simpl in v_vala2, v_vala2. apply Typ.eqb_spec in H2. apply Typ.eqb_spec in H3. rewrite andb_true_iff in Heq15. destruct Heq15 as (Heq15a1 & Heq15a2); rewrite eqb_spec in Heq15a1, Heq15a2 ;rewrite Heq15a1, Heq15a2 in *. assert (interp_form_hatom_bv a1' = interp_bv t_i (interp_atom (t_atom .[a1']))). { rewrite !Atom.t_interp_wf in Htia1; 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 !Atom.t_interp_wf in Htia1; trivial. rewrite Htia1 in HSp1. unfold interp_bv in HSp1. assert (interp_form_hatom_bv a2' = interp_bv t_i (interp_atom (t_atom .[a2']))). { rewrite !Atom.t_interp_wf in Htia2; trivial. 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. unfold interp_bv in HSp2. rewrite !Atom.t_interp_wf in Htia2; trivial. rewrite Htia2 in HSp2. unfold interp_bv in HSp2. generalize dependent v_vala1. generalize dependent v_vala2. rewrite H2, H3. unfold BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. assert ( H100: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs2))) = N ). { rewrite !andb_true_iff in Heq16. destruct Heq16 as ((Heq16a, Heq16b), Heq16c). rewrite N.eqb_eq in Heq16c. now rewrite map_length. } generalize (BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs2)). rewrite H100. assert ( H101: (N.of_nat (Datatypes.length (map (Lit.interp rho) bs1))) = N ). { rewrite !andb_true_iff in Heq16. destruct Heq16 as ((Heq16a, Heq16b), Heq16c). rewrite N.eqb_eq in Heq16b. now rewrite map_length. } generalize (BITVECTOR_LIST.of_bits_size (map (Lit.interp rho) bs1)). rewrite H101. rewrite Typ.cast_refl in *. intros. apply BITVECTOR_LIST.bv_eq_reflect in HSp2. apply BITVECTOR_LIST.bv_eq_reflect in HSp1. apply (@Bool.eqb_true_iff (Lit.interp rho a) (Lit.interp rho bsres)). unfold Lit.interp, Var.interp. rewrite rho_interp. rewrite Heq10. simpl. unfold Atom.interp_form_hatom. unfold Atom.interp_hatom. rewrite !Atom.t_interp_wf; trivial. rewrite Heq9. simpl. rewrite !Atom.t_interp_wf; trivial. rewrite Htia1, Htia2. simpl. rewrite Form.wf_interp_form; trivial. simpl. apply Bool.eqb_prop in Heq12. rewrite Heq12. rewrite HSp1, HSp2. case_eq (Lit.is_pos bsres). intros Hpos. unfold BITVECTOR_LIST.bv_ult. unfold RAWBITVECTOR_LIST.bv_ult, RAWBITVECTOR_LIST.bits. unfold BITVECTOR_LIST.bv, BITVECTOR_LIST.of_bits, RAWBITVECTOR_LIST.of_bits. simpl. unfold RAWBITVECTOR_LIST.size. simpl. rewrite !Typ.N_cast_refl. rewrite !andb_true_iff in Heq16. destruct Heq16 as ((Heq16 & Heq16l) & Heq16r). rewrite N.eqb_eq in Heq16r, Heq16l. rewrite map_length, Heq16l. rewrite H100. rewrite N.eqb_compare. rewrite N.compare_refl. unfold RAWBITVECTOR_LIST.ult_list. specialize (@prop_check_ult (List.rev bs1) (List.rev bs2)). intros. cut ( Datatypes.length (List.rev bs1) = Datatypes.length (List.rev bs2)). intros. specialize (H6 H7). do 2 rewrite <- List.map_rev. rewrite H6. pose proof (rho_interp). specialize (H8 (Lit.blit a)). rewrite Heq10 in H8. simpl in H8. rewrite !rev_length in H7. specialize (@prop_check_ult2 bs1 bs2 bsres H7 Heq16). intros. rewrite H9. simpl. unfold Atom.interp_form_hatom, interp_hatom. simpl. now rewrite prop_lit. rewrite !rev_length. apply (f_equal nat_of_N) in Heq16l. apply (f_equal nat_of_N) in Heq16r. rewrite Nat2N.id in Heq16l, Heq16r. now rewrite Heq16l, Heq16r. intros. rewrite !andb_true_iff in Heq16. destruct Heq16 as ((Heq16 & Heq16l) & Heq16r). rewrite N.eqb_eq in Heq16r, Heq16l. contradict Heq16. unfold check_ult. rewrite H6. 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