Stlc.OrdSet

Require Import MSetList MSets Structures.Orders Eqdep_dec.

Module BoolDec <: DecidableType.
    Definition U := bool.
    Definition eq_dec := Bool.bool_dec.
End BoolDec.

Module Type SetExtT.
  Include SWithLeibniz.
  Parameter Disjoint : t -> t -> Prop.
  Axiom Disjoint_spec : forall m m', Disjoint m m' <-> forall k, ~ (In k m /\ In k m').
  Parameter set_extensionality :
    forall (X Y : t), (forall (x : elt), In x X <-> In x Y) -> X = Y.
  Parameter set_map : (elt -> elt) -> t -> t.
  Axiom set_map_spec : forall (f : elt -> elt) (X : t) (e : elt),
      In e X -> In (f e) (set_map f X).
  Axiom set_map_spec_1 : forall (f : elt -> elt) (X : t) (e e' : elt),
      In e X -> e' = f e -> In e' (set_map f X).
  Axiom set_map_iff : forall (f : elt -> elt) (X : t) e,
    In e (set_map f X) <-> exists e', e = f e' /\ In e' X.
  Axiom union_assoc :
    forall s s' s'' : t, (union (union s s') s'') = (union s (union s' s'')).
  Axiom union_comm : forall s s' : t, union s s' = union s' s.
  Axiom set_map_card : forall f s, cardinal (set_map f s) = cardinal s.
End SetExtT.

Module SetExt (E : UsualOrderedType) <: SetExtT.
  Module SLeib <: MSetList.OrderedTypeWithLeibniz.
  Include E.
  Lemma eq_leibniz : forall x y, eq x y -> x = y.
  Proof.
    intros x y Heq. auto.
  Qed.
  End SLeib.
  Module S := MSetList.MakeWithLeibniz SLeib.

  Include S.

  Module OP := OrdProperties S.
  Import OP.

  Module Dec := DecidableEqDep BoolDec.

  Lemma set_extensionality (X Y : t):
    (forall (x : elt), In x X <-> In x Y) -> X = Y.
  Proof.
    intros Hin.
    destruct X as [xs sxs]. destruct Y as [ys sys].
    assert (Heq : xs = ys) by
        (apply eq_leibniz_list;
         apply OP.sort_equivlistA_eqlistA; try rewrite Raw.isok_iff; auto).
    subst. f_equal.
    (* NOTE: We can solve this goal without assuming proof irrelevance, because
       for types with decidable equality UIP in provable *)
    apply Dec.UIP.
  Qed.

  Definition set_map (f : elt -> elt) (X : t) : t :=
    fold (fun x Y => add (f x) Y) X empty.

  Lemma set_map_spec (f : elt -> elt) (X : t) : forall (e : elt),
    In e X -> In (f e) (set_map f X).
  Proof.
    (* NOTE: it is very convenient to use special induction principle for fold here *)
    apply P.fold_rec with (P:=fun X Y => forall e, In e X -> In (f e) Y).
    + intros. exfalso. unfold S.Empty in *. apply (H e);auto.
    + intros. apply P.FM.add_iff. destruct (H1 e). intuition. subst. auto.
  Qed.

  Lemma set_map_spec_1 (f : elt -> elt) (X : t) : forall (e e' : elt),
    In e X -> e' = f e -> In e' (set_map f X).
  Proof.
    intros. subst. apply set_map_spec;auto.
  Qed.

  Lemma set_map_iff (f : elt -> elt) (X : t) : forall e,
    In e (set_map f X) <-> exists e', e = f e' /\ In e' X.
  Proof.
    intros e.
    split.
    + revert e. apply P.fold_rec with
          (P := fun x' Y => forall e, In e Y -> exists e', e = f e' /\ In e' X).
      intros s' H' e He.
      * inversion He.
      * intros x a Y Y' Hx Hx' Hadd IH e He. apply P.FM.add_iff in He. intuition.
        subst. exists x. unfold P.Add in *. destruct (Hadd x);intuition.
    + intros. destruct H. intuition. subst.
      apply set_map_spec;auto.
  Qed.

  Definition Disjoint (m m' : t) :=
    forall k, ~ (In k m /\ In k m').

  Lemma Disjoint_spec m m' : Disjoint m m' <-> forall k, ~ (In k m /\ In k m').
  Proof.
    split;auto.
  Qed.

  Lemma union_assoc :
    forall s s' s'' : S.t, (S.union (S.union s s') s'') = (S.union s (S.union s' s'')).
  Proof.
    intros. apply set_extensionality. apply P.union_assoc.
  Qed.

  Lemma union_comm : forall s s' : S.t, S.union s s' = S.union s' s.
  Proof.
    intros.
    apply set_extensionality. intros.
    split;intros; apply P.Dec.F.union_1 in H; intuition;auto with set.
  Qed.
  Axiom set_map_card : forall f s, cardinal (set_map f s) = cardinal s.
End SetExt.