diff options
Diffstat (limited to 'theories/MSets/MSetInterface.v')
| -rw-r--r-- | theories/MSets/MSetInterface.v | 219 |
1 files changed, 214 insertions, 5 deletions
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 194cb904..f2b908af 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite set library *) (** Set interfaces, inspired by the one of Ocaml. When compared with @@ -439,7 +437,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E. Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}. Definition t := t_. - Implicit Arguments Mkt [ [is_ok] ]. + Arguments Mkt this {is_ok}. Hint Resolve is_ok : typeclass_instances. Definition In (x : elt)(s : t) := M.In x s.(this). @@ -653,7 +651,218 @@ Module Raw2Sets (O:OrderedType)(M:RawSets O) <: Sets with Module E := O. End Raw2Sets. -(** We provide an ordering for sets-as-sorted-lists *) +(** It is in fact possible to provide an ordering on sets with + very little information on them (more or less only the [In] + predicate). This generic build of ordering is in fact not + used for the moment, we rather use a simplier version + dedicated to sets-as-sorted-lists, see [MakeListOrdering]. +*) + +Module Type IN (O:OrderedType). + Parameter Inline t : Type. + Parameter Inline In : O.t -> t -> Prop. + Declare Instance In_compat : Proper (O.eq==>eq==>iff) In. + Definition Equal s s' := forall x, In x s <-> In x s'. + Definition Empty s := forall x, ~In x s. +End IN. + +Module MakeSetOrdering (O:OrderedType)(Import M:IN O). + Module Import MO := OrderedTypeFacts O. + + Definition eq : t -> t -> Prop := Equal. + + Instance eq_equiv : Equivalence eq. + Proof. firstorder. Qed. + + Instance : Proper (O.eq==>eq==>iff) In. + Proof. + intros x x' Ex s s' Es. rewrite Ex. apply Es. + Qed. + + Definition Below x s := forall y, In y s -> O.lt y x. + Definition Above x s := forall y, In y s -> O.lt x y. + + Definition EquivBefore x s s' := + forall y, O.lt y x -> (In y s <-> In y s'). + + Definition EmptyBetween x y s := + forall z, In z s -> O.lt z y -> O.lt z x. + + Definition lt s s' := exists x, EquivBefore x s s' /\ + ((In x s' /\ Below x s) \/ + (In x s /\ exists y, In y s' /\ O.lt x y /\ EmptyBetween x y s')). + + Instance : Proper (O.eq==>eq==>eq==>iff) EquivBefore. + Proof. + unfold EquivBefore. intros x x' E s1 s1' E1 s2 s2' E2. + setoid_rewrite E; setoid_rewrite E1; setoid_rewrite E2; intuition. + Qed. + + Instance : Proper (O.eq==>eq==>iff) Below. + Proof. + unfold Below. intros x x' Ex s s' Es. + setoid_rewrite Ex; setoid_rewrite Es; intuition. + Qed. + + Instance : Proper (O.eq==>eq==>iff) Above. + Proof. + unfold Above. intros x x' Ex s s' Es. + setoid_rewrite Ex; setoid_rewrite Es; intuition. + Qed. + + Instance : Proper (O.eq==>O.eq==>eq==>iff) EmptyBetween. + Proof. + unfold EmptyBetween. intros x x' Ex y y' Ey s s' Es. + setoid_rewrite Ex; setoid_rewrite Ey; setoid_rewrite Es; intuition. + Qed. + + Instance lt_compat : Proper (eq==>eq==>iff) lt. + Proof. + unfold lt. intros s1 s1' E1 s2 s2' E2. + setoid_rewrite E1; setoid_rewrite E2; intuition. + Qed. + + Instance lt_strorder : StrictOrder lt. + Proof. + split. + (* irreflexive *) + intros s (x & _ & [(IN,Em)|(IN & y & IN' & LT & Be)]). + specialize (Em x IN); order. + specialize (Be x IN LT); order. + (* transitive *) + intros s1 s2 s3 (x & EQ & [(IN,Pre)|(IN,Lex)]) + (x' & EQ' & [(IN',Pre')|(IN',Lex')]). + (* 1) Pre / Pre --> Pre *) + assert (O.lt x x') by (specialize (Pre' x IN); auto). + exists x; split. + intros y Hy; rewrite <- (EQ' y); auto; order. + left; split; auto. + rewrite <- (EQ' x); auto. + (* 2) Pre / Lex *) + elim_compare x x'. + (* 2a) x=x' --> Pre *) + destruct Lex' as (y & INy & LT & Be). + exists y; split. + intros z Hz. split; intros INz. + specialize (Pre z INz). rewrite <- (EQ' z), <- (EQ z); auto; order. + specialize (Be z INz Hz). rewrite (EQ z), (EQ' z); auto; order. + left; split; auto. + intros z Hz. transitivity x; auto; order. + (* 2b) x<x' --> Pre *) + exists x; split. + intros z Hz. rewrite <- (EQ' z) by order; auto. + left; split; auto. + rewrite <- (EQ' x); auto. + (* 2c) x>x' --> Lex *) + exists x'; split. + intros z Hz. rewrite (EQ z) by order; auto. + right; split; auto. + rewrite (EQ x'); auto. + (* 3) Lex / Pre --> Lex *) + destruct Lex as (y & INy & LT & Be). + specialize (Pre' y INy). + exists x; split. + intros z Hz. rewrite <- (EQ' z) by order; auto. + right; split; auto. + exists y; repeat split; auto. + rewrite <- (EQ' y); auto. + intros z Hz LTz; apply Be; auto. rewrite (EQ' z); auto; order. + (* 4) Lex / Lex *) + elim_compare x x'. + (* 4a) x=x' --> impossible *) + destruct Lex as (y & INy & LT & Be). + setoid_replace x with x' in LT; auto. + specialize (Be x' IN' LT); order. + (* 4b) x<x' --> Lex *) + exists x; split. + intros z Hz. rewrite <- (EQ' z) by order; auto. + right; split; auto. + destruct Lex as (y & INy & LT & Be). + elim_compare y x'. + (* 4ba *) + destruct Lex' as (y' & Iny' & LT' & Be'). + exists y'; repeat split; auto. order. + intros z Hz LTz. specialize (Be' z Hz LTz). + rewrite <- (EQ' z) in Hz by order. + apply Be; auto. order. + (* 4bb *) + exists y; repeat split; auto. + rewrite <- (EQ' y); auto. + intros z Hz LTz. apply Be; auto. rewrite (EQ' z); auto; order. + (* 4bc*) + assert (O.lt x' x) by auto. order. + (* 4c) x>x' --> Lex *) + exists x'; split. + intros z Hz. rewrite (EQ z) by order; auto. + right; split; auto. + rewrite (EQ x'); auto. + Qed. + + Lemma lt_empty_r : forall s s', Empty s' -> ~ lt s s'. + Proof. + intros s s' Hs' (x & _ & [(IN,_)|(_ & y & IN & _)]). + elim (Hs' x IN). + elim (Hs' y IN). + Qed. + + Definition Add x s s' := forall y, In y s' <-> O.eq x y \/ In y s. + + Lemma lt_empty_l : forall x s1 s2 s2', + Empty s1 -> Above x s2 -> Add x s2 s2' -> lt s1 s2'. + Proof. + intros x s1 s2 s2' Em Ab Ad. + exists x; split. + intros y Hy; split; intros IN. + elim (Em y IN). + rewrite (Ad y) in IN; destruct IN as [EQ|IN]. order. + specialize (Ab y IN). order. + left; split. + rewrite (Ad x). now left. + intros y Hy. elim (Em y Hy). + Qed. + + Lemma lt_add_lt : forall x1 x2 s1 s1' s2 s2', + Above x1 s1 -> Above x2 s2 -> Add x1 s1 s1' -> Add x2 s2 s2' -> + O.lt x1 x2 -> lt s1' s2'. + Proof. + intros x1 x2 s1 s1' s2 s2' Ab1 Ab2 Ad1 Ad2 LT. + exists x1; split; [ | right; split]; auto. + intros y Hy. rewrite (Ad1 y), (Ad2 y). + split; intros [U|U]; try order. + specialize (Ab1 y U). order. + specialize (Ab2 y U). order. + rewrite (Ad1 x1); auto with *. + exists x2; repeat split; auto. + rewrite (Ad2 x2); now left. + intros y. rewrite (Ad2 y). intros [U|U]. order. + specialize (Ab2 y U). order. + Qed. + + Lemma lt_add_eq : forall x1 x2 s1 s1' s2 s2', + Above x1 s1 -> Above x2 s2 -> Add x1 s1 s1' -> Add x2 s2 s2' -> + O.eq x1 x2 -> lt s1 s2 -> lt s1' s2'. + Proof. + intros x1 x2 s1 s1' s2 s2' Ab1 Ab2 Ad1 Ad2 Hx (x & EQ & Disj). + assert (O.lt x1 x). + destruct Disj as [(IN,_)|(IN,_)]; auto. rewrite Hx; auto. + exists x; split. + intros z Hz. rewrite (Ad1 z), (Ad2 z). + split; intros [U|U]; try (left; order); right. + rewrite <- (EQ z); auto. + rewrite (EQ z); auto. + destruct Disj as [(IN,Em)|(IN & y & INy & LTy & Be)]. + left; split; auto. + rewrite (Ad2 x); auto. + intros z. rewrite (Ad1 z); intros [U|U]; try specialize (Ab1 z U); auto; order. + right; split; auto. + rewrite (Ad1 x); auto. + exists y; repeat split; auto. + rewrite (Ad2 y); auto. + intros z. rewrite (Ad2 z). intros [U|U]; try specialize (Ab2 z U); auto; order. + Qed. + +End MakeSetOrdering. + Module MakeListOrdering (O:OrderedType). Module MO:=OrderedTypeFacts O. @@ -663,7 +872,7 @@ Module MakeListOrdering (O:OrderedType). Definition eq s s' := forall x, In x s <-> In x s'. - Instance eq_equiv : Equivalence eq. + Instance eq_equiv : Equivalence eq := _. Inductive lt_list : t -> t -> Prop := | lt_nil : forall x s, lt_list nil (x :: s) |