proposition: Lemma check_aux_interp_aux_aux : forall a t, check_aux get_type a t -> exists v, interp_aux a = (Bval t v).
proof: Proof. intros [op|op h|op h1 h2|op h1 h2 h3|op ha|f l]; simpl. destruct op as [ | |l n]; intros [ | i | | | |size]; simpl; try discriminate. exists 1%positive; auto. exists 0%Z; auto. intros H. exists (BITVECTOR_LIST._of_bits l size). unfold is_true in H. rewrite N.eqb_eq in H. now rewrite H. destruct op as [ | | | | |n n0|n|n|n n0 n1|n n0|n n0]; intros [ | ind| | | |size]; simpl; try discriminate; try rewrite Typ.eqb_spec; intros H1a; destruct (check_aux_interp_hatom h) as [x Hx]; rewrite Hx; simpl; generalize x Hx; try rewrite H1a; intros y Hy; try rewrite Typ.cast_refl. exists (y~0)%positive; auto. exists (y~1)%positive; auto. exists (Zpos y); auto. exists (Zneg y); auto. exists (- y)%Z; auto. exists (BITVECTOR_LIST.bitOf n0 y); auto. intros. apply andb_true_iff in H1a. destruct H1a as (Ha, Hb). rewrite N.eqb_eq in Ha. revert x y Hx Hy Hb. rewrite <- Ha in *. intros. apply Typ.eqb_spec in Hb. revert x y Hx Hy. rewrite Hb. intros. exists (@BITVECTOR_LIST.bv_not n y); auto. rewrite Typ.cast_refl; auto. intros. apply andb_true_iff in H1a. destruct H1a as (Ha, Hb). rewrite N.eqb_eq in Ha. revert x y Hx Hy Hb. rewrite <- Ha in *. intros. apply Typ.eqb_spec in Hb. revert x y Hx Hy. rewrite Hb. intros. exists (@BITVECTOR_LIST.bv_neg n y); auto. rewrite Typ.cast_refl; auto. intros. apply andb_true_iff in H1a. destruct H1a as (Ha, Hb). rewrite N.eqb_eq in Ha. revert x y Hx Hy Hb. rewrite <- Ha in *. intros. apply Typ.eqb_spec in Hb. revert x y Hx Hy. rewrite Hb. intros. exists (@BITVECTOR_LIST.bv_extr n n0 n1 y); auto. rewrite Typ.cast_refl; auto. intros. apply andb_true_iff in H1a. destruct H1a as (Ha, Hb). rewrite N.eqb_eq in Ha. revert x y Hx Hy Hb. rewrite <- Ha in *. intros. apply Typ.eqb_spec in Hb. revert x y Hx Hy. rewrite Hb. intros. exists (@BITVECTOR_LIST.bv_zextn n n0 y); auto. rewrite Typ.cast_refl; auto. intros. apply andb_true_iff in H1a. destruct H1a as (Ha, Hb). rewrite N.eqb_eq in Ha. revert x y Hx Hy Hb. rewrite <- Ha in *. intros. apply Typ.eqb_spec in Hb. revert x y Hx Hy. rewrite Hb. intros. exists (@BITVECTOR_LIST.bv_sextn n n0 y); auto. rewrite Typ.cast_refl; auto. destruct op as [ | | | | | | | A |s1|s2| s3 | s4 | s6 | s7 | s8 | s9 | s10 | n m | ti te | ti te]; [ intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | intros [ ti' te' | i | | | |s ] | | ]; simpl; try discriminate; unfold is_true; try (rewrite andb_true_iff ;change (Typ.eqb (get_type h1) Typ.TZ = true /\ Typ.eqb (get_type h2) Typ.TZ = true) with (is_true (Typ.eqb (get_type h1) Typ.TZ) /\ is_true (Typ.eqb (get_type h2) Typ.TZ)); rewrite !Typ.eqb_spec; intros [H1 H2]; destruct (check_aux_interp_hatom h1) as [x1 Hx1]; rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl; generalize x1 Hx1 x2 Hx2; rewrite H1, H2; intros y1 Hy1 y2 Hy2; rewrite !Typ.cast_refl); try (change (Typ.eqb (get_type h1) Typ.TBV = true /\ Typ.eqb (get_type h2) Typ.TBV = true) with (is_true (Typ.eqb (get_type h1) Typ.TBV) /\ is_true (Typ.eqb (get_type h2) Typ.TBV)); rewrite !Typ.eqb_spec; intros [H1 H2]; destruct (check_aux_interp_hatom h1) as [x1 Hx1]; rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl; generalize x1 Hx1 x2 Hx2; rewrite H1, H2; intros y1 Hy1 y2 Hy2; rewrite !Typ.cast_refl). exists (y1 + y2)%Z; auto. exists (y1 - y2)%Z; auto. exists (y1 * y2)%Z; auto. exists (y1 <? y2)%Z; auto. exists (y1 <=? y2)%Z; auto. exists (y1 >=? y2)%Z; auto. exists (y1 >? y2)%Z; auto. rewrite andb_true_iff ; change (Typ.eqb (get_type h1) A = true /\ Typ.eqb (get_type h2) A = true) with (is_true (Typ.eqb (get_type h1) A) /\ is_true (Typ.eqb (get_type h2) A)); rewrite !Typ.eqb_spec; intros [H1 H2]; destruct (check_aux_interp_hatom h1) as [x1 Hx1]; rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl; generalize x1 Hx1 x2 Hx2; rewrite H1, H2; intros y1 Hy1 y2 Hy2; rewrite !Typ.cast_refl; exists (Typ.i_eqb t_i A y1 y2); auto. simpl in s. intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). apply Typ.eqb_spec in Hb. apply Typ.eqb_spec in Hc. rewrite N.eqb_eq in Ha. revert Hb Hc. rewrite Ha in *. intros. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. revert x1 Hx1 x2 Hx2. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite Typ.cast_refl. exists (BITVECTOR_LIST.bv_and y1 y2); auto. simpl in s. intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). apply Typ.eqb_spec in Hb. apply Typ.eqb_spec in Hc. rewrite N.eqb_eq in Ha. revert Hb Hc. rewrite Ha in *. intros. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. revert x1 Hx1 x2 Hx2. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite Typ.cast_refl. exists (BITVECTOR_LIST.bv_or y1 y2); auto. simpl in s. intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). apply Typ.eqb_spec in Hb. apply Typ.eqb_spec in Hc. rewrite N.eqb_eq in Ha. revert Hb Hc. rewrite Ha in *. intros. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. revert x1 Hx1 x2 Hx2. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite Typ.cast_refl. exists (BITVECTOR_LIST.bv_xor y1 y2); auto. simpl in s. intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). apply Typ.eqb_spec in Hb. apply Typ.eqb_spec in Hc. rewrite N.eqb_eq in Ha. revert Hb Hc. rewrite Ha in *. intros. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. revert x1 Hx1 x2 Hx2. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite Typ.cast_refl. exists (BITVECTOR_LIST.bv_add y1 y2); auto. simpl in s. intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). apply Typ.eqb_spec in Hb. apply Typ.eqb_spec in Hc. rewrite N.eqb_eq in Ha. revert Hb Hc. rewrite Ha in *. intros. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. revert x1 Hx1 x2 Hx2. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite Typ.cast_refl. exists (BITVECTOR_LIST.bv_mult y1 y2); auto. intros. rewrite !andb_true_iff in H. destruct H as (Hb, Hc). apply Typ.eqb_spec in Hb. apply Typ.eqb_spec in Hc. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. revert x1 Hx1 x2 Hx2. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite Typ.cast_refl. exists (BITVECTOR_LIST.bv_ult y1 y2); auto. intros. rewrite !andb_true_iff in H. destruct H as (Hb, Hc). apply Typ.eqb_spec in Hb. apply Typ.eqb_spec in Hc. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. revert x1 Hx1 x2 Hx2. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite Typ.cast_refl. exists (BITVECTOR_LIST.bv_slt y1 y2); auto. intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). apply N.eqb_eq in Ha. apply Typ.eqb_spec in Hb. apply Typ.eqb_spec in Hc. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. revert x1 Hx1 x2 Hx2. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite !Typ.cast_refl. rewrite <- Ha. exists (BITVECTOR_LIST.bv_concat y1 y2); auto. simpl in s. intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). apply Typ.eqb_spec in Hb. apply Typ.eqb_spec in Hc. rewrite N.eqb_eq in Ha. revert Hb Hc. rewrite Ha in *. intros. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. revert x1 Hx1 x2 Hx2. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite Typ.cast_refl. exists (BITVECTOR_LIST.bv_shl y1 y2); auto. simpl in s. intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). apply Typ.eqb_spec in Hb. apply Typ.eqb_spec in Hc. rewrite N.eqb_eq in Ha. revert Hb Hc. rewrite Ha in *. intros. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. revert x1 Hx1 x2 Hx2. rewrite Hb, Hc. intros y1 Hy1 y2 Hy2. rewrite Typ.cast_refl. exists (BITVECTOR_LIST.bv_shr y1 y2); auto. intros t' H. rewrite !andb_true_iff in H. destruct H as ((H1, H2), H3). destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. apply Typ.eqb_spec in H1. apply Typ.eqb_spec in H2. apply Typ.eqb_spec in H3. revert x1 Hx1 x2 Hx2. rewrite H2, H3, H1. rewrite !Typ.cast_refl. intros. exists (FArray.select x1 x2); auto. intros t' H. rewrite !andb_true_iff in H. destruct H as ((H1, H2), H3). destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; simpl. apply Typ.eqb_spec in H1. apply Typ.eqb_spec in H2. apply Typ.eqb_spec in H3. revert x1 Hx1 x2 Hx2. rewrite H2, H3, H1. rewrite !Typ.cast_refl. intros. exists ((@FArray.diff (Typ.interp t_i t') (Typ.interp t_i te) (Typ.dec_interp t_i t') (Typ.ord_interp t_i t') (Typ.comp_interp t_i t') (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i t') (Typ.inh_interp t_i te) x1 x2)); auto. destruct op as [ti te]; intros [ ti' te' | | | | | ]; simpl; try discriminate; unfold is_true. intros H. rewrite !andb_true_iff in H. destruct H as ((((H1, H2), H3), H4), H5). apply Typ.eqb_spec in H1. apply Typ.eqb_spec in H2. apply Typ.eqb_spec in H3. apply Typ.eqb_spec in H4. apply Typ.eqb_spec in H5. destruct (check_aux_interp_hatom h1) as [x1 Hx1]. rewrite Hx1; destruct (check_aux_interp_hatom h2) as [x2 Hx2]; rewrite Hx2; destruct (check_aux_interp_hatom h3) as [x3 Hx3]; rewrite Hx3; simpl. revert x1 Hx1 x2 Hx2 x3 Hx3. rewrite H3, H4, H5, H1, H2. intros. rewrite !Typ.cast_refl. intros. exists (@FArray.store (Typ.interp t_i ti') (Typ.interp t_i te') (Typ.dec_interp t_i ti') (Typ.ord_interp t_i ti') (Typ.comp_interp t_i ti') (Typ.ord_interp t_i te') (Typ.comp_interp t_i te') (Typ.inh_interp t_i te') x1 x2 x3); auto. destruct op as [A]; simpl; intros [ | | | | | ]; try discriminate; simpl; intros _; case (compute_interp A nil ha). intro l; exists (distinct (Typ.i_eqb t_i A) (rev l)); auto. exists true; auto. intro t; apply check_args_interp_aux. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList