Library Stdlib.Structures.OrdersEx

Examples of Ordered Type structures.

Ordered Type for bool, nat, Positive, N, Z, ascii, string with the usual or lexicographic order.
An OrderedType can now directly be seen as a DecidableType

Module OT_as_DT (O:OrderedType) <: DecidableType := O.

(Usual) Decidable Type for bool, nat, positive, N, Z
From two ordered types, we can build a new OrderedType over their cartesian product, using the lexicographic order.

Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
 Include PairDecidableType O1 O2.

 Definition lt :=
   (relation_disjunction (O1.lt @@1) (O1.eq * O2.lt))%signature.

#[global]
 Instance lt_strorder : StrictOrder lt.

#[global]
 Instance lt_compat : Proper (eq==>eq==>iff) lt.

 Definition compare x y :=
  match O1.compare (fst x) (fst y) with
   | Eq => O2.compare (snd x) (snd y)
   | Lt => Lt
   | Gt => Gt
  end.

 Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).

End PairOrderedType.

Even if positive can be seen as an ordered type with respect to the usual order (see above), we can also use a lexicographic order over bits (lower bits are considered first). This is more natural when using positive as indexes for sets or maps (see MSetPositive).

Local Open Scope positive.

Module PositiveOrderedTypeBits <: UsualOrderedType.
  Definition t:=positive.
  Include HasUsualEq <+ UsualIsEq.
  Definition eqb := Pos.eqb.
  Definition eqb_eq := Pos.eqb_eq.
  Include HasEqBool2Dec.

  Fixpoint bits_lt (p q:positive) : Prop :=
   match p, q with
   | xH, xI _ => True
   | xH, _ => False
   | xO p, xO q => bits_lt p q
   | xO _, _ => True
   | xI p, xI q => bits_lt p q
   | xI _, _ => False
   end.

  Definition lt:=bits_lt.

  Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x.

  Lemma bits_lt_trans :
    forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.

#[global]
  Instance lt_compat : Proper (eq==>eq==>iff) lt.

#[global]
  Instance lt_strorder : StrictOrder lt.

  Fixpoint compare x y :=
    match x, y with
      | x~1, y~1 => compare x y
      | _~1, _ => Gt
      | x~0, y~0 => compare x y
      | _~0, _ => Lt
      | 1, _~1 => Lt
      | 1, 1 => Eq
      | 1, _~0 => Gt
    end.

  Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).

End PositiveOrderedTypeBits.

Module Ascii_as_OT <: UsualOrderedType.
  Definition t := ascii.
  Include HasUsualEq <+ UsualIsEq.
  Definition eqb := Ascii.eqb.
  Definition eqb_eq := Ascii.eqb_eq.
  Include HasEqBool2Dec.

  Definition compare (a b : ascii) := N_as_OT.compare (N_of_ascii a) (N_of_ascii b).
  Definition lt (a b : ascii) := N_as_OT.lt (N_of_ascii a) (N_of_ascii b).

#[global]
  Instance lt_compat : Proper (eq==>eq==>iff) lt.

#[global]
  Instance lt_strorder : StrictOrder lt.

  Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
End Ascii_as_OT.

String is an ordered type with respect to the usual lexical order.

Module String_as_OT <: UsualOrderedType.
  Definition t := string.
  Include HasUsualEq <+ UsualIsEq.
  Definition eqb := String.eqb.
  Definition eqb_eq := String.eqb_eq.
  Include HasEqBool2Dec.

  Fixpoint compare (a b : string)
    := match a, b with
       | EmptyString, EmptyString => Eq
       | EmptyString, _ => Lt
       | String _ _, EmptyString => Gt
       | String a_head a_tail, String b_head b_tail =>
         match Ascii_as_OT.compare a_head b_head with
         | Lt => Lt
         | Gt => Gt
         | Eq => compare a_tail b_tail
         end
       end.

  Definition lt (a b : string) := compare a b = Lt.

#[global]
  Instance lt_compat : Proper (eq==>eq==>iff) lt.

  Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).

#[global]
  Instance lt_strorder : StrictOrder lt.
End String_as_OT.