(***************************************************************************
* A Library for Finite Sets with Leibnitz Equality                         *
* Arthur Charguéraud, March 2007, Coq v8.1                                 *
***************************************************************************)

Set Implicit Arguments.
Require Import LibTactics List OrderedTypeEx.


Module FinSet (E : UsualOrderedType).


(* ********************************************************************** *)
(** * Abstract interface for finite sets *)

(** Type of elements. *)

Notation "'item'" := (E.t) : fset_scope_def.

Open Local Scope fset_scope_def.

(** Definitions and operations on finite sets *)

Parameter fset : Set.
Parameter empty : fset.
Parameter singleton : item -> fset.
Parameter union : fset -> fset -> fset.
Parameter remove : fset -> fset -> fset.
Parameter inter : fset -> fset -> fset.
Parameter of_list : fset -> list item. 
Parameter from_list : list item -> fset.
Parameter mem : item -> fset -> Prop.

(** Equality on these sets is extensional *)

Definition subset E F :=
  forall x, mem x E -> mem x F.

Definition exteq E F := 
  subset E F /\ subset F E.

Parameter exteq_to_eq : forall E F, 
  exteq E F -> E = F.

Definition notin x E :=
  ~ mem x E.

Definition disjoint E F :=
  inter E F = empty.

(** Notations *)

Notation "{}" := (empty) : fset_scope.

Notation "{{ x }}" := (singleton x) : fset_scope.

Notation "E \u F" := (union E F)
  (at level 68, left associativity) : fset_scope.

Notation "x \in E" := (mem x E) (at level 69) : fset_scope.

Notation "x \notin E" := (notin x E) (at level 69) : fset_scope.

Notation "E << F" := (subset E F) (at level 70) : fset_scope.

Notation "E \rem F" := (remove E F) (at level 70) : fset_scope.

Delimit Scope fset_scope with fset.
Bind Scope fset_scope with fset.
Open Local Scope fset_scope.


(* ********************************************************************** *)
(** * Facts about finite sets *)

(** Interaction of in with constructions *)

Parameter in_empty : forall x,
  x \in {} -> False.

Parameter in_singleton : forall x y,
  x \in {{y}} <-> x = y.

Parameter in_union : forall x E F,
  x \in (E \u F) <-> (x \in E) \/ (x \in F).

(** Properties of union *)

Lemma union_same : forall E,
  E \u E = E.
Proof.
  intros. apply exteq_to_eq. split; 
   intros x; rewrite_all* in_union.
Qed.

Lemma union_comm : forall E F,
  E \u F = F \u E.
Proof.
  intros. apply exteq_to_eq. split;
   intros x; rewrite_all* in_union.
Qed.

Lemma union_assoc : forall E F G,
  E \u (F \u G) = (E \u F) \u G.
Proof.
  intros. apply exteq_to_eq. split;
   intros x; rewrite_all* in_union.
Qed.

Lemma union_empty_l : forall E,
  {} \u E = E.
Proof.
  intros. apply exteq_to_eq. split; 
   intros x; rewrite_all in_union.
    intros [ H | H ]. false. apply* in_empty. auto.
    auto*.
Qed.

(** More properties of in *)

Lemma in_singleton_self : forall x,
  x \in {{x}}.
Proof. intros. rewrite~ in_singleton. Qed.

(** More properties of union *)

Lemma union_empty_r : forall E,
  E \u {} = E.
Proof. intros. rewrite union_comm. apply union_empty_l. Qed.

Lemma union_comm_assoc : forall E F G,
  E \u (F \u G) = F \u (E \u G).
Proof.
  intros. rewrite union_assoc.
  rewrite (union_comm E F).
  rewrite~ <- union_assoc.
Qed.

(** Subset relation properties *)

Lemma subset_refl : forall E,
  E << E.
Proof. intros_all~. Qed.

Lemma subset_trans : forall F E G,
  E << F -> F << G -> E << G.
Proof. intros_all~. Qed.

(** Interaction of subset with constructions *)

Lemma subset_empty_l : forall E,
  {} << E.
Proof. intros_all. false. apply* in_empty. Qed.

Lemma subset_singleton : forall x E,
  x \in E <-> {{x}} << E.
Proof.
  split; introv H. 
  introv M. rewrite in_singleton in M. subst*.
  apply H. apply in_singleton_self.
Qed.

Lemma subset_union_weak_l : forall E F,
  E << (E \u F).
Proof. intros_all. rewrite~ in_union. Qed.

Lemma subset_union_weak_r : forall E F,
  F << (E \u F).
Proof. intros_all. rewrite~ in_union. Qed.

Lemma subset_union_l : forall E F G,
  (E \u F) << G <-> (E << G) /\ (F << G).
Proof.
  split; introv H.
    split; intros_all.
      apply H. apply* subset_union_weak_l.
      apply H. apply* subset_union_weak_r.
    introv M. rewrite* in_union in M.
Qed.

(** Proving subset relations using \notin *)

Axiom subset_by_notin : forall E F,
  (forall x, x \notin F -> x \notin E) ->
  E << F.
(* TODO: il faudrait mettre mem dans bool ! 
  Proof.
  introv H IE. unfolds notin. auto*.
*)

(** Interaction of notin with constructions *)

Lemma notin_empty : forall x,
  x \notin {}.
Proof. intros_all. apply* in_empty. Qed.

Lemma notin_singleton : forall x y,
  x \notin {{y}} <-> x <> y.
Proof. unfold notin. intros. rewrite* <- in_singleton. Qed.

Lemma notin_same : forall x,
  x \notin {{x}} -> False.
Proof. intros. apply H. apply* in_singleton_self. Qed.

Lemma notin_union : forall x E F,
  x \notin (E \u F) <-> (x \notin E) /\ (x \notin F).
Proof. unfold notin. intros. rewrite* in_union. Qed.


End FinSet.



(* todo: pb level parsing on \rem *)