(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(* Ordered types *)

Inductive Compare [X:Set; lt,eq:X->X->Prop; x,y:X] : Set :=
  | Lt : (lt x y) -> (Compare lt eq x y)
  | Eq : (eq x y) -> (Compare lt eq x y)
  | Gt : (lt y x) -> (Compare lt eq x y).

Module Type OrderedType.

  Parameter t : Set.

  Parameter eq : t -> t -> Prop.
  Parameter lt : t -> t -> Prop.

  Axiom eq_refl : (x:t) (eq x x).
  Axiom eq_sym : (x,y:t) (eq x y) -> (eq y x).
  Axiom eq_trans : (x,y,z:t) (eq x y) -> (eq y z) -> (eq x z).
 
  Axiom lt_trans : (x,y,z:t) (lt x y) -> (lt y z) -> (lt x z).
  Axiom lt_not_eq : (x,y:t) (lt x y) -> ~(eq x y).

  Parameter compare : (x,y:t)(Compare lt eq x y).

  Hints Immediate eq_sym.
  Hints Resolve eq_refl eq_trans lt_not_eq lt_trans.

End OrderedType.