Uniformisation Sorting/Mergesort and Structures/Orders

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

1 files changed, 174 insertions, 1 deletions

diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index c71be0a6e..96daca5cd 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -82,7 +82,6 @@ Module Type DecStrOrder' := DecStrOrder <+ EqLtNotation.
 Module Type OrderedType' := OrderedType <+ EqLtNotation.
 Module Type OrderedTypeFull' := OrderedTypeFull <+ EqLtLeNotation.
 
-
 (** NB: in [OrderedType], an [eq_dec] could be deduced from [compare].
   But adding this redundant field allows to see an [OrderedType] as a
   [DecidableType]. *)
@@ -158,3 +157,177 @@ End OTF_LtIsTotal.
 Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
  := O <+ OTF_LtIsTotal.
 
+
+(** * Versions with boolean comparisons
+
+    This style is used in [Mergesort]
+*)
+
+(** For stating properties like transitivity  of [leb],
+    we coerce [bool] into [Prop].
+    NB: To migrate in Init/Datatype later *)
+Local Coercion is_true b := b = true.  (*: bool >-> Sortclass.*)
+Hint Unfold is_true.
+
+Module Type HasLeBool (Import T:Typ).
+  Parameter Inline leb : t -> t -> bool.
+End HasLeBool.
+
+Module Type HasLtBool (Import T:Typ).
+  Parameter Inline ltb : t -> t -> bool.
+End HasLtBool.
+
+Module Type LeBool := Typ <+ HasLeBool.
+Module Type LtBool := Typ <+ HasLtBool.
+
+Module Type LeBoolNotation (E:LeBool).
+  Infix "<=?" := E.leb (at level 35).
+End LeBoolNotation.
+
+Module Type LtBoolNotation (E:LtBool).
+  Infix "<?" := E.ltb (at level 35).
+End LtBoolNotation.
+
+Module Type LeBool' := LeBool <+ LeBoolNotation.
+Module Type LtBool' := LtBool <+ LtBoolNotation.
+
+Module Type LeBool_Le (T:Typ)(X:HasLeBool T)(Y:HasLe T).
+ Parameter leb_le : forall x y, X.leb x y = true <-> Y.le x y.
+End LeBool_Le.
+
+Module Type LtBool_Lt (T:Typ)(X:HasLtBool T)(Y:HasLt T).
+ Parameter ltb_lt : forall x y, X.ltb x y = true <-> Y.lt x y.
+End LtBool_Lt.
+
+Module Type LeBoolIsTotal (Import X:LeBool').
+ Axiom leb_total : forall x y, (x <=? y) = true \/ (y <=? x) = true.
+End LeBoolIsTotal.
+
+Module Type TotalLeBool := LeBool <+ LeBoolIsTotal.
+Module Type TotalLeBool' := LeBool' <+ LeBoolIsTotal.
+
+Module Type LeBoolIsTransitive (Import X:LeBool').
+ Axiom leb_trans : Transitive X.leb.
+End LeBoolIsTransitive.
+
+Module Type TotalTransitiveLeBool := TotalLeBool <+ LeBoolIsTransitive.
+Module Type TotalTransitiveLeBool' := TotalLeBool' <+ LeBoolIsTransitive.
+
+
+(** * From [OrderedTypeFull] to [TotalTransitiveLeBool] *)
+
+Module OTF_to_TTLB (Import O : OrderedTypeFull') <: TotalTransitiveLeBool.
+
+ Definition leb x y :=
+  match compare x y with Gt => false | _ => true end.
+
+ Lemma leb_le : forall x y, leb x y <-> x <= y.
+ Proof.
+ intros. unfold leb. rewrite le_lteq.
+ destruct (compare_spec x y) as [EQ|LT|GT]; split; auto.
+ discriminate.
+ intros LE. elim (StrictOrder_Irreflexive x).
+ destruct LE as [LT|EQ]. now transitivity y. now rewrite <- EQ in GT.
+ Qed.
+
+ Lemma leb_total : forall x y, leb x y \/ leb y x.
+ Proof.
+ intros. rewrite 2 leb_le. rewrite 2 le_lteq.
+ destruct (compare_spec x y); intuition.
+ Qed.
+
+ Lemma leb_trans : Transitive leb.
+ Proof.
+ intros x y z. rewrite !leb_le, !le_lteq.
+ intros [Hxy|Hxy] [Hyz|Hyz].
+ left; transitivity y; auto.
+ left; rewrite <- Hyz; auto.
+ left; rewrite Hxy; auto.
+ right; transitivity y; auto.
+ Qed.
+
+ Definition t := t.
+
+End OTF_to_TTLB.
+
+
+(** * From [TotalTransitiveLeBool] to [OrderedTypeFull]
+
+    [le] is [leb ... = true].
+    [eq] is [le /\ swap le].
+    [lt] is [le /\ ~swap le].
+*)
+
+Local Open Scope bool_scope.
+
+Module TTLB_to_OTF (Import O : TotalTransitiveLeBool') <: OrderedTypeFull.
+
+ Definition t := t.
+
+ Definition le x y : Prop := x <=? y.
+ Definition eq x y : Prop := le x y /\ le y x.
+ Definition lt x y : Prop := le x y /\ ~le y x.
+
+ Definition compare x y :=
+  if x <=? y then (if y <=? x then Eq else Lt) else Gt.
+
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+ Proof.
+ intros. unfold compare.
+ case_eq (x <=? y).
+ case_eq (y <=? x).
+ constructor. split; auto.
+ constructor. split; congruence.
+ constructor. destruct (leb_total x y); split; congruence.
+ Qed.
+
+ Definition eqb x y := (x <=? y) && (y <=? x).
+
+ Lemma eqb_eq : forall x y, eqb x y <-> eq x y.
+ Proof.
+ intros. unfold eq, eqb, le.
+ case leb; simpl; intuition; discriminate.
+ Qed.
+
+ Include HasEqBool2Dec.
+
+ Instance eq_equiv : Equivalence eq.
+ Proof.
+ split.
+ intros x; unfold eq, le. destruct (leb_total x x); auto.
+ intros x y; unfold eq, le. intuition.
+ intros x y z; unfold eq, le. intuition; apply leb_trans with y; auto.
+ Qed.
+
+ Instance lt_strorder : StrictOrder lt.
+ Proof.
+ split.
+ intros x. unfold lt; red; intuition.
+ intros x y z; unfold lt, le. intuition.
+ apply leb_trans with y; auto.
+ absurd (z <=? y); auto.
+ apply leb_trans with x; auto.
+ Qed.
+
+ Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
+ Proof.
+ apply proper_sym_impl_iff_2; auto with *.
+ intros x x' Hx y y' Hy' H. unfold eq, lt, le in *.
+ intuition.
+ apply leb_trans with x; auto.
+ apply leb_trans with y; auto.
+ absurd (y <=? x); auto.
+ apply leb_trans with x'; auto.
+ apply leb_trans with y'; auto.
+ Qed.
+
+ Definition le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
+ Proof.
+ intros.
+ unfold lt, eq, le.
+ split; [ | intuition ].
+ intros LE.
+ case_eq (y <=? x); [right|left]; intuition; try discriminate.
+ Qed.
+
+End TTLB_to_OTF.