proposition: Lemma interp_binop_eqb_antisym: forall a b va vb, interp_atom a = Bval t_i Typ.TZ va -> interp_atom b = Bval t_i Typ.TZ vb -> (interp_bool t_i (apply_binop t_i Typ.TZ Typ.TZ Typ.Tbool (Typ.i_eqb t_i Typ.TZ) (interp a) (interp b)) = false) -> negb (interp_bool t_i (apply_binop t_i Typ.TZ Typ.TZ Typ.Tbool Z.leb (interp a) (interp b))) = false -> negb (interp_bool t_i (apply_binop t_i Typ.TZ Typ.TZ Typ.Tbool Z.leb (interp b) (interp a))) = false -> False.
proof: Proof. intros a b va vb HHa HHb. unfold Atom.interp, Atom.interp_hatom. rewrite HHa, HHb; simpl. intros. case_eq (va <=? vb)%Z; intros; subst. case_eq (vb <=? va)%Z; intros; subst. apply Zle_bool_imp_le in H2. apply Zle_bool_imp_le in H3. apply Z.eqb_neq in H. lia. rewrite H3 in H1; simpl in H1; elim diff_true_false; trivial. rewrite H2 in H0; simpl in H1; elim diff_true_false; trivial. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz