proposition: Lemma check_trans_aux_correct : forall eqs u t1 t2 res c, Typ.eqb (get_type t1) u -> Typ.eqb (get_type t2) u -> Atom.interp_bool t_i (interp (Atom.Abop (Atom.BO_eq u) t1 t2)) \/ C.interp rho c -> C.interp rho (check_trans_aux t1 t2 eqs res c).
proof: Proof. induction eqs;simpl;intros. - apply get_eq_interp;intros. match goal with |- context [if ?b then _ else _] => case_eq b end; intros;trivial with smtcoq_euf. simpl;rewrite Lit.interp_lit;unfold Var.interp. destruct H1;[ | rewrite H1,orb_true_r;auto with smtcoq_euf smtcoq_core]. rewrite orb_true_iff, !andb_true_iff in H7;destruct H7 as [[H7 H8] | [H7 H8]]. rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst. tunicity. subst t. rewrite H4, H1;auto with smtcoq_euf smtcoq_core. rewrite eqb_spec in H7. rewrite eqb_spec in H8. subst. tunicity. subst t;rewrite interp_binop_eqb_sym in H1;rewrite H4, H1;auto with smtcoq_euf smtcoq_core. - apply get_eq_interp;intros. destruct (Misc.reflect_eqb t2 b);subst;tunicity; try subst t. + apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (4:= H1);trivial. rewrite interp_binop_eqb_sym;trivial. + destruct (Misc.reflect_eqb t2 a0); subst;tunicity; try subst t. * apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (4:= H1);trivial. * destruct (Misc.reflect_eqb t1 b);subst;tunicity; try subst t. -- apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (5:= H1);trivial. -- destruct (Misc.reflect_eqb t1 a0);[subst;tunicity;try subst t|auto with smtcoq_euf smtcoq_core]. apply (IHeqs u);trivial. simpl;unfold is_true;rewrite orb_true_iff. rewrite Lit.interp_nlit;unfold Var.interp. case_eq (rho (Lit.blit a));[rewrite H4; intros | simpl;auto]. destruct H1;[left | auto]. apply interp_binop_eqb_trans with (5:= H1);trivial. rewrite interp_binop_eqb_sym;trivial. Qed.
imports: Bool List Int63 PArray State SMT_terms