proposition: Lemma check_neg_hatom_correct : wt t_i t_func t_atom -> wf t_atom -> default t_atom = Acop CO_xH -> forall h1 h2, check_neg_hatom h1 h2 -> match interp_hatom t_i t_func t_atom h1, interp_hatom t_i t_func t_atom h2 with | Val Typ.Tbool v1, Val Typ.Tbool v2 => v1 = negb v2 | Val _ _, Val _ _ => False end.
proof: Proof. unfold wt; unfold is_true at 1; rewrite aforallbi_spec; intros Hwt Hwf Hdef h1 h2; unfold check_neg_hatom; case_eq (get_atom h1); try discriminate; intros b1 t11 t12 H1; case_eq (get_atom h2); try discriminate; intros b2 t21 t22 H2; assert (H7: h1 <? length t_atom) by (apply PArray.get_not_default_lt; rewrite H1, Hdef; discriminate); generalize (Hwt _ H7); rewrite H1; simpl; generalize H1; case b1; try discriminate; clear H1 b1; simpl; intro H1; case (get_type' t_i (t_interp t_i t_func t_atom) h1); try discriminate; simpl; rewrite andb_true_iff; intros [H30 H31]; change (is_true (Typ.eqb (get_type' t_i (t_interp t_i t_func t_atom) t11) Typ.TZ)) in H30; change (is_true (Typ.eqb (get_type' t_i (t_interp t_i t_func t_atom) t12) Typ.TZ)) in H31; rewrite Typ.eqb_spec in H30, H31; generalize (check_aux_interp_hatom _ t_func _ Hwf t11), (check_aux_interp_hatom _ t_func _ Hwf t12); rewrite H30, H31; intros [v1 Hv1] [v2 Hv2]; generalize H2; case b2; try discriminate; clear H2 b2; intro H2; unfold is_true; rewrite andb_true_iff; intros [H3 H4]; generalize (check_hatom_correct Hwf Hdef _ _ H3), (check_hatom_correct Hwf Hdef _ _ H4); unfold interp_hatom; intros H5 H6; rewrite t_interp_wf; auto; rewrite H1; simpl; rewrite Hv1, Hv2; simpl; rewrite t_interp_wf; auto; rewrite H2; simpl; rewrite <- H5; rewrite <- H6, Hv1, Hv2; simpl. rewrite Z.ltb_antisym; auto. rewrite Z.geb_leb, Z.ltb_antisym; auto. rewrite Z.leb_antisym; auto. rewrite Z.gtb_ltb, Z.leb_antisym; auto. rewrite Z.geb_leb, Z.leb_antisym; auto. rewrite Z.geb_leb, Z.gtb_ltb, Z.leb_antisym; auto. rewrite Z.gtb_ltb, Z.ltb_antisym; auto. rewrite Z.geb_leb, Z.gtb_ltb, Z.ltb_antisym; auto. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList