proposition: Lemma check_aux_interp_aux_contr_aux : forall a, (forall T, check_aux get_type a T = false) -> interp_aux a = bvtrue.
proof: Proof. intros [op | op h | op h1 h2 | op h1 h2 h3 | op ha | f l]; simpl. destruct op; simpl; intro H. discriminate (H Typ.Tpositive). discriminate (H Typ.TZ). specialize (H (Typ.TBV n)). simpl in H. rewrite N.eqb_refl in H. now contradict H. destruct op; simpl; intro H; destruct (check_aux_interp_hatom h) as [v Hv]; rewrite Hv; simpl; rewrite Typ.neq_cast; try (pose (H2 := H Typ.Tpositive); simpl in H2; rewrite H2; auto); try (pose (H2 := H Typ.TZ); simpl in H2; rewrite H2; auto); try (pose (H2 := H Typ.Tbool); simpl in H2; rewrite H2; auto); try (pose (H2 := H Typ.TBV); simpl in H2; rewrite H2; auto). specialize (H (Typ.TBV n)). simpl in H. rewrite andb_false_iff in H. destruct H as [ H | H]. rewrite N.eqb_refl in H. now contradict H. now rewrite H. specialize (H (Typ.TBV n)). simpl in H. rewrite andb_false_iff in H. destruct H as [ H | H]. rewrite N.eqb_refl in H. now contradict H. now rewrite H. specialize (H (Typ.TBV n0)). simpl in H. rewrite andb_false_iff in H. destruct H as [ H | H]. rewrite N.eqb_refl in H. now contradict H. now rewrite H. specialize (H (Typ.TBV (i + n))). simpl in H. rewrite andb_false_iff in H. destruct H as [ H | H]. rewrite N.eqb_refl in H. now contradict H. now rewrite H. specialize (H (Typ.TBV (i + n))). simpl in H. rewrite andb_false_iff in H. destruct H as [ H | H]. rewrite N.eqb_refl in H. now contradict H. now rewrite H. destruct op; simpl; intro H; destruct (check_aux_interp_hatom h1) as [v1 Hv1]; destruct (check_aux_interp_hatom h2) as [v2 Hv2]; rewrite Hv1, Hv2; simpl; try (pose (H2 := H Typ.TZ); simpl in H2; rewrite andb_false_iff in H2; destruct H2 as [H2|H2]; [rewrite (Typ.neq_cast (get_type h1)), H2|rewrite (Typ.neq_cast (get_type h2)), H2; case (Typ.cast (get_type h1) Typ.TZ)]; auto); try (pose (H2 := H Typ.Tbool); simpl in H2; rewrite andb_false_iff in H2; destruct H2 as [H2|H2]; [rewrite (Typ.neq_cast (get_type h1)), H2|rewrite (Typ.neq_cast (get_type h2)), H2; case (Typ.cast (get_type h1) Typ.TZ)]; auto); try (pose (H2 := H Typ.TBV); simpl in H2; rewrite !andb_false_iff in H2; destruct H2 as [[H2|H2]|H2]; [rewrite N.eqb_refl in H2; discriminate | rewrite (Typ.neq_cast (get_type h1)), H2|rewrite (Typ.neq_cast (get_type h2)), H2; case (Typ.cast (get_type h1) Typ.TBV); case (Typ.cast (get_type h1) Typ.TBV)]; auto). intros. simpl in H. case_eq (Typ.cast (get_type h1) t). easy. easy. case_eq (Typ.cast (get_type h1) t). easy. easy. specialize (H (Typ.TBV n)). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. rewrite andb_false_iff in H. destruct H as [ H | H ]. rewrite N.eqb_refl in H. now contradict H. apply Typ.cast_diff in H. now rewrite H. apply Typ.cast_diff in H. rewrite H. case (Typ.cast (get_type h1) (Typ.TBV n)); auto. specialize (H (Typ.TBV n)). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. rewrite andb_false_iff in H. destruct H as [ H | H ]. rewrite N.eqb_refl in H. now contradict H. apply Typ.cast_diff in H. now rewrite H. apply Typ.cast_diff in H. rewrite H. case (Typ.cast (get_type h1) (Typ.TBV n)); auto. specialize (H (Typ.TBV n)). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. rewrite andb_false_iff in H. destruct H as [ H | H ]. rewrite N.eqb_refl in H. now contradict H. apply Typ.cast_diff in H. now rewrite H. apply Typ.cast_diff in H. rewrite H. case (Typ.cast (get_type h1) (Typ.TBV n)); auto. specialize (H (Typ.TBV n)). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. rewrite andb_false_iff in H. destruct H as [ H | H ]. rewrite N.eqb_refl in H. now contradict H. apply Typ.cast_diff in H. now rewrite H. apply Typ.cast_diff in H. rewrite H. case (Typ.cast (get_type h1) (Typ.TBV n)); auto. specialize (H (Typ.TBV n)). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. rewrite andb_false_iff in H. destruct H as [ H | H ]. rewrite N.eqb_refl in H. now contradict H. apply Typ.cast_diff in H. now rewrite H. apply Typ.cast_diff in H. rewrite H. case (Typ.cast (get_type h1) (Typ.TBV n)); auto. specialize (H Typ.Tbool). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. specialize (H0 H). now rewrite H0. case_eq (Typ.cast (get_type h1) (Typ.TBV n)). intros. specialize (@Typ.cast_diff (get_type h2) (Typ.TBV n)). intros. specialize (H1 H). easy. easy. case_eq (Typ.cast (get_type h1) (Typ.TBV n)). intros. specialize (@Typ.cast_diff (get_type h2) (Typ.TBV n)). intros. specialize (H1 H2). easy. easy. specialize (H Typ.Tbool). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. specialize (H0 H). now rewrite H0. case_eq (Typ.cast (get_type h1) (Typ.TBV n)). intros. specialize (@Typ.cast_diff (get_type h2) (Typ.TBV n)). intros. specialize (H1 H). easy. easy. case_eq (Typ.cast (get_type h1) (Typ.TBV n)). intros. specialize (@Typ.cast_diff (get_type h2) (Typ.TBV n)). intros. specialize (H1 H2). easy. easy. specialize (H (Typ.TBV (n+n0))). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. rewrite andb_false_iff in H. destruct H as [ H | H ]. rewrite N.eqb_refl in H. now contradict H. apply Typ.cast_diff in H. now rewrite H. apply Typ.cast_diff in H. rewrite H. case (Typ.cast (get_type h1) (Typ.TBV n)); auto. specialize (H (Typ.TBV n)). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. rewrite andb_false_iff in H. destruct H as [ H | H ]. rewrite N.eqb_refl in H. now contradict H. apply Typ.cast_diff in H. now rewrite H. apply Typ.cast_diff in H. rewrite H. case (Typ.cast (get_type h1) (Typ.TBV n)); auto. specialize (H (Typ.TBV n)). simpl in H. apply andb_false_iff in H. destruct H. specialize (@Typ.cast_diff (get_type h1) (Typ.TBV n)). intros. rewrite andb_false_iff in H. destruct H as [ H | H ]. rewrite N.eqb_refl in H. now contradict H. apply Typ.cast_diff in H. now rewrite H. apply Typ.cast_diff in H. rewrite H. case (Typ.cast (get_type h1) (Typ.TBV n)); auto. specialize (H t0). simpl in H. rewrite !andb_false_iff in H. destruct H. destruct H. rewrite Typ.eqb_refl in H. now contradict H. rewrite (Typ.cast_diff _ _ H); auto. rewrite (Typ.cast_diff _ _ H); auto. case (Typ.cast (get_type h1) (Typ.TFArray t t0)); auto. specialize (H t). simpl in H. rewrite !andb_false_iff in H. destruct H. destruct H. rewrite Typ.eqb_refl in H. now contradict H. rewrite (Typ.cast_diff _ _ H); auto. rewrite (Typ.cast_diff _ _ H); auto. case (Typ.cast (get_type h1) (Typ.TFArray t t0)); auto. destruct op; simpl; intro H; destruct (check_aux_interp_hatom h1) as [v1 Hv1]; destruct (check_aux_interp_hatom h2) as [v2 Hv2]; destruct (check_aux_interp_hatom h3) as [v3 Hv3]; rewrite Hv1, Hv2, Hv3; simpl. specialize (H (Typ.TFArray t t0)). simpl in H. rewrite !andb_false_iff in H. destruct H as [[ [ [ H | H] | H] | H] | H]; try (rewrite (Typ.cast_diff _ _ H); auto); try (case (Typ.cast (get_type h1) (Typ.TFArray t t0)); auto); try (rewrite !Typ.eqb_refl in H; now contradict H). intros. case (Typ.cast (get_type h2) t); auto. destruct op as [A]; simpl; intro H; generalize (H Typ.Tbool); simpl; clear H; assert (H: forall l1, List.forallb (fun t1 : int => Typ.eqb (get_type t1) A) ha = false -> match compute_interp A l1 ha with | Some l => Bval Typ.Tbool (distinct (Typ.i_eqb t_i A) (rev l)) | None => bvtrue end = bvtrue). induction ha as [ |h ha Iha]; simpl. intros; discriminate. intro l1; destruct (check_aux_interp_hatom h) as [vh Hh]; case_eq (Typ.eqb (get_type h) A); simpl. change (Typ.eqb (get_type h) A = true) with (is_true (Typ.eqb (get_type h) A)); rewrite Typ.eqb_spec; intro; subst A; intro H; rewrite Hh; simpl; rewrite Typ.cast_refl; apply Iha; auto. intros H _; rewrite Hh; simpl; rewrite (Typ.cast_diff _ _ H); auto. apply H. apply check_args_interp_aux_contr. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList