DecidableType2+OrderedType2 : notations in specific Module Type, slicing of OrderedType2

 OrderedType2 is reorganized in atomic module type following the same approach used
 for DecidableType2.

 We use the following convention: module type Foo' is exactly module type Foo,
 except that some notations may have been added. In functor arg, we can use
 Foo or Foo' depending on whether we want nice notation or not. Note that any
 implementation of Foo is accepted as implementation of Foo' :-). For the moment,
 these notations are not placed in specific scopes, I think it isn't useful, but
 I may be wrong, we'll see later when using them.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12635 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 171 insertions, 83 deletions

diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 585b98136..2679d25b0 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -13,33 +13,47 @@ Require Export RelationClasses.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** * Types with Equality, and nothing more (for subtyping purpose) *)
+(** * Structure with just a base type [t] *)
 
-Module Type BareEquality.
+Module Type Typ.
   Parameter Inline t : Type.
+End Typ.
+
+(** * Structure with an equality relation [eq] *)
+
+Module Type HasEq (Import T:Typ).
   Parameter Inline eq : t -> t -> Prop.
-End BareEquality.
+End HasEq.
+
+Module Type Eq := Typ <+ HasEq.
 
-(** * Specification of the equality by the Type Classe [Equivalence] *)
+Module Type EqNotation (Import E:Eq).
+  Infix "==" := eq (at level 70, no associativity).
+  Notation "x ~= y" := (~eq x y) (at level 70, no associativity).
+End EqNotation.
 
-Module Type IsEq (Import E:BareEquality).
+Module Type Eq' := Eq <+ EqNotation.
+
+(** * Specification of the equality via the [Equivalence] type class *)
+
+Module Type IsEq (Import E:Eq).
   Declare Instance eq_equiv : Equivalence eq.
 End IsEq.
 
 (** * Earlier specification of equality by three separate lemmas. *)
 
-Module Type IsEqOrig (Import E:BareEquality).
-  Axiom eq_refl : forall x : t, eq x x.
-  Axiom eq_sym : forall x y : t, eq x y -> eq y x.
-  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+Module Type IsEqOrig (Import E:Eq').
+  Axiom eq_refl : forall x : t, x==x.
+  Axiom eq_sym : forall x y : t, x==y -> y==x.
+  Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z.
   Hint Immediate eq_sym.
   Hint Resolve eq_refl eq_trans.
 End IsEqOrig.
 
 (** * Types with decidable equality *)
 
-Module Type HasEqDec (Import E:BareEquality).
-  Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
+Module Type HasEqDec (Import E:Eq').
+  Parameter eq_dec : forall x y : t, { x==y } + { ~ x==y }.
 End HasEqDec.
 
 (** * Boolean Equality *)
@@ -47,50 +61,61 @@ End HasEqDec.
 (** Having [eq_dec] is the same as having a boolean equality plus
     a correctness proof. *)
 
-Module Type HasEqBool (Import E:BareEquality).
+Module Type HasEqBool (Import E:Eq').
   Parameter Inline eqb : t -> t -> bool.
-  Parameter eqb_eq : forall x y, eqb x y = true <-> eq x y.
+  Parameter eqb_eq : forall x y, eqb x y = true <-> x==y.
 End HasEqBool.
 
 (** From these basic blocks, we can build many combinations
     of static standalone module types. *)
 
-Module Type EqualityType := BareEquality <+ IsEq.
+Module Type EqualityType := Eq <+ IsEq.
 
-Module Type EqualityTypeOrig := BareEquality <+ IsEqOrig.
+Module Type EqualityTypeOrig := Eq <+ IsEqOrig.
 
 Module Type EqualityTypeBoth <: EqualityType <: EqualityTypeOrig
- := BareEquality <+ IsEq <+ IsEqOrig.
+ := Eq <+ IsEq <+ IsEqOrig.
 
 Module Type DecidableType <: EqualityType
- := BareEquality <+ IsEq <+ HasEqDec.
+ := Eq <+ IsEq <+ HasEqDec.
 
 Module Type DecidableTypeOrig <: EqualityTypeOrig
- := BareEquality <+ IsEqOrig <+ HasEqDec.
+ := Eq <+ IsEqOrig <+ HasEqDec.
 
 Module Type DecidableTypeBoth <: DecidableType <: DecidableTypeOrig
  := EqualityTypeBoth <+ HasEqDec.
 
 Module Type BooleanEqualityType <: EqualityType
- := BareEquality <+ IsEq <+ HasEqBool.
+ := Eq <+ IsEq <+ HasEqBool.
 
 Module Type BooleanDecidableType <: DecidableType <: BooleanEqualityType
- := BareEquality <+ IsEq <+ HasEqDec <+ HasEqBool.
+ := Eq <+ IsEq <+ HasEqDec <+ HasEqBool.
 
 Module Type DecidableTypeFull <: DecidableTypeBoth <: BooleanDecidableType
- := BareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
+ := Eq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
+
+(** Same, with notation for [eq] *)
 
+Module Type EqualityType' := EqualityType <+ EqNotation.
+Module Type EqualityTypeOrig' := EqualityTypeOrig <+ EqNotation.
+Module Type EqualityTypeBoth' := EqualityTypeBoth <+ EqNotation.
+Module Type DecidableType' := DecidableType <+ EqNotation.
+Module Type DecidableTypeOrig' := DecidableTypeOrig <+ EqNotation.
+Module Type DecidableTypeBoth' := DecidableTypeBoth <+ EqNotation.
+Module Type BooleanEqualityType' := BooleanEqualityType <+ EqNotation.
+Module Type BooleanDecidableType' := BooleanDecidableType <+ EqNotation.
+Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
 
 (** * Compatibility wrapper from/to the old version of
       [EqualityType] and [DecidableType] *)
 
-Module BackportEq (E:BareEquality)(F:IsEq E) <: IsEqOrig E.
+Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
  Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
  Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
  Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
 End BackportEq.
 
-Module UpdateEq (E:BareEquality)(F:IsEqOrig E) <: IsEq E.
+Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.
  Instance eq_equiv : Equivalence E.eq.
  Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed.
 End UpdateEq.
@@ -110,7 +135,7 @@ Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth
 
 (** * Having [eq_dec] is equivalent to having [eqb] and its spec. *)
 
-Module HasEqDec2Bool (E:BareEquality)(F:HasEqDec E) <: HasEqBool E.
+Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E.
  Definition eqb x y := if F.eq_dec x y then true else false.
  Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y.
  Proof.
@@ -120,7 +145,7 @@ Module HasEqDec2Bool (E:BareEquality)(F:HasEqDec E) <: HasEqBool E.
  Qed.
 End HasEqDec2Bool.
 
-Module HasEqBool2Dec (E:BareEquality)(F:HasEqBool E) <: HasEqDec E.
+Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E.
  Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}.
  Proof.
   intros x y. assert (H:=F.eqb_eq x y).
@@ -143,45 +168,45 @@ Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
    A particular case of [DecidableType] where the equality is
    the usual one of Coq. *)
 
-Module Type UsualBareEquality <: BareEquality.
+Module Type UsualEq <: Eq.
  Parameter Inline t : Type.
  Definition eq := @eq t.
-End UsualBareEquality.
+End UsualEq.
 
-Module UsualIsEq (E:UsualBareEquality) <: IsEq E.
+Module UsualIsEq (E:UsualEq) <: IsEq E.
  Program Instance eq_equiv : Equivalence E.eq.
 End UsualIsEq.
 
-Module UsualIsEqOrig (E:UsualBareEquality) <: IsEqOrig E.
+Module UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.
  Definition eq_refl := @eq_refl E.t.
  Definition eq_sym := @eq_sym E.t.
  Definition eq_trans := @eq_trans E.t.
 End UsualIsEqOrig.
 
 Module Type UsualEqualityType <: EqualityType
- := UsualBareEquality <+ IsEq.
+ := UsualEq <+ IsEq.
 
 Module Type UsualDecidableType <: DecidableType
- := UsualBareEquality <+ IsEq <+ HasEqDec.
+ := UsualEq <+ IsEq <+ HasEqDec.
 
 Module Type UsualDecidableTypeBoth <: DecidableTypeBoth
- := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec.
+ := UsualEq <+ IsEq <+ IsEqOrig <+ HasEqDec.
 
-Module Type UsualBoolEq := UsualBareEquality <+ HasEqBool.
+Module Type UsualBoolEq := UsualEq <+ HasEqBool.
 
 Module Type UsualDecidableTypeFull <: DecidableTypeFull
- := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
+ := UsualEq <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool.
 
 
 (** Some shortcuts for easily building a [UsualDecidableType] *)
 
 Module Type MiniDecidableType.
  Parameter t : Type.
- Parameter eq_dec : forall x y : t, {eq x y}+{~eq x y}.
+ Parameter eq_dec : forall x y : t, {x=y}+{~x=y}.
 End MiniDecidableType.
 
 Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth.
- Definition eq := @eq M.t.
+ Definition eq := @Logic.eq M.t.
  Include M <+ UsualIsEq <+ UsualIsEqOrig.
 End Make_UDT.
 
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index be7ec153b..5b669db4e 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -14,82 +14,145 @@ Unset Strict Implicit.
 
 (** * Ordered types *)
 
-Module Type MiniOrderedType.
-  Include Type EqualityType.
+(** First, signatures with only the order relations *)
 
+Module Type HasLt (Import T:Typ).
   Parameter Inline lt : t -> t -> Prop.
+End HasLt.
+
+Module Type HasLe (Import T:Typ).
+  Parameter Inline le : t -> t -> Prop.
+End HasLe.
+
+Module Type EqLt := Typ <+ HasEq <+ HasLt.
+Module Type EqLe := Typ <+ HasEq <+ HasLe.
+Module Type EqLtLe := Typ <+ HasEq <+ HasLt <+ HasLe.
+
+(** Versions with nice notations *)
+
+Module Type LtNotation (E:EqLt).
+  Infix "<" := E.lt.
+  Notation "x < y < z" := (x<y /\ y<z).
+End LtNotation.
+
+Module Type LeNotation (E:EqLe).
+  Infix "<=" := E.le.
+  Notation "x <= y <= z" := (x<=y /\ y<=z).
+End LeNotation.
+
+Module Type LtLeNotation (E:EqLtLe).
+  Include Type LtNotation E <+ LeNotation E.
+  Notation "x <= y < z" := (x<=y /\ y<z).
+  Notation "x < y <= z" := (x<y /\ y<=z).
+End LtLeNotation.
+
+Module Type EqLtNotation (E:EqLt) := EqNotation E <+ LtNotation E.
+Module Type EqLeNotation (E:EqLe) := EqNotation E <+ LeNotation E.
+Module Type EqLtLeNotation (E:EqLtLe) := EqNotation E <+ LtLeNotation E.
+
+Module Type EqLt' := EqLt <+ EqLtNotation.
+Module Type EqLe' := EqLe <+ EqLeNotation.
+Module Type EqLtLe' := EqLtLe <+ EqLtLeNotation.
+
+(** Versions with logical specifications *)
+
+Module Type IsStrOrder (Import E:EqLt).
   Declare Instance lt_strorder : StrictOrder lt.
   Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
+End IsStrOrder.
 
+Module Type LeIsLtEq (Import E:EqLtLe').
+  Axiom le_lteq : forall x y, x<=y <-> x<y \/ x==y.
+End LeIsLtEq.
+
+Module Type HasCompare (Import E:EqLt).
   Parameter Inline compare : t -> t -> comparison.
   Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+End HasCompare.
 
-End MiniOrderedType.
-
+Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
+Module Type DecStrOrder := StrOrder <+ HasCompare.
+Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec.
+Module Type OrderedTypeFull := OrderedType <+ HasLe <+ LeIsLtEq.
 
-Module Type OrderedType.
-  Include Type MiniOrderedType.
+Module Type StrOrder' := StrOrder <+ EqLtNotation.
+Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation.
+Module Type OrderedType' := OrderedType <+ EqLtNotation.
+Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation.
 
-  (** A [eq_dec] can be deduced from [compare] below. But adding this
-     redundant field allows to see an OrderedType as a DecidableType. *)
-  Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }.
 
-End OrderedType.
+(** NB: in [OrderedType], an [eq_dec] could be deduced from [compare].
+  But adding this redundant field allows to see an [OrderedType] as a
+  [DecidableType]. *)
 
+(** * Versions with [eq] being the usual Leibniz equality of Coq *)
 
-Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType.
-  Include O.
+Module Type UsualStrOrder := UsualEqualityType <+ HasLt <+ IsStrOrder.
+Module Type UsualDecStrOrder := UsualStrOrder <+ HasCompare.
+Module Type UsualOrderedType <: UsualDecidableType <: OrderedType
+ := UsualDecStrOrder <+ HasEqDec.
+Module Type UsualOrderedTypeFull := UsualOrderedType <+ HasLe <+ LeIsLtEq.
 
-  Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
-  Proof.
-   intros.
-   assert (H:=compare_spec x y); destruct (compare x y).
-   left; inversion_clear H; auto.
-   right; inversion_clear H. intro H'. rewrite H' in *.
-      apply (StrictOrder_Irreflexive y); auto.
-   right; inversion_clear H. intro H'. rewrite H' in *.
-      apply (StrictOrder_Irreflexive y); auto.
-  Defined.
+(** NB: in [UsualOrderedType], the field [lt_compat] is
+    useless since [eq] is [Leibniz], but it should be
+    there for subtyping. *)
 
-End MOT_to_OT.
+Module Type UsualStrOrder' := UsualStrOrder <+ LtNotation.
+Module Type UsualDecStrOrder' := UsualDecStrOrder <+ LtNotation.
+Module Type UsualOrderedType' := UsualOrderedType <+ LtNotation.
+Module Type UsualOrderedTypeFull' := UsualOrderedTypeFull <+ LtLeNotation.
 
+(** * Purely logical versions *)
 
-(** * UsualOrderedType
+Module Type LtIsTotal (Import E:EqLt').
+  Axiom lt_total : forall x y, x<y \/ x==y \/ y<x.
+End LtIsTotal.
 
-    A particular case of [OrderedType] where the equality is
-    the usual one of Coq. *)
+Module Type TotalOrder := StrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.
+Module Type UsualTotalOrder <: TotalOrder
+ := UsualStrOrder <+ HasLe <+ LeIsLtEq <+ LtIsTotal.
 
-Module Type UsualOrderedType.
- Include Type UsualDecidableType.
+Module Type TotalOrder' := TotalOrder <+ EqLtLeNotation.
+Module Type UsualTotalOrder' := UsualTotalOrder <+ LtLeNotation.
 
- Parameter Inline lt : t -> t -> Prop.
- Declare Instance lt_strorder : StrictOrder lt.
- (* The following is useless since eq is Leibniz, but should be there
-    for subtyping... *)
- Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
+(** * Conversions *)
 
- Parameter Inline compare : t -> t -> comparison.
- Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+(** From [compare] to [eqb], and then [eq_dec] *)
 
-End UsualOrderedType.
+Module Compare2EqBool (Import O:DecStrOrder') <: HasEqBool O.
 
-(** a [UsualOrderedType] is in particular an [OrderedType]. *)
+ Definition eqb x y :=
+   match compare x y with Eq => true | _ => false end.
 
-Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U.
+ Lemma eqb_eq : forall x y, eqb x y = true <-> x==y.
+ Proof.
+ unfold eqb. intros x y.
+ destruct (compare_spec x y) as [H|H|H]; split; auto; try discriminate.
+ intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
+ intros EQ; rewrite EQ in H; elim (StrictOrder_Irreflexive _ H).
+ Qed.
 
+End Compare2EqBool.
 
-(** * OrderedType with also a [<=] predicate *)
+Module DSO_to_OT (O:DecStrOrder) <: OrderedType :=
+  O <+ Compare2EqBool <+ HasEqBool2Dec.
 
-Module Type OrderedTypeFull.
- Include Type OrderedType.
- Parameter Inline le : t -> t -> Prop.
- Axiom le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
-End OrderedTypeFull.
+(** From [OrderedType] To [OrderedTypeFull] (adding [<=]) *)
 
-Module OT_to_Full (O:OrderedType) <: OrderedTypeFull.
+Module OT_to_Full (O:OrderedType') <: OrderedTypeFull.
  Include O.
- Definition le x y := lt x y \/ eq x y.
- Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
+ Definition le x y := x<y \/ x==y.
+ Lemma le_lteq : forall x y, le x y <-> x<y \/ x==y.
  Proof. unfold le; split; auto. Qed.
 End OT_to_Full.
 
+(** From computational to logical versions *)
+
+Module OTF_LtIsTotal (Import O:OrderedTypeFull') <: LtIsTotal O.
+ Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
+ Proof. intros; destruct (compare_spec x y); auto. Qed.
+End OTF_LtIsTotal.
+
+Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
+ := O <+ OTF_LtIsTotal.
+