Library Coq.MSets.MSetList


Finite sets library

This file proposes an implementation of the non-dependent interface MSetInterface.S using strictly ordered list.

Require Export MSetInterface OrdersFacts OrdersLists.
Set Implicit Arguments.

Functions over lists

First, we provide sets as lists which are not necessarily sorted. The specs are proved under the additional condition of being sorted. And the functions returning sets are proved to preserve this invariant.

Module Ops (X:OrderedType) <: WOps X.

  Definition elt := X.t.
  Definition t := list elt.

  Definition empty : t := nil.

  Definition is_empty (l : t) := if l then true else false.

The set operations.


  Fixpoint mem x s :=
    match s with
    | nil => false
    | y :: l =>
        match X.compare x y with
        | Lt => false
        | Eq => true
        | Gt => mem x l
        end
    end.

  Fixpoint add x s :=
    match s with
    | nil => x :: nil
    | y :: l =>
        match X.compare x y with
        | Lt => x :: s
        | Eq => s
        | Gt => y :: add x l
        end
    end.

  Definition singleton (x : elt) := x :: nil.

  Fixpoint remove x s : t :=
    match s with
    | nil => nil
    | y :: l =>
        match X.compare x y with
        | Lt => s
        | Eq => l
        | Gt => y :: remove x l
        end
    end.

  Fixpoint union (s : t) : t -> t :=
    match s with
    | nil => fun s' => s'
    | x :: l =>
        (fix union_aux (s' : t) : t :=
           match s' with
           | nil => s
           | x' :: l' =>
               match X.compare x x' with
               | Lt => x :: union l s'
               | Eq => x :: union l l'
               | Gt => x' :: union_aux l'
               end
           end)
    end.

  Fixpoint inter (s : t) : t -> t :=
    match s with
    | nil => fun _ => nil
    | x :: l =>
        (fix inter_aux (s' : t) : t :=
           match s' with
           | nil => nil
           | x' :: l' =>
               match X.compare x x' with
               | Lt => inter l s'
               | Eq => x :: inter l l'
               | Gt => inter_aux l'
               end
           end)
    end.

  Fixpoint diff (s : t) : t -> t :=
    match s with
    | nil => fun _ => nil
    | x :: l =>
        (fix diff_aux (s' : t) : t :=
           match s' with
           | nil => s
           | x' :: l' =>
               match X.compare x x' with
               | Lt => x :: diff l s'
               | Eq => diff l l'
               | Gt => diff_aux l'
               end
           end)
    end.

  Fixpoint equal (s : t) : t -> bool :=
    fun s' : t =>
    match s, s' with
    | nil, nil => true
    | x :: l, x' :: l' =>
        match X.compare x x' with
        | Eq => equal l l'
        | _ => false
        end
    | _, _ => false
    end.

  Fixpoint subset s s' :=
    match s, s' with
    | nil, _ => true
    | x :: l, x' :: l' =>
        match X.compare x x' with
        | Lt => false
        | Eq => subset l l'
        | Gt => subset s l'
        end
    | _, _ => false
    end.

  Definition fold (B : Type) (f : elt -> B -> B) (s : t) (i : B) : B :=
    fold_left (flip f) s i.

  Fixpoint filter (f : elt -> bool) (s : t) : t :=
    match s with
    | nil => nil
    | x :: l => if f x then x :: filter f l else filter f l
    end.

  Fixpoint for_all (f : elt -> bool) (s : t) : bool :=
    match s with
    | nil => true
    | x :: l => if f x then for_all f l else false
    end.

  Fixpoint exists_ (f : elt -> bool) (s : t) : bool :=
    match s with
    | nil => false
    | x :: l => if f x then true else exists_ f l
    end.

  Fixpoint partition (f : elt -> bool) (s : t) : t * t :=
    match s with
    | nil => (nil, nil)
    | x :: l =>
        let (s1, s2) := partition f l in
        if f x then (x :: s1, s2) else (s1, x :: s2)
    end.

  Definition cardinal (s : t) : nat := length s.

  Definition elements (x : t) : list elt := x.

  Definition min_elt (s : t) : option elt :=
    match s with
    | nil => None
    | x :: _ => Some x
    end.

  Fixpoint max_elt (s : t) : option elt :=
    match s with
    | nil => None
    | x :: nil => Some x
    | _ :: l => max_elt l
    end.

  Definition choose := min_elt.

  Fixpoint compare s s' :=
   match s, s' with
    | nil, nil => Eq
    | nil, _ => Lt
    | _, nil => Gt
    | x::s, x'::s' =>
      match X.compare x x' with
       | Eq => compare s s'
       | Lt => Lt
       | Gt => Gt
      end
   end.

End Ops.

Module MakeRaw (X: OrderedType) <: RawSets X.
  Module Import MX := OrderedTypeFacts X.
  Module Import ML := OrderedTypeLists X.

  Include Ops X.

Proofs of set operation specifications.


  Section ForNotations.

  Definition inf x l :=
   match l with
   | nil => true
   | y::_ => match X.compare x y with Lt => true | _ => false end
   end.

  Fixpoint isok l :=
   match l with
   | nil => true
   | x::l => inf x l && isok l
   end.

  Notation Sort l := (isok l = true).
  Notation Inf := (lelistA X.lt).
  Notation In := (InA X.eq).

  Hint Extern 20 => solve [order] : core.

  Definition IsOk s := Sort s.

  Class Ok (s:t) : Prop := ok : Sort s.

  Hint Resolve ok : core.
  Hint Unfold Ok : core.

  Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.

  Lemma inf_iff : forall x l, Inf x l <-> inf x l = true.

  Lemma isok_iff : forall l, sort X.lt l <-> Ok l.

  Hint Extern 1 (Ok _) => rewrite <- isok_iff : core.

  Ltac inv_ok := match goal with
   | H:sort X.lt (_ :: _) |- _ => inversion_clear H; inv_ok
   | H:sort X.lt nil |- _ => clear H; inv_ok
   | H:sort X.lt ?l |- _ => change (Ok l) in H; inv_ok
   | H:Ok _ |- _ => rewrite <- isok_iff in H; inv_ok
   | |- Ok _ => rewrite <- isok_iff
   | _ => idtac
  end.

  Ltac inv := invlist InA; inv_ok; invlist lelistA.
  Ltac constructors := repeat constructor.

  Ltac sort_inf_in := match goal with
   | H:Inf ?x ?l, H':In ?y ?l |- _ =>
     cut (X.lt x y); [ intro | apply Sort_Inf_In with l; auto]
   | _ => fail
  end.

  Global Instance isok_Ok s `(isok s = true) : Ok s | 10.

  Definition Equal s s' := forall a : elt, In a s <-> In a s'.
  Definition Subset s s' := forall a : elt, In a s -> In a s'.
  Definition Empty s := forall a : elt, ~ In a s.
  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
  Definition Exists (P : elt -> Prop) (s : t) := exists x, In x s /\ P x.

  Lemma mem_spec :
   forall (s : t) (x : elt) (Hs : Ok s), mem x s = true <-> In x s.

  Lemma add_inf :
   forall (s : t) (x a : elt), Inf a s -> X.lt a x -> Inf a (add x s).
  Hint Resolve add_inf : core.

  Global Instance add_ok s x : forall `(Ok s), Ok (add x s).

  Lemma add_spec :
   forall (s : t) (x y : elt) (Hs : Ok s),
    In y (add x s) <-> X.eq y x \/ In y s.

  Lemma remove_inf :
   forall (s : t) (x a : elt) (Hs : Ok s), Inf a s -> Inf a (remove x s).
  Hint Resolve remove_inf : core.

  Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s).

  Lemma remove_spec :
   forall (s : t) (x y : elt) (Hs : Ok s),
    In y (remove x s) <-> In y s /\ ~X.eq y x.

  Global Instance singleton_ok x : Ok (singleton x).

  Lemma singleton_spec : forall x y : elt, In y (singleton x) <-> X.eq y x.

  Ltac induction2 :=
    simple induction s;
     [ simpl; auto; try solve [ intros; inv ]
     | intros x l Hrec; simple induction s';
        [ simpl; auto; try solve [ intros; inv ]
        | intros x' l' Hrec'; simpl; elim_compare x x'; intros; inv; auto ]].

  Lemma union_inf :
   forall (s s' : t) (a : elt) (Hs : Ok s) (Hs' : Ok s'),
   Inf a s -> Inf a s' -> Inf a (union s s').
  Hint Resolve union_inf : core.

  Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').

  Lemma union_spec :
   forall (s s' : t) (x : elt) (Hs : Ok s) (Hs' : Ok s'),
   In x (union s s') <-> In x s \/ In x s'.

  Lemma inter_inf :
   forall (s s' : t) (a : elt) (Hs : Ok s) (Hs' : Ok s'),
   Inf a s -> Inf a s' -> Inf a (inter s s').
  Hint Resolve inter_inf : core.

  Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s').

  Lemma inter_spec :
   forall (s s' : t) (x : elt) (Hs : Ok s) (Hs' : Ok s'),
   In x (inter s s') <-> In x s /\ In x s'.

  Lemma diff_inf :
   forall (s s' : t) (Hs : Ok s) (Hs' : Ok s') (a : elt),
   Inf a s -> Inf a s' -> Inf a (diff s s').
  Hint Resolve diff_inf : core.

  Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s').

  Lemma diff_spec :
   forall (s s' : t) (x : elt) (Hs : Ok s) (Hs' : Ok s'),
   In x (diff s s') <-> In x s /\ ~In x s'.

  Lemma equal_spec :
   forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'),
   equal s s' = true <-> Equal s s'.

  Lemma subset_spec :
   forall (s s' : t) (Hs : Ok s) (Hs' : Ok s'),
   subset s s' = true <-> Subset s s'.

  Global Instance empty_ok : Ok empty.

  Lemma empty_spec : Empty empty.

  Lemma is_empty_spec : forall s : t, is_empty s = true <-> Empty s.

  Lemma elements_spec1 : forall (s : t) (x : elt), In x (elements s) <-> In x s.

  Lemma elements_spec2 : forall (s : t) (Hs : Ok s), sort X.lt (elements s).

  Lemma elements_spec2w : forall (s : t) (Hs : Ok s), NoDupA X.eq (elements s).

  Lemma min_elt_spec1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s.

  Lemma min_elt_spec2 :
   forall (s : t) (x y : elt) (Hs : Ok s),
   min_elt s = Some x -> In y s -> ~ X.lt y x.

  Lemma min_elt_spec3 : forall s : t, min_elt s = None -> Empty s.

  Lemma max_elt_spec1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s.

  Lemma max_elt_spec2 :
   forall (s : t) (x y : elt) (Hs : Ok s),
   max_elt s = Some x -> In y s -> ~ X.lt x y.

  Lemma max_elt_spec3 : forall s : t, max_elt s = None -> Empty s.

  Definition choose_spec1 :
    forall (s : t) (x : elt), choose s = Some x -> In x s := min_elt_spec1.

  Definition choose_spec2 :
    forall s : t, choose s = None -> Empty s := min_elt_spec3.

  Lemma choose_spec3: forall s s' x x', Ok s -> Ok s' ->
   choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x'.

  Lemma fold_spec :
   forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
   fold f s i = fold_left (flip f) (elements s) i.

  Lemma cardinal_spec :
   forall (s : t) (Hs : Ok s),
   cardinal s = length (elements s).

  Lemma filter_inf :
   forall (s : t) (x : elt) (f : elt -> bool) (Hs : Ok s),
   Inf x s -> Inf x (filter f s).

  Global Instance filter_ok s f : forall `(Ok s), Ok (filter f s).

  Lemma filter_spec :
   forall (s : t) (x : elt) (f : elt -> bool),
   Proper (X.eq==>eq) f ->
   (In x (filter f s) <-> In x s /\ f x = true).

  Lemma for_all_spec :
   forall (s : t) (f : elt -> bool),
   Proper (X.eq==>eq) f ->
   (for_all f s = true <-> For_all (fun x => f x = true) s).

  Lemma exists_spec :
   forall (s : t) (f : elt -> bool),
   Proper (X.eq==>eq) f ->
   (exists_ f s = true <-> Exists (fun x => f x = true) s).

  Lemma partition_inf1 :
   forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s),
   Inf x s -> Inf x (fst (partition f s)).

  Lemma partition_inf2 :
   forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s),
   Inf x s -> Inf x (snd (partition f s)).

  Global Instance partition_ok1 s f : forall `(Ok s), Ok (fst (partition f s)).

  Global Instance partition_ok2 s f : forall `(Ok s), Ok (snd (partition f s)).

  Lemma partition_spec1 :
   forall (s : t) (f : elt -> bool),
   Proper (X.eq==>eq) f -> Equal (fst (partition f s)) (filter f s).

  Lemma partition_spec2 :
   forall (s : t) (f : elt -> bool),
   Proper (X.eq==>eq) f ->
   Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).

  End ForNotations.

  Definition In := InA X.eq.
  Instance In_compat : Proper (X.eq==>eq==> iff) In.

  Module L := MakeListOrdering X.
  Definition eq := L.eq.
  Definition eq_equiv := L.eq_equiv.
  Definition lt l1 l2 :=
    exists l1' l2', Ok l1' /\ Ok l2' /\ eq l1 l1' /\ eq l2 l2' /\ L.lt l1' l2'.

  Instance lt_strorder : StrictOrder lt.

  Instance lt_compat : Proper (eq==>eq==>iff) lt.

  Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').

  Lemma compare_spec : forall s s', Ok s -> Ok s' ->
   CompSpec eq lt s s' (compare s s').

End MakeRaw.

Encapsulation

Now, in order to really provide a functor implementing S, we need to encapsulate everything into a type of strictly ordered lists.

Module Make (X: OrderedType) <: S with Module E := X.
 Module Raw := MakeRaw X.
 Include Raw2Sets X Raw.
End Make.

For this specific implementation, eq coincides with Leibniz equality

Require Eqdep_dec.

Module Type OrderedTypeWithLeibniz.
  Include OrderedType.
  Parameter eq_leibniz : forall x y, eq x y -> x = y.
End OrderedTypeWithLeibniz.

Module Type SWithLeibniz.
  Declare Module E : OrderedTypeWithLeibniz.
  Include SetsOn E.
  Parameter eq_leibniz : forall x y, eq x y -> x = y.
End SWithLeibniz.

Module MakeWithLeibniz (X: OrderedTypeWithLeibniz) <: SWithLeibniz with Module E := X.
  Module E := X.
  Module Raw := MakeRaw X.
  Include Raw2SetsOn X Raw.

  Lemma eq_leibniz_list : forall xs ys, eqlistA X.eq xs ys -> xs = ys.

  Lemma eq_leibniz : forall s s', eq s s' -> s = s'.

End MakeWithLeibniz.