Library Coq.ZArith.ZOrderedType


Require Import BinInt Zcompare Zorder Zbool ZArith_dec
 Equalities Orders OrdersTac.

Local Open Scope Z_scope.

DecidableType structure for binary integers


Module Z_as_UBE <: UsualBoolEq.
 Definition t := Z.
 Definition eq := @eq Z.
 Definition eqb := Zeq_bool.
 Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
End Z_as_UBE.

Module Z_as_DT <: UsualDecidableTypeFull := Make_UDTF Z_as_UBE.

Note that the last module fulfills by subtyping many other interfaces, such as DecidableType or EqualityType.

OrderedType structure for binary integers


Module Z_as_OT <: OrderedTypeFull.
 Include Z_as_DT.
 Definition lt := Zlt.
 Definition le := Zle.
 Definition compare := Zcompare.

 Instance lt_strorder : StrictOrder Zlt.

 Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Zlt.

 Definition le_lteq := Zle_lt_or_eq_iff.
 Definition compare_spec := Zcompare_spec.

End Z_as_OT.

Note that Z_as_OT can also be seen as a UsualOrderedType and a OrderedType (and also as a DecidableType).

An order tactic for integers


Module ZOrder := OTF_to_OrderTac Z_as_OT.
Ltac z_order := ZOrder.order.

Note that z_order is domain-agnostic: it will not prove 1<=2 or x<=x+x, but rather things like x<=y -> y<=x -> x=y.