Require Export MSetInterface OrdersFacts OrdersLists.
Set Implicit Arguments.

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.

  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 :=
    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.

  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 Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
  Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
  Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).

  Definition IsOk s := Sort s.

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

  Hint Resolve @ok.
  Hint Unfold Ok.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

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

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.