Require Import MSetInterface.
Set Implicit Arguments.

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) (s : t) (i : B) : B :=
    fold_left (flip f) s i.

  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.

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

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

  Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
  Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
  Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).

  Definition IsOk := NoDup.

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

  Hint Unfold Ok.
  Hint Resolve @ok.

  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.

Module Make (X: DecidableType) <: WSets with Module E := X.
 Module Raw := MakeRaw X.
 Include WRaw2Sets X Raw.
End Make.