Uniformisation Sorting/Mergesort and Structures/Orders

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

2 files changed, 198 insertions, 33 deletions

diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index 723bb76d31..238013b854 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -13,7 +13,7 @@
 
 (* Initial author: Hugo Herbelin, Oct 2009 *)
 
-Require Import List Setoid Permutation Sorted.
+Require Import List Setoid Permutation Sorted Orders.
 
 (** Notations and conventions *)
 
@@ -22,22 +22,16 @@ Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
 
 Open Scope bool_scope.
 
-Local Coercion eq_true : bool >-> Sortclass.
+Local Coercion is_true : bool >-> Sortclass.
 
-(** A total relation *)
-
-Module Type TotalOrder.
-  Parameter A : Type.
-  Parameter le_bool : A -> A -> bool.
-  Infix "<=?" := le_bool (at level 35).
-  Axiom le_bool_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
-End TotalOrder.
-
-(** The main module defining [mergesort] on a given total order.
-    We require minimal hypotheses
- *)
+(** The main module defining [mergesort] on a given boolean
+    order [<=?]. We require minimal hypotheses : this boolean
+    order should only be total: [forall x y, (x<=?y) \/ (y<=?x)].
+    Transitivity is not mandatory, but without it one can
+    only prove [LocallySorted] and not [StronglySorted].
+*)
 
-Module Sort (Import X:TotalOrder).
+Module Sort (Import X:Orders.TotalLeBool').
 
 Fixpoint merge l1 l2 :=
   let fix merge_aux l2 :=
@@ -116,7 +110,7 @@ Definition sort := iter_merge [].
 
 (** The proof of correctness *)
 
-Local Notation Sorted := (LocallySorted le_bool) (only parsing).
+Local Notation Sorted := (LocallySorted leb) (only parsing).
 
 Fixpoint SortedStack stack :=
   match stack with
@@ -127,7 +121,7 @@ Fixpoint SortedStack stack :=
 
 Local Ltac invert H := inversion H; subst; clear H.
 
-Fixpoint flatten_stack (stack : list (option (list A))) :=
+Fixpoint flatten_stack (stack : list (option (list t))) :=
   match stack with
   | [] => []
   | None :: stack' => flatten_stack stack'
@@ -145,19 +139,18 @@ induction l1; induction l2; intros; simpl; auto.
       clear H0 H3 IHl1; simpl in *.
       destruct (b <=? a0); constructor; auto || rewrite Heq1; constructor.
     assert (a0 <=? a) by
-      (destruct (le_bool_total a0 a) as [H'|H']; trivial || (rewrite Heq1 in H'; inversion H')).
+      (destruct (leb_total a0 a) as [H'|H']; trivial || (rewrite Heq1 in H'; inversion H')).
     invert H0.
       constructor; trivial.
       assert (Sorted (merge (a::l1) (b::l))) by auto using IHl1.
       clear IHl2; simpl in *.
-      destruct (a <=? b) as ()_eqn:Heq2;
-        constructor; auto.
+      destruct (a <=? b); constructor; auto.
 Qed.
 
 Theorem Permuted_merge : forall l1 l2, Permutation (l1++l2) (merge l1 l2).
 Proof.
   induction l1; simpl merge; intro.
-    assert (forall l, (fix merge_aux (l0 : list A) : list A := l0) l = l)
+    assert (forall l, (fix merge_aux (l0 : list t) : list t := l0) l = l)
     as -> by (destruct l; trivial). (* Technical lemma *)
     apply Permutation_refl.
   induction l2.
@@ -241,7 +234,7 @@ Proof.
 intro; apply Sorted_iter_merge. constructor.
 Qed.
 
-Corollary LocallySorted_sort : forall l, Sorted.Sorted le_bool (sort l).
+Corollary LocallySorted_sort : forall l, Sorted.Sorted leb (sort l).
 Proof. intro; eapply Sorted_LocallySorted_iff, Sorted_sort; auto. Qed.
 
 Theorem Permuted_sort : forall l, Permutation l (sort l).
@@ -250,27 +243,26 @@ intro; apply (Permuted_iter_merge l []).
 Qed.
 
 Corollary StronglySorted_sort : forall l,
-  Transitive le_bool -> StronglySorted le_bool (sort l).
+  Transitive leb -> StronglySorted leb (sort l).
 Proof. auto using Sorted_StronglySorted, LocallySorted_sort. Qed.
 
 End Sort.
 
 (** An example *)
 
-Module NatOrder.
-  Definition A := nat.
-  Fixpoint le_bool x y :=
+Module NatOrder <: TotalLeBool.
+  Definition t := nat.
+  Fixpoint leb x y :=
     match x, y with
     | 0, _ => true
-    | S x', 0 => false
-    | S x', S y' => le_bool x' y'
+    | _, 0 => false
+    | S x', S y' => leb x' y'
     end.
-  Infix "<=?" := le_bool (at level 35).
-  Theorem le_bool_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
+  Infix "<=?" := leb (at level 35).
+  Theorem leb_total : forall a1 a2, a1 <=? a2 \/ a2 <=? a1.
   Proof.
-    induction a1; destruct a2; simpl; auto using is_eq_true.
+    induction a1; destruct a2; simpl; auto.
   Qed.
-
 End NatOrder.
 
 Module Import NatSort := Sort NatOrder.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index c71be0a6ee..96daca5cd3 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.