From 86465afdd668759afc3d57d9feebe26d07dd6a4b Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 16 Feb 2010 10:49:40 +0000 Subject: Uniformisation Sorting/Mergesort and Structures/Orders git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12772 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Structures/Orders.v | 175 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 174 insertions(+), 1 deletion(-) (limited to 'theories/Structures') 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 " 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. -- cgit v1.2.3