Library Stdlib.Structures.OrderedTypeEx


From Stdlib Require Import OrderedType.
From Stdlib Require Import BinInt.
From Stdlib Require Import PeanoNat Peano_dec Compare_dec.
From Stdlib Require Import Ascii String.
From Stdlib Require Import NArith Ndec.

Examples of Ordered Type structures.

First, a particular case of OrderedType where the equality is the usual one of Coq.

Module Type UsualOrderedType.
 Parameter Inline t : Type.
 Definition eq := @eq t.
 Parameter Inline lt : t -> t -> Prop.
 Definition eq_refl := @eq_refl t.
 Definition eq_sym := @eq_sym t.
 Definition eq_trans := @eq_trans t.
 Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
 Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 Parameter compare : forall x y : t, Compare lt eq x y.
 Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
End UsualOrderedType.

a UsualOrderedType is in particular an OrderedType.

Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U.

nat is an ordered type with respect to the usual order on natural numbers.

Module Nat_as_OT <: UsualOrderedType.

  Definition t := nat.

  Definition eq := @eq nat.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.

  Definition lt := lt.

  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.

  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.

  Definition compare x y : Compare lt eq x y.

  Definition eq_dec := eq_nat_dec.

End Nat_as_OT.

Z is an ordered type with respect to the usual order on integers.

Local Open Scope Z_scope.

Module Z_as_OT <: UsualOrderedType.

  Definition t := Z.
  Definition eq := @eq Z.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.

  Definition lt (x y:Z) := (x<y).

  Lemma lt_trans : forall x y z, x<y -> y<z -> x<z.

  Lemma lt_not_eq : forall x y, x<y -> ~ x=y.

  Definition compare x y : Compare lt eq x y.

  Definition eq_dec := Z.eq_dec.

End Z_as_OT.

positive is an ordered type with respect to the usual order on natural numbers.

Local Open Scope positive_scope.

Module Positive_as_OT <: UsualOrderedType.
  Definition t:=positive.
  Definition eq:=@eq positive.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.

  Definition lt := Pos.lt.

  Definition lt_trans := Pos.lt_trans.

  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.

  Definition compare x y : Compare lt eq x y.

  Definition eq_dec := Pos.eq_dec.

End Positive_as_OT.

N is an ordered type with respect to the usual order on natural numbers.

Module N_as_OT <: UsualOrderedType.
  Definition t:=N.
  Definition eq:=@eq N.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.

  Definition lt := N.lt.
  Definition lt_trans := N.lt_trans.
  Definition lt_not_eq := N.lt_neq.

  Definition compare x y : Compare lt eq x y.

  Definition eq_dec := N.eq_dec.

End N_as_OT.

From two ordered types, we can build a new OrderedType over their cartesian product, using the lexicographic order.

Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
 Module MO1:=OrderedTypeFacts(O1).
 Module MO2:=OrderedTypeFacts(O2).

 Definition t := prod O1.t O2.t.

 Definition eq x y := O1.eq (fst x) (fst y) /\ O2.eq (snd x) (snd y).

 Definition lt x y :=
    O1.lt (fst x) (fst y) \/
    (O1.eq (fst x) (fst y) /\ O2.lt (snd x) (snd y)).

 Lemma eq_refl : forall x : t, eq x x.

 Lemma eq_sym : forall x y : t, eq x y -> eq y x.

 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.

 Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.

 Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.

 Definition compare : forall x y : t, Compare lt eq x y.
 Defined.

 Definition eq_dec : forall x y : t, {eq x y} + {~ eq 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 FSetPositive and FMapPositive.

Module PositiveOrderedTypeBits <: UsualOrderedType.
  Definition t:=positive.
  Definition eq:=@eq positive.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.

  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_trans :
    forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.

  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.

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

  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.

  Definition compare : forall x y : t, Compare lt eq x y.

  Lemma eq_dec (x y: positive): {x = y} + {x <> y}.

End PositiveOrderedTypeBits.

Module Ascii_as_OT <: UsualOrderedType.
  Definition t := ascii.

  Definition eq := @eq ascii.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.

  Definition cmp : ascii -> ascii -> comparison := Ascii.compare.

  Lemma cmp_eq (a b : ascii):
    cmp a b = Eq <-> a = b.

  Lemma cmp_lt_nat (a b : ascii):
    cmp a b = Lt <-> (nat_of_ascii a < nat_of_ascii b)%nat.

  Lemma cmp_antisym (a b : ascii):
    cmp a b = CompOpp (cmp b a).

  Definition lt (x y : ascii) := (N_of_ascii x < N_of_ascii y)%N.

  Lemma lt_trans (x y z : ascii):
    lt x y -> lt y z -> lt x z.

  Lemma lt_not_eq (x y : ascii):
     lt x y -> x <> y.

  Local Lemma compare_helper_eq {a b : ascii} (E : cmp a b = Eq):
    a = b.

  Local Lemma compare_helper_gt {a b : ascii} (G : cmp a b = Gt):
    lt b a.

  Definition compare (a b : ascii) : Compare lt eq a b :=
    match cmp a b as z return _ = z -> _ with
    | Lt => fun E => LT E
    | Gt => fun E => GT (compare_helper_gt E)
    | Eq => fun E => EQ (compare_helper_eq E)
    end Logic.eq_refl.

  Definition eq_dec (x y : ascii): {x = y} + { ~ (x = y)} := ascii_dec 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.

  Definition eq := @eq string.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.

  Inductive lts : string -> string -> Prop :=
    | lts_empty : forall a s, lts EmptyString (String a s)
    | lts_tail : forall a s1 s2, lts s1 s2 -> lts (String a s1) (String a s2)
    | lts_head : forall (a b : ascii) s1 s2,
        lt (nat_of_ascii a) (nat_of_ascii b) ->
        lts (String a s1) (String b s2).

  Definition lt := lts.

  Lemma nat_of_ascii_inverse a b : nat_of_ascii a = nat_of_ascii b -> a = b.

  Lemma lts_tail_unique a s1 s2 : lt (String a s1) (String a s2) ->
    lt s1 s2.

  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.

  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.

  Definition cmp : string -> string -> comparison := String.compare.

  Lemma cmp_eq (a b : string):
    cmp a b = Eq <-> a = b.
  Lemma cmp_antisym (a b : string):
    cmp a b = CompOpp (cmp b a).

  Lemma cmp_lt (a b : string):
    cmp a b = Lt <-> lt a b.

  Local Lemma compare_helper_lt {a b : string} (L : cmp a b = Lt):
    lt a b.

  Local Lemma compare_helper_gt {a b : string} (G : cmp a b = Gt):
    lt b a.

  Local Lemma compare_helper_eq {a b : string} (E : cmp a b = Eq):
    a = b.

  Definition compare (a b : string) : Compare lt eq a b :=
    match cmp a b as z return _ = z -> _ with
    | Lt => fun E => LT (compare_helper_lt E)
    | Gt => fun E => GT (compare_helper_gt E)
    | Eq => fun E => EQ (compare_helper_eq E)
    end Logic.eq_refl.

  Definition eq_dec (x y : string): {x = y} + { ~ (x = y)} := string_dec x y.
End String_as_OT.