Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import OrderedType.
Require Import ZArith.
Require Import PeanoNat.
Require Import Ascii String.
Require Import Omega.
Require Import NArith Ndec.
Require Import Compare_dec.

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.forall x y z : t, lt x y -> lt y z -> lt x z
  Proof.forall x y z : t, lt x y -> lt y z -> lt x z unfold lt; intros; apply lt_trans with y; auto. Qed.

  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.forall x y : t, lt x y -> ~ eq x y
  Proof.forall x y : t, lt x y -> ~ eq x y unfold lt, eq; intros; omega. Qed.

  Definition compare x y : Compare lt eq x y.x, y:nat
Compare lt eq x y
  Proof.x, y:nat
Compare lt eq x y
    case_eq (Nat.compare x y); intro.x, y:nat
H:(x ?= y) = Eq
Compare lt eq x y
x, y:nat
H:(x ?= y) = Lt
Compare lt eq x y
x, y:nat
H:(x ?= y) = Gt
Compare lt eq x y
    -x, y:nat
H:(x ?= y) = Eq
Compare lt eq x y apply EQ.x, y:nat
H:(x ?= y) = Eq
eq x y now apply nat_compare_eq.
    -x, y:nat
H:(x ?= y) = Lt
Compare lt eq x y apply LT.x, y:nat
H:(x ?= y) = Lt
lt x y now apply nat_compare_Lt_lt.
    -x, y:nat
H:(x ?= y) = Gt
Compare lt eq x y apply GT.x, y:nat
H:(x ?= y) = Gt
lt y x now apply nat_compare_Gt_gt.
  Defined.

  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.forall x y z : Z, x < y -> y < z -> x < z
  Proof.forall x y z : Z, x < y -> y < z -> x < z intros; omega. Qed.

  Lemma lt_not_eq : forall x y, x<y -> ~ x=y.forall x y : Z, x < y -> x <> y
  Proof.forall x y : Z, x < y -> x <> y intros; omega. Qed.

  Definition compare x y : Compare lt eq x y.x, y:Z
Compare lt eq x y
  Proof.x, y:Z
Compare lt eq x y
    case_eq (x ?= y); intro.x, y:Z
H:(x ?= y) = Eq
Compare lt eq x y
x, y:Z
H:(x ?= y) = Lt
Compare lt eq x y
x, y:Z
H:(x ?= y) = Gt
Compare lt eq x y
    -x, y:Z
H:(x ?= y) = Eq
Compare lt eq x y apply EQ.x, y:Z
H:(x ?= y) = Eq
eq x y now apply Z.compare_eq.
    -x, y:Z
H:(x ?= y) = Lt
Compare lt eq x y apply LT.x, y:Z
H:(x ?= y) = Lt
lt x y assumption.
    -x, y:Z
H:(x ?= y) = Gt
Compare lt eq x y apply GT.x, y:Z
H:(x ?= y) = Gt
lt y x now apply Z.gt_lt.
  Defined.

  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.forall x y : t, lt x y -> ~ eq x y
  Proof.forall x y : t, lt x y -> ~ eq x y
  intros x y H.x, y:t
H:lt x y
~ eq x y contradict H.x, y:t
H:eq x y
~ lt x y rewrite H.x, y:t
H:eq x y
~ lt y y apply Pos.lt_irrefl.
  Qed.

  Definition compare x y : Compare lt eq x y.x, y:positive
Compare lt eq x y
  Proof.x, y:positive
Compare lt eq x y
  case_eq (x ?= y); intros H.x, y:positive
H:(x ?= y) = Eq
Compare lt eq x y
x, y:positive
H:(x ?= y) = Lt
Compare lt eq x y
x, y:positive
H:(x ?= y) = Gt
Compare lt eq x y
  -x, y:positive
H:(x ?= y) = Eq
Compare lt eq x y apply EQ.x, y:positive
H:(x ?= y) = Eq
eq x y now apply Pos.compare_eq.
  -x, y:positive
H:(x ?= y) = Lt
Compare lt eq x y apply LT; assumption.
  -x, y:positive
H:(x ?= y) = Gt
Compare lt eq x y apply GT.x, y:positive
H:(x ?= y) = Gt
lt y x now apply Pos.gt_lt.
  Defined.

  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.x, y:N
Compare lt eq x y
  Proof.x, y:N
Compare lt eq x y
  case_eq (x ?= y)%N; intro.x, y:N
H:(x ?= y)%N = Eq
Compare lt eq x y
x, y:N
H:(x ?= y)%N = Lt
Compare lt eq x y
x, y:N
H:(x ?= y)%N = Gt
Compare lt eq x y
  -x, y:N
H:(x ?= y)%N = Eq
Compare lt eq x y apply EQ.x, y:N
H:(x ?= y)%N = Eq
eq x y now apply N.compare_eq.
  -x, y:N
H:(x ?= y)%N = Lt
Compare lt eq x y apply LT.x, y:N
H:(x ?= y)%N = Lt
lt x y assumption.
  -x, y:N
H:(x ?= y)%N = Gt
Compare lt eq x y apply GT.x, y:N
H:(x ?= y)%N = Gt
lt y x now apply N.gt_lt.
  Defined.

  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.forall x : t, eq x x
 Proof.forall x : t, eq x x
 intros (x1,x2); red; simpl; auto.
 Qed.

 Lemma eq_sym : forall x y : t, eq x y -> eq y x.forall x y : t, eq x y -> eq y x
 Proof.forall x y : t, eq x y -> eq y x
 intros (x1,x2) (y1,y2); unfold eq; simpl; intuition.
 Qed.

 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.forall x y z : t, eq x y -> eq y z -> eq x z
 Proof.forall x y z : t, eq x y -> eq y z -> eq x z
 intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto.
 Qed.

 Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.forall x y z : t, lt x y -> lt y z -> lt x z
 Proof.forall x y z : t, lt x y -> lt y z -> lt x z
 intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition.x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
z1:O1.t
z2:O2.t
H1:O1.lt x1 y1
H:O1.lt y1 z1
O1.lt x1 z1 \/ O1.eq x1 z1 /\ O2.lt x2 z2
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
z1:O1.t
z2:O2.t
H1:O1.lt x1 y1
H0:O1.eq y1 z1
H2:O2.lt y2 z2
O1.lt x1 z1 \/ O1.eq x1 z1 /\ O2.lt x2 z2
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
z1:O1.t
z2:O2.t
H:O1.eq x1 y1
H2:O2.lt x2 y2
H1:O1.lt y1 z1
O1.lt x1 z1 \/ O1.eq x1 z1 /\ O2.lt x2 z2
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
z1:O1.t
z2:O2.t
H:O1.eq x1 y1
H2:O2.lt x2 y2
H0:O1.eq y1 z1
H3:O2.lt y2 z2
O1.lt x1 z1 \/ O1.eq x1 z1 /\ O2.lt x2 z2
 left; eauto.x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
z1:O1.t
z2:O2.t
H1:O1.lt x1 y1
H0:O1.eq y1 z1
H2:O2.lt y2 z2
O1.lt x1 z1 \/ O1.eq x1 z1 /\ O2.lt x2 z2
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
z1:O1.t
z2:O2.t
H:O1.eq x1 y1
H2:O2.lt x2 y2
H1:O1.lt y1 z1
O1.lt x1 z1 \/ O1.eq x1 z1 /\ O2.lt x2 z2
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
z1:O1.t
z2:O2.t
H:O1.eq x1 y1
H2:O2.lt x2 y2
H0:O1.eq y1 z1
H3:O2.lt y2 z2
O1.lt x1 z1 \/ O1.eq x1 z1 /\ O2.lt x2 z2
 left; eapply MO1.lt_eq; eauto.x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
z1:O1.t
z2:O2.t
H:O1.eq x1 y1
H2:O2.lt x2 y2
H1:O1.lt y1 z1
O1.lt x1 z1 \/ O1.eq x1 z1 /\ O2.lt x2 z2
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
z1:O1.t
z2:O2.t
H:O1.eq x1 y1
H2:O2.lt x2 y2
H0:O1.eq y1 z1
H3:O2.lt y2 z2
O1.lt x1 z1 \/ O1.eq x1 z1 /\ O2.lt x2 z2
 left; eapply MO1.eq_lt; eauto.x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
z1:O1.t
z2:O2.t
H:O1.eq x1 y1
H2:O2.lt x2 y2
H0:O1.eq y1 z1
H3:O2.lt y2 z2
O1.lt x1 z1 \/ O1.eq x1 z1 /\ O2.lt x2 z2
 right; split; eauto.
 Qed.

 Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.forall x y : t, lt x y -> ~ eq x y
 Proof.forall x y : t, lt x y -> ~ eq x y
 intros (x1,x2) (y1,y2); unfold eq, lt; simpl; intuition.x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
H1:O1.eq x1 y1
H2:O2.eq x2 y2
H0:O1.lt x1 y1
False
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
H1:O1.eq x1 y1
H2:O2.eq x2 y2
H:O1.eq x1 y1
H3:O2.lt x2 y2
False
 apply (O1.lt_not_eq H0 H1).x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
H1:O1.eq x1 y1
H2:O2.eq x2 y2
H:O1.eq x1 y1
H3:O2.lt x2 y2
False
 apply (O2.lt_not_eq H3 H2).
 Qed.

 Definition compare : forall x y : t, Compare lt eq x y.forall x y : t, Compare lt eq x y
 intros (x1,x2) (y1,y2).x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
Compare lt eq (x1, x2) (y1, y2)
 destruct (O1.compare x1 y1).x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
l:O1.lt x1 y1
Compare lt eq (x1, x2) (y1, y2)
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
e:O1.eq x1 y1
Compare lt eq (x1, x2) (y1, y2)
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
l:O1.lt y1 x1
Compare lt eq (x1, x2) (y1, y2)
 apply LT; unfold lt; auto.x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
e:O1.eq x1 y1
Compare lt eq (x1, x2) (y1, y2)
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
l:O1.lt y1 x1
Compare lt eq (x1, x2) (y1, y2)
 destruct (O2.compare x2 y2).x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
e:O1.eq x1 y1
l:O2.lt x2 y2
Compare lt eq (x1, x2) (y1, y2)
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
e:O1.eq x1 y1
e0:O2.eq x2 y2
Compare lt eq (x1, x2) (y1, y2)
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
e:O1.eq x1 y1
l:O2.lt y2 x2
Compare lt eq (x1, x2) (y1, y2)
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
l:O1.lt y1 x1
Compare lt eq (x1, x2) (y1, y2)
 apply LT; unfold lt; auto.x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
e:O1.eq x1 y1
e0:O2.eq x2 y2
Compare lt eq (x1, x2) (y1, y2)
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
e:O1.eq x1 y1
l:O2.lt y2 x2
Compare lt eq (x1, x2) (y1, y2)
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
l:O1.lt y1 x1
Compare lt eq (x1, x2) (y1, y2)
 apply EQ; unfold eq; auto.x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
e:O1.eq x1 y1
l:O2.lt y2 x2
Compare lt eq (x1, x2) (y1, y2)
x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
l:O1.lt y1 x1
Compare lt eq (x1, x2) (y1, y2)
 apply GT; unfold lt; auto.x1:O1.t
x2:O2.t
y1:O1.t
y2:O2.t
l:O1.lt y1 x1
Compare lt eq (x1, x2) (y1, y2)
 apply GT; unfold lt; auto.
 Defined.

 Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.forall x y : t, {eq x y} + {~ eq x y}
 Proof.forall x y : t, {eq x y} + {~ eq x y}
 intros; elim (compare x y); intro H; [ right | left | right ]; auto.x, y:t
H:lt x y
~ eq x y
x, y:t
H:lt y x
~ eq x y
 auto using lt_not_eq.x, y:t
H:lt y x
~ eq x y
 assert (~ eq y x); auto using lt_not_eq, eq_sym.
 Defined.

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.forall x y z : positive,
bits_lt x y -> bits_lt y z -> bits_lt x z
  Proof.forall x y z : positive,
bits_lt x y -> bits_lt y z -> bits_lt x z
  induction x.x:positive
IHx:forall y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z
forall y z : positive,
bits_lt x~1 y -> bits_lt y z -> bits_lt x~1 z
x:positive
IHx:forall y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z
forall y z : positive,
bits_lt x~0 y -> bits_lt y z -> bits_lt x~0 z
forall y z : positive,
bits_lt 1 y -> bits_lt y z -> bits_lt 1 z
  induction y; destruct z; simpl; eauto; intuition.x:positive
IHx:forall y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z
forall y z : positive,
bits_lt x~0 y -> bits_lt y z -> bits_lt x~0 z
forall y z : positive,
bits_lt 1 y -> bits_lt y z -> bits_lt 1 z
  induction y; destruct z; simpl; eauto; intuition.forall y z : positive,
bits_lt 1 y -> bits_lt y z -> bits_lt 1 z
  induction y; destruct z; simpl; eauto; intuition.
  Qed.

  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.forall x y z : t, lt x y -> lt y z -> lt x z
  Proof.forall x y z : t, lt x y -> lt y z -> lt x z
  exact bits_lt_trans.
  Qed.

  Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x.forall x : positive, ~ bits_lt x x
  Proof.forall x : positive, ~ bits_lt x x
  induction x; simpl; auto.
  Qed.

  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.forall x y : t, lt x y -> ~ eq x y
  Proof.forall x y : t, lt x y -> ~ eq x y
  intros; intro.x, y:t
H:lt x y
H0:eq x y
False
  rewrite <- H0 in H; clear H0 y.x:t
H:lt x x
False
  unfold lt in H.x:t
H:bits_lt x x
False
  exact (bits_lt_antirefl x H).
  Qed.

  Definition compare : forall x y : t, Compare lt eq x y.forall x y : t, Compare lt eq x y
  Proof.forall x y : t, Compare lt eq x y
  induction x; destruct y.x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
Compare lt eq x~1 y~1
x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
Compare lt eq x~1 y~0
x:positive
IHx:forall y : t, Compare lt eq x y
Compare lt eq x~1 1
x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
Compare lt eq x~0 y~1
x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
Compare lt eq x~0 y~0
x:positive
IHx:forall y : t, Compare lt eq x y
Compare lt eq x~0 1
y:positive
Compare lt eq 1 y~1
y:positive
Compare lt eq 1 y~0
Compare lt eq 1 1
  - (* I I *)x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
Compare lt eq x~1 y~1
    destruct (IHx y) as [l|e|g].x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
l:lt x y
Compare lt eq x~1 y~1
x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
e:eq x y
Compare lt eq x~1 y~1
x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
g:lt y x
Compare lt eq x~1 y~1
    apply LT; auto.x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
e:eq x y
Compare lt eq x~1 y~1
x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
g:lt y x
Compare lt eq x~1 y~1
    apply EQ; rewrite e; red; auto.x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
g:lt y x
Compare lt eq x~1 y~1
    apply GT; auto.
  - (* I O *)x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
Compare lt eq x~1 y~0
    apply GT; simpl; auto.
  - (* I H *)x:positive
IHx:forall y : t, Compare lt eq x y
Compare lt eq x~1 1
    apply GT; simpl; auto.
  - (* O I *)x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
Compare lt eq x~0 y~1
    apply LT; simpl; auto.
  - (* O O *)x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
Compare lt eq x~0 y~0
    destruct (IHx y) as [l|e|g].x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
l:lt x y
Compare lt eq x~0 y~0
x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
e:eq x y
Compare lt eq x~0 y~0
x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
g:lt y x
Compare lt eq x~0 y~0
    apply LT; auto.x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
e:eq x y
Compare lt eq x~0 y~0
x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
g:lt y x
Compare lt eq x~0 y~0
    apply EQ; rewrite e; red; auto.x:positive
IHx:forall y0 : t, Compare lt eq x y0
y:positive
g:lt y x
Compare lt eq x~0 y~0
    apply GT; auto.
  - (* O H *)x:positive
IHx:forall y : t, Compare lt eq x y
Compare lt eq x~0 1
    apply LT; simpl; auto.
  - (* H I *)y:positive
Compare lt eq 1 y~1
    apply LT; simpl; auto.
  - (* H O *)y:positive
Compare lt eq 1 y~0
    apply GT; simpl; auto.
  - (* H H *)Compare lt eq 1 1
    apply EQ; red; auto.
  Qed.

  Lemma eq_dec (x y: positive): {x = y} + {x <> y}.x, y:positive
{x = y} + {x <> y}
  Proof.x, y:positive
{x = y} + {x <> y}
  intros.x, y:positive
{x = y} + {x <> y} case_eq (x ?= y); intros.x, y:positive
H:(x ?= y) = Eq
{x = y} + {x <> y}
x, y:positive
H:(x ?= y) = Lt
{x = y} + {x <> y}
x, y:positive
H:(x ?= y) = Gt
{x = y} + {x <> y}
  -x, y:positive
H:(x ?= y) = Eq
{x = y} + {x <> y} left.x, y:positive
H:(x ?= y) = Eq
x = y now apply Pos.compare_eq.
  -x, y:positive
H:(x ?= y) = Lt
{x = y} + {x <> y} right.x, y:positive
H:(x ?= y) = Lt
x <> y intro.x, y:positive
H:(x ?= y) = Lt
H0:x = y
False subst y.x:positive
H:(x ?= x) = Lt
False now rewrite (Pos.compare_refl x) in *.
  -x, y:positive
H:(x ?= y) = Gt
{x = y} + {x <> y} right.x, y:positive
H:(x ?= y) = Gt
x <> y intro.x, y:positive
H:(x ?= y) = Gt
H0:x = y
False subst y.x:positive
H:(x ?= x) = Gt
False now rewrite (Pos.compare_refl x) in *.
  Qed.

End PositiveOrderedTypeBits.

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.a, b:ascii
nat_of_ascii a = nat_of_ascii b -> a = b
  Proof.a, b:ascii
nat_of_ascii a = nat_of_ascii b -> a = b
    intro H.a, b:ascii
H:nat_of_ascii a = nat_of_ascii b
a = b
    rewrite <- (ascii_nat_embedding a).a, b:ascii
H:nat_of_ascii a = nat_of_ascii b
ascii_of_nat (nat_of_ascii a) = b
    rewrite <- (ascii_nat_embedding b).a, b:ascii
H:nat_of_ascii a = nat_of_ascii b
ascii_of_nat (nat_of_ascii a) =
ascii_of_nat (nat_of_ascii b)
    apply f_equal; auto.
  Qed.

  Lemma lts_tail_unique a s1 s2 : lt (String a s1) (String a s2) ->
    lt s1 s2.a:ascii
s1, s2:string
lt (String a s1) (String a s2) -> lt s1 s2
  Proof.a:ascii
s1, s2:string
lt (String a s1) (String a s2) -> lt s1 s2
    intro H; inversion H; subst; auto.a:ascii
s1, s2:string
H:lt (String a s1) (String a s2)
H1:(nat_of_ascii a < nat_of_ascii a)%nat
lt s1 s2
    remember (nat_of_ascii a) as x.a:ascii
s1, s2:string
H:lt (String a s1) (String a s2)
x:nat
Heqx:x = nat_of_ascii a
H1:(x < x)%nat
lt s1 s2
    apply lt_irrefl in H1; inversion H1.
  Qed.

  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.forall x y z : t, lt x y -> lt y z -> lt x z
  Proof.forall x y z : t, lt x y -> lt y z -> lt x z
    induction x; intros y z H1 H2.y, z:t
H1:lt "" y
H2:lt y z
lt "" z
a:ascii
x:string
IHx:forall y0 z0 : t, lt x y0 -> lt y0 z0 -> lt x z0
y, z:t
H1:lt (String a x) y
H2:lt y z
lt (String a x) z
    -y, z:t
H1:lt "" y
H2:lt y z
lt "" z destruct y as [| b y']; inversion H1.b:ascii
y':string
z:t
H1:lt "" (String b y')
H2:lt (String b y') z
a:ascii
s:string
H:a = b
H3:s = y'
lt "" z
      destruct z as [| c z']; inversion H2; constructor.
    -a:ascii
x:string
IHx:forall y0 z0 : t, lt x y0 -> lt y0 z0 -> lt x z0
y, z:t
H1:lt (String a x) y
H2:lt y z
lt (String a x) z destruct y as [| b y']; inversion H1; subst;
        destruct z as [| c z']; inversion H2; subst.x:string
IHx:forall y z : t, lt x y -> lt y z -> lt x z
y':string
c:ascii
z':string
H2:lt (String c y') (String c z')
H1:lt (String c x) (String c y')
H0:lts x y'
H3:lts y' z'
lt (String c x) (String c z')
x:string
IHx:forall y z : t, lt x y -> lt y z -> lt x z
b:ascii
y':string
c:ascii
z':string
H1:lt (String b x) (String b y')
H2:lt (String b y') (String c z')
H0:lts x y'
H3:(nat_of_ascii b < nat_of_ascii c)%nat
lt (String b x) (String c z')
a:ascii
x:string
IHx:forall y z : t, lt x y -> lt y z -> lt x z
y':string
c:ascii
z':string
H0:(nat_of_ascii a < nat_of_ascii c)%nat
H2:lt (String c y') (String c z')
H1:lt (String a x) (String c y')
H3:lts y' z'
lt (String a x) (String c z')
a:ascii
x:string
IHx:forall y z : t, lt x y -> lt y z -> lt x z
b:ascii
y':string
c:ascii
z':string
H1:lt (String a x) (String b y')
H2:lt (String b y') (String c z')
H0:(nat_of_ascii a < nat_of_ascii b)%nat
H3:(nat_of_ascii b < nat_of_ascii c)%nat
lt (String a x) (String c z')
      +x:string
IHx:forall y z : t, lt x y -> lt y z -> lt x z
y':string
c:ascii
z':string
H2:lt (String c y') (String c z')
H1:lt (String c x) (String c y')
H0:lts x y'
H3:lts y' z'
lt (String c x) (String c z') constructor.x:string
IHx:forall y z : t, lt x y -> lt y z -> lt x z
y':string
c:ascii
z':string
H2:lt (String c y') (String c z')
H1:lt (String c x) (String c y')
H0:lts x y'
H3:lts y' z'
lts x z' eapply IHx; eauto.
      +x:string
IHx:forall y z : t, lt x y -> lt y z -> lt x z
b:ascii
y':string
c:ascii
z':string
H1:lt (String b x) (String b y')
H2:lt (String b y') (String c z')
H0:lts x y'
H3:(nat_of_ascii b < nat_of_ascii c)%nat
lt (String b x) (String c z') constructor; assumption.
      +a:ascii
x:string
IHx:forall y z : t, lt x y -> lt y z -> lt x z
y':string
c:ascii
z':string
H0:(nat_of_ascii a < nat_of_ascii c)%nat
H2:lt (String c y') (String c z')
H1:lt (String a x) (String c y')
H3:lts y' z'
lt (String a x) (String c z') constructor; assumption.
      +a:ascii
x:string
IHx:forall y z : t, lt x y -> lt y z -> lt x z
b:ascii
y':string
c:ascii
z':string
H1:lt (String a x) (String b y')
H2:lt (String b y') (String c z')
H0:(nat_of_ascii a < nat_of_ascii b)%nat
H3:(nat_of_ascii b < nat_of_ascii c)%nat
lt (String a x) (String c z') constructor.a:ascii
x:string
IHx:forall y z : t, lt x y -> lt y z -> lt x z
b:ascii
y':string
c:ascii
z':string
H1:lt (String a x) (String b y')
H2:lt (String b y') (String c z')
H0:(nat_of_ascii a < nat_of_ascii b)%nat
H3:(nat_of_ascii b < nat_of_ascii c)%nat
(nat_of_ascii a < nat_of_ascii c)%nat eapply lt_trans; eassumption.
  Qed.

  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.forall x y : t, lt x y -> ~ eq x y
  Proof.forall x y : t, lt x y -> ~ eq x y
    induction x; intros y LT.y:t
LT:lt "" y
~ eq "" y
a:ascii
x:string
IHx:forall y0 : t, lt x y0 -> ~ eq x y0
y:t
LT:lt (String a x) y
~ eq (String a x) y
    -y:t
LT:lt "" y
~ eq "" y inversion LT.y:t
LT:lt "" y
a:ascii
s:string
H0:String a s = y
~ eq "" (String a s) intro.y:t
LT:lt "" y
a:ascii
s:string
H0:String a s = y
H:eq "" (String a s)
False inversion H.
    -a:ascii
x:string
IHx:forall y0 : t, lt x y0 -> ~ eq x y0
y:t
LT:lt (String a x) y
~ eq (String a x) y inversion LT; subst; intros EQ.a:ascii
x:string
IHx:forall y : t, lt x y -> ~ eq x y
s2:string
LT:lt (String a x) (String a s2)
H2:lts x s2
EQ:eq (String a x) (String a s2)
False
a:ascii
x:string
IHx:forall y : t, lt x y -> ~ eq x y
b:ascii
s2:string
LT:lt (String a x) (String b s2)
H2:(nat_of_ascii a < nat_of_ascii b)%nat
EQ:eq (String a x) (String b s2)
False
      *a:ascii
x:string
IHx:forall y : t, lt x y -> ~ eq x y
s2:string
LT:lt (String a x) (String a s2)
H2:lts x s2
EQ:eq (String a x) (String a s2)
False specialize (IHx s2 H2).a:ascii
x, s2:string
IHx:~ eq x s2
LT:lt (String a x) (String a s2)
H2:lts x s2
EQ:eq (String a x) (String a s2)
False
        inversion EQ; subst; auto.a:ascii
s2:string
EQ:eq (String a s2) (String a s2)
H2:lts s2 s2
LT:lt (String a s2) (String a s2)
IHx:~ eq s2 s2
False
        apply IHx; unfold eq; auto.
      *a:ascii
x:string
IHx:forall y : t, lt x y -> ~ eq x y
b:ascii
s2:string
LT:lt (String a x) (String b s2)
H2:(nat_of_ascii a < nat_of_ascii b)%nat
EQ:eq (String a x) (String b s2)
False inversion EQ; subst; auto.s2:string
b:ascii
EQ:eq (String b s2) (String b s2)
IHx:forall y : t, lt s2 y -> ~ eq s2 y
H2:(nat_of_ascii b < nat_of_ascii b)%nat
LT:lt (String b s2) (String b s2)
False
        apply Nat.lt_irrefl in H2; auto.
  Qed.

  Definition compare x y : Compare lt eq x y.x, y:string
Compare lt eq x y
  Proof.x, y:string
Compare lt eq x y
    generalize dependent y.x:string
forall y : string, Compare lt eq x y
    induction x as [ | a s1]; destruct y as [ | b s2].Compare lt eq ""%string ""%string
b:ascii
s2:string
Compare lt eq ""%string (String b s2)
a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
Compare lt eq (String a s1) ""%string
a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
Compare lt eq (String a s1) (String b s2)
    -Compare lt eq ""%string ""%string apply EQ; constructor.
    -b:ascii
s2:string
Compare lt eq ""%string (String b s2) apply LT; constructor.
    -a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
Compare lt eq (String a s1) ""%string apply GT; constructor.
    -a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
Compare lt eq (String a s1) (String b s2) destruct ((nat_of_ascii a) ?= (nat_of_ascii b))%nat eqn:ltb.a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a ?= nat_of_ascii b)%nat = Eq
Compare lt eq (String a s1) (String b s2)
a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a ?= nat_of_ascii b)%nat = Lt
Compare lt eq (String a s1) (String b s2)
a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a ?= nat_of_ascii b)%nat = Gt
Compare lt eq (String a s1) (String b s2)
      +a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a ?= nat_of_ascii b)%nat = Eq
Compare lt eq (String a s1) (String b s2) assert (a = b).a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a ?= nat_of_ascii b)%nat = Eq
a = b
a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a ?= nat_of_ascii b)%nat = Eq
H:a = b
Compare lt eq (String a s1) (String b s2)
        {a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a ?= nat_of_ascii b)%nat = Eq
a = b
          apply Nat.compare_eq in ltb.a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:nat_of_ascii a = nat_of_ascii b
a = b
          assert (ascii_of_nat (nat_of_ascii a)
                  = ascii_of_nat (nat_of_ascii b)) by auto.a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:nat_of_ascii a = nat_of_ascii b
H:ascii_of_nat (nat_of_ascii a) =
ascii_of_nat (nat_of_ascii b)
a = b
          repeat rewrite ascii_nat_embedding in H.a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:nat_of_ascii a = nat_of_ascii b
H:a = b
a = b
          auto.
        }a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a ?= nat_of_ascii b)%nat = Eq
H:a = b
Compare lt eq (String a s1) (String b s2)
        subst.s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii b ?= nat_of_ascii b)%nat = Eq
Compare lt eq (String b s1) (String b s2)
        destruct (IHs1 s2).s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii b ?= nat_of_ascii b)%nat = Eq
l:lt s1 s2
Compare lt eq (String b s1) (String b s2)
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii b ?= nat_of_ascii b)%nat = Eq
e:eq s1 s2
Compare lt eq (String b s1) (String b s2)
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii b ?= nat_of_ascii b)%nat = Eq
l:lt s2 s1
Compare lt eq (String b s1) (String b s2)
        *s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii b ?= nat_of_ascii b)%nat = Eq
l:lt s1 s2
Compare lt eq (String b s1) (String b s2) apply LT; constructor; auto.
        *s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii b ?= nat_of_ascii b)%nat = Eq
e:eq s1 s2
Compare lt eq (String b s1) (String b s2) apply EQ.s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii b ?= nat_of_ascii b)%nat = Eq
e:eq s1 s2
eq (String b s1) (String b s2) unfold eq in e.s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii b ?= nat_of_ascii b)%nat = Eq
e:s1 = s2
eq (String b s1) (String b s2) subst.s2:string
IHs1:forall y : string, Compare lt eq s2 y
b:ascii
ltb:(nat_of_ascii b ?= nat_of_ascii b)%nat = Eq
eq (String b s2) (String b s2) constructor; auto.
        *s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii b ?= nat_of_ascii b)%nat = Eq
l:lt s2 s1
Compare lt eq (String b s1) (String b s2) apply GT; constructor; auto.
      +a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a ?= nat_of_ascii b)%nat = Lt
Compare lt eq (String a s1) (String b s2) apply nat_compare_lt in ltb.a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a < nat_of_ascii b)%nat
Compare lt eq (String a s1) (String b s2)
        apply LT; constructor; auto.
      +a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a ?= nat_of_ascii b)%nat = Gt
Compare lt eq (String a s1) (String b s2) apply nat_compare_gt in ltb.a:ascii
s1:string
IHs1:forall y : string, Compare lt eq s1 y
b:ascii
s2:string
ltb:(nat_of_ascii a > nat_of_ascii b)%nat
Compare lt eq (String a s1) (String b s2)
        apply GT; constructor; auto.
  Defined.

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