Library Coq.MSets.MSetWeakList

Finite sets library

This file proposes an implementation of the non-dependent interface MSetWeakInterface.S using lists without redundancy.

Require Import MSetInterface.
Set Implicit Arguments.

Functions over lists

First, we provide sets as lists which are (morally) without redundancy. The specs are proved under the additional condition of no redundancy. And the functions returning sets are proved to preserve this invariant.

The set operations.

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

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

  Definition empty : t := nil.

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

  Fixpoint mem (x : elt) (s : t) : bool :=
    match s with
    | nil => false
    | y :: l =>
           if X.eq_dec x y then true else mem x l
    end.

  Fixpoint add (x : elt) (s : t) : t :=
    match s with
    | nil => x :: nil
    | y :: l =>
        if X.eq_dec x y then s else y :: add x l
    end.

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

  Fixpoint remove (x : elt) (s : t) : t :=
    match s with
    | nil => nil
    | y :: l =>
        if X.eq_dec x y then l else y :: remove x l
    end.

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

  Definition union (s : t) : t -> t := fold add s.

  Definition diff (s s' : t) : t := fold remove s' s.

  Definition inter (s s': t) : t :=
    fold (fun x s => if mem x s' then add x s else s) s nil.

  Definition subset (s s' : t) : bool := is_empty (diff s s').

  Definition equal (s s' : t) : bool := andb (subset s s') (subset s' s).

  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 (s : t) : list elt := s.

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

End Ops.

Proofs of set operation specifications.

Module MakeRaw (X:DecidableType) <: WRawSets X.
  Include Ops X.

  Section ForNotations.
  Notation NoDup := (NoDupA X.eq).
  Notation In := (InA X.eq).

  Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
  Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
  Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
  Hint Resolve eqr eqtrans : core.
  Hint Immediate eqsym : core.

  Definition IsOk := NoDup.

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

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

  Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.

  Ltac inv_ok := match goal with
   | H:Ok (_ :: _) |- _ => inversion_clear H; inv_ok
   | H:Ok nil |- _ => clear H; inv_ok
   | H:NoDup ?l |- _ => change (Ok l) in H; inv_ok
   | _ => idtac
  end.

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

  Fixpoint isok l := match l with
   | nil => true
   | a::l => negb (mem a l) && isok l
  end.

  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 := exists x, In x s /\ P x.

  Lemma In_compat : Proper (X.eq==>eq==>iff) In.

  Lemma mem_spec : forall s x `{Ok s},
   mem x s = true <-> In x s.

  Lemma isok_iff : forall l, Ok l <-> isok l = true.

  Global Instance isok_Ok l : isok l = true -> Ok l | 10.

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

  Global Instance add_ok s x `(Ok s) : Ok (add 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 remove_ok s x `(Ok s) : Ok (remove x s).

  Lemma singleton_ok : forall x : elt, Ok (singleton x).

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

  Lemma 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_spec2w : forall (s : t) {Hs : Ok s}, NoDup (elements s).

  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.

  Global Instance union_ok : forall s s' `(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'.

  Global Instance inter_ok s s' `(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'.

  Global Instance diff_ok : forall s s' `(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 subset_spec :
   forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'},
   subset s s' = true <-> Subset s s'.

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

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

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

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

  Lemma filter_spec' : forall s x f,
   In x (filter f s) -> In x 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).

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

  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_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).

  Lemma partition_ok1' :
   forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt),
    In x (fst (partition f s)) -> In x s.

  Lemma partition_ok2' :
   forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt),
    In x (snd (partition f s)) -> In x s.

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

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

  End ForNotations.

  Definition In := InA X.eq.
  Definition eq := Equal.
  Instance eq_equiv : Equivalence eq := _.

End MakeRaw.

Encapsulation

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