proposition: Lemma compute_interp_spec : forall ty l acc, match compute_interp ty acc l with | Some l' => forall i j, In2 i j l' <-> (In2 i j acc \/ (List.In j acc /\ exists a, List.In a l /\ interp_hatom a = Bval ty i) \/ (exists a b, In2 b a l /\ interp_hatom a = Bval ty i /\ interp_hatom b = Bval ty j)) | None => exists a, List.In a l /\ let (ta,_) := interp_hatom a in ta <> ty end.
proof: Proof. intro ty; induction l as [ |a q IHq]; simpl. intros acc i; split. intro H; left; auto. intros [H|[[_ [a [H _]]]|[a [b [H _]]]]]; auto. elim H. inversion H. intro acc; case_eq (interp_hatom a); intros ta va Heq; rewrite Typ.neq_cast; case_eq (Typ.eqb ta ty). change (Typ.eqb ta ty = true) with (is_true (Typ.eqb ta ty)); rewrite Typ.eqb_spec; intro; subst ta; rewrite Typ.cast_refl; generalize (IHq (va :: acc)); clear IHq; case (compute_interp ty (va :: acc) q). intros l IH i j; rewrite (IH i j); clear IH; split. intros [H|[[H [b [H1 H2]]]|[b [c [H [H1 H2]]]]]]. inversion H; clear H. subst i l0; right; left; split; auto; exists a; split; auto. subst k l0; left; auto. inversion H; clear H. subst va; right; right; exists b; exists a; repeat split; auto; constructor 1; auto. right; left; split; auto; exists b; auto. right; right; exists b; exists c; repeat split; auto; constructor 2; auto. intros [H|[[H [b [[H1|H1] H2]]]|[b [c [H [H1 H2]]]]]]. left; constructor 2; auto. subst b; rewrite Heq in H2; generalize (Bval_inj2 _ _ _ H2); intro; subst va; left; constructor; auto. right; left; split. constructor 2; auto. exists b; auto. inversion H; clear H. subst c l0; rewrite Heq in H2; generalize (Bval_inj2 _ _ _ H2); intro; subst va; right; left; split. constructor 1; auto. exists b; auto. subst k l0; right; right; exists b; exists c; auto. intros [a1 [H1 H2]]; exists a1; split; auto. intro H; exists a; split; auto; rewrite Heq; intro H1; subst ta; rewrite Typ.eqb_refl in H; discriminate. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList