Set Implicit Arguments.
Generalizable Variables A B.
Require Import Coq.Classes.Morphisms. From TLC Require Import LibTactics LibLogic LibReflect LibList
  LibOperation LibMonoid LibInt LibNat
  LibEpsilon LibRelation LibMin.
From TLC Require Export LibContainer.

Definition set (A : Type) := A -> Prop.

Section Operations.
Variables (A B : Type).
Implicit Types x : A.
Implicit Types E F G : set A.

Definition set_st (P:A->Prop) : set A :=
  P.

Definition empty_impl : set A :=
  (fun _ => False).

Definition full_impl : set A :=
  (fun _ => True).

Definition single_impl x :=
  (= x).

Definition in_impl x E :=
  E x.

Definition compl_impl : set A -> set A :=
  @pred_not A.
Definition union_impl : set A -> set A -> set A :=
  @pred_or A.

Definition inter_impl : set A -> set A -> set A :=
  @pred_and A.

Definition remove_impl : set A -> set A -> set A :=
  fun E F x => E x /\ ~ F x.

Definition incl_impl : set A -> set A -> Prop :=
  @pred_incl A.

Definition disjoint_impl : set A -> set A -> Prop :=
  fun E F : set A => inter_impl E F = empty_impl.

Definition list_repr_impl (E:set A) (l:list A) :=
  noduplicates l /\ forall x, mem x l <-> E x.

Definition to_list (E:set A) :=
  epsilon (list_repr_impl E).

Definition to_set (xs : list A) : set A :=
  set_st (fun x => mem x xs).

Definition list_covers_impl (E:set A) L :=
  forall x, E x -> mem x L.

Definition finite (E:set A) :=
  exists L, list_covers_impl E L.

Definition card_impl (E:set A) : nat :=
  mmin le (fun n => exists L, list_covers_impl E L /\ n = length L).

Definition fold_impl (m:monoid_op B) (f:A->B) (E:set A) :=
  LibList.fold_right (fun x acc => monoid_oper m (f x) acc)
    (monoid_neutral m) (to_list E).

End Operations.

Notation "x \indom E" := (x \in (dom E : set _))
  (at level 39) : container_scope.

Notation "x \notindom E" := (x \notin ((dom E) : set _))
  (at level 39) : container_scope.

Instance Inhab_set : forall A, Inhab (set A).
Proof using. intros. apply (Inhab_of_val (@empty_impl A)). Qed.

Lemma in_inst : forall A, BagIn A (set A).
Proof using. constructor. exact (@in_impl A). Defined.

Hint Extern 1 (BagIn _ (set _)) => apply in_inst : typeclass_instances.

Instance empty_inst : forall A, BagEmpty (set A).
  constructor. apply (@empty_impl A). Defined.

Instance single_inst : forall A, BagSingle A (set A).
  constructor. rapply (@single_impl A). Defined.

Instance union_inst : forall A, BagUnion (set A).
  constructor. rapply (@union_impl A). Defined.

Instance inter_inst : forall A, BagInter (set A).
  constructor. rapply (@inter_impl A). Defined.

Instance remove_inst : forall A, BagRemove (set A) (set A).
  constructor. rapply (@remove_impl A). Defined.

Instance incl_inst : forall A, BagIncl (set A).
  constructor. rapply (@incl_impl A). Defined.

Instance disjoint_inst : forall A, BagDisjoint (set A).
  constructor. rapply (@disjoint_impl A). Defined.

Instance fold_inst : forall A B, BagFold B (A->B) (set A).
  constructor. rapply (@fold_impl A B). Defined.

Instance card_inst : forall A, BagCard (set A).
  constructor. rapply (@card_impl A). Defined.

Global Opaque set finite in_inst empty_inst single_inst union_inst inter_inst
  remove_inst incl_inst disjoint_inst card_inst fold_inst.

Definition list_repr A (E:set A) (L:list A) :=
  noduplicates L /\ (forall x, mem x L <-> x \in E).

Definition list_covers A (E:set A) (L:list A) :=
  forall x, x \in E -> mem x L.

Notation "\set{ x | P }" := (@set_st _ (fun x => P))
 (at level 0, x ident, P at level 200) : set_scope.
Notation "\set{ x : A | P }" := (@set_st A (fun x => P))
 (at level 0, x ident, P at level 200) : set_scope.
Notation "\set{ x '\in' E | P }" := (@set_st _ (fun x => x \in E /\ P))
 (at level 0, x ident, P at level 200) : set_scope.

Notation "\set{= e | x '\in' E }" :=
 (@set_st _ (fun a => exists_ x \in E, a = e ))
 (at level 0, x ident, E at level 200) : set_scope.
Notation "\set{= e | x '\in' E , y ''\in' F }" :=
 (@set_st _ (fun a => exists_ x \in E, exists_ y \in F, a = e ))
 (at level 0, x ident, F at level 200) : set_scope.
Notation "\set{= e | x y '\in' E }" :=
 (@set_st _ (fun a => exists_ x y \in E, a = e ))
 (at level 0, x ident, y ident, E at level 200) : set_scope.

Section Instances.
Variables (A:Type).
Implicit Types E F : set A.

Transparent set finite empty_inst single_inst single_impl in_inst
  incl_inst inter_inst union_inst card_inst fold_inst remove_inst
  disjoint_inst.
Hint Constructors mem.

Ltac set_unf := unfold finite,
  card_inst, card_impl, card,
  to_list,
  disjoint_impl, disjoint_inst, disjoint,
  incl_inst, incl_impl,
  empty_inst, empty_impl, empty,
  single_inst, single_impl, single,
  in_inst, in_impl, is_in,
  incl_inst, incl_impl, incl,
  compl_impl, pred_not,
  inter_inst, inter_impl, inter, pred_and,
  union_inst, union_impl, union, pred_or,
  remove_inst, remove_impl, remove,
  fold_inst, fold_impl, fold in *.

Lemma disjoint_eq_inter_empty : forall E F,
  (E \# F) = (E \n F = \{}).
Proof using. auto. Qed.

Lemma in_set_st_eq : forall (P:A->Prop) x,
  x \in set_st P = P x.
Proof using. intros. apply* prop_ext. Qed.

Lemma set_ext_eq : forall E F,
  (E = F) = (forall (x:A), x \in E <-> x \in F).
Proof using.
  intros. apply prop_ext. iff H. subst*. extens*.
Qed.

Lemma set_ext : forall E F,
  (forall (x:A), x \in E <-> x \in F) ->
  E = F.
Proof using. intros. rewrite~ set_ext_eq. Qed.

Lemma set_st_eq : forall A (P Q : A -> Prop),
  (forall (x:A), P x <-> Q x) ->
  set_st P = set_st Q.
Proof using. intros. asserts_rewrite~ (P = Q). extens~. Qed.

Global Instance in_extens_inst : In_extens (A:=A) (T:=set A).
Proof using. constructor. intros. rewrite* set_ext_eq. Qed.

Global Instance in_empty_eq_inst : In_empty_eq (A:=A) (T:=set A).
Proof using. constructor. intros. apply* prop_ext. Qed.

Global Instance in_single_eq_inst : In_single_eq (A:=A) (T:=set A).
Proof using. constructor. intros. apply* prop_ext. Qed.

Global Instance in_union_eq_inst : In_union_eq (A:=A) (T:=set A).
Proof using. constructor. intros. set_unf. simpl. apply* prop_ext. Qed.

Global Instance in_inter_eq_inst : In_inter_eq (A:=A) (T:=set A).
Proof using. constructor. intros. set_unf. apply* prop_ext. Qed.

Global Instance in_remove_eq_inst : In_remove_eq (A:=A) (T:=set A).
Proof using. constructor. intros. set_unf. applys* prop_ext. Qed.

Global Instance incl_in_eq_inst : Incl_in_eq (A:=A) (T:=set A).
Proof using. constructor. intros. set_unf. autos*. Qed.

Global Instance disjoint_eq_inst : Disjoint_eq (T:=set A).
Proof using.
  constructor. intros. rewrite disjoint_eq_inter_empty.
  set_unf. applys prop_ext. iff M.
    intros x. rewrite* <- (@fun_eq_1 _ _ x _ _ M).
    extens*.
Qed.



Lemma eq_union_single_remove_one : forall E x,
  x \in E ->
  E = \{x} \u (E \-- x).
Proof using.
  introv H. set_unf. extens. intros y. iff M.
    simpls. tests*: (y = x).
    destruct M. subst*. autos*.
Qed.

Lemma set_remove_one_add_same : forall E x,
  x \notin E ->
  E = (E \u \{x}) \-- x.
Proof using.
  introv Hx. set_unf. extens. iff.
  { split. eauto. intro. subst*. }
  { tauto. }
Qed.

Lemma list_covers_of_list_repr : forall E L,
  list_repr E L ->
  list_covers E L.
Proof using. introv (ND&EQ). introv Hx. rewrite~ EQ. Qed.

Lemma list_repr_disjoint_union : forall E F LE LF,
  E \# F ->
  list_repr E LE ->
  list_repr F LF ->
  list_repr (E \u F) (LE ++ LF).
Proof using.
  introv D (HE&QE) (HF&QF). split.
  applys~ noduplicates_app.
    intros x ? ?. applys* @disjoint_inv x.
      typeclass. rewrite~ <- QE. rewrite~ <- QF.
    intros x. rewrite mem_app_eq. rewrite in_union_eq.
      rewrite <- QE. rewrite* <- QF.
Qed.

Lemma noduplicates_of_list_repr : forall E xs,
  list_repr E xs ->
  noduplicates xs.
Proof using. unfold list_repr. tauto. Qed.

Lemma ex_list_repr_impl_of_ex_list_covers_impl : forall E,
  ex (list_covers_impl E) ->
  ex (list_repr_impl E).
Proof using.
  introv (L&M). sets_eq L1 EQL1: (remove_duplicates L).
  forwards~ (HN&HM&_): remove_duplicates_spec EQL1.
  sets L2: (filter (fun x => x \in E) L1).
  exists L2. split.
    applys* noduplicates_filter.
    intros x. specializes M x. rewrite <- HM in M. set_unf. iff N.
      subst L2. forwards*: mem_filter_inv N.
      applys* mem_filter.
Qed.

Lemma list_repr_to_list_of_finite : forall E,
  finite E ->
  list_repr E (to_list E).
Proof using.
  introv FE. unfolds to_list, finite, list_repr_impl.
  epsilon~ L'.
  applys~ ex_list_repr_impl_of_ex_list_covers_impl.
Qed.

Lemma eq_to_list_inv : forall E L,
  L = to_list E ->
  finite E ->
  list_repr E L.
Proof.
  introv EQ HE. unfolds. subst. forwards* (?&?): list_repr_to_list_of_finite HE.
Qed.

Lemma finite_eq_in_iff_mem_to_list : forall E,
  finite E = (forall x, x \in E <-> mem x (to_list E)).
Proof.
  intros. applys prop_ext. iff M.
  { forwards* (N1&N2): eq_to_list_inv E. intros x. specializes N2 x. autos*. }
  { exists (to_list E). intros x Ex. rewrite~ <- M. }
Qed.

Lemma to_list_empty :
  to_list (\{}:set A) = nil.
Proof using.
  set_unf. epsilon l.
  { exists (@nil A). split. { constructor. } { intros. rewrite* mem_nil_eq. } }
  intros Hl. inverts Hl. simpls. destruct~ l. false. rewrite <- H0. simple~.
Qed.

Lemma to_list_single : forall (x:A),
  to_list (\{x}) = x::nil.
Proof using.
  intros. unfold to_list. epsilon l.
  { exists (x::nil). split.
   { applys noduplicates_one. }
   { unfold single_inst, single_impl. simple~.
     intros. rewrite* mem_one_eq. } }
  introv Hl. unfolds single_inst, single_impl. simpls~.
  inverts Hl as H H0. destruct (H0 x). specializes~ H2.
  destruct l.
  { inverts H2. }
  { tests E: (x = a).
    { fequals. destruct l. auto. forwards~: (proj1 (H0 a0)).
      subst. inverts H as M1 M2. false* M1. }
    { inverts H2. false. forwards~: (proj1 (H0 a)). false. } }
Qed.

Lemma finite_of_list_covers : forall (E:set A) L,
  list_covers E L ->
  finite E.
Proof using. introv H. exists* L. Qed.

Lemma finite_of_list_repr : forall (E:set A) L,
  list_repr E L ->
  finite E.
Proof using. introv (ND&EQ). exists~ L. introv Hx. rewrite~ EQ. Qed.

Lemma finite_of_ex_list_covers : forall (E:set A),
  ex (list_covers E) ->
  finite E.
Proof using. introv (L&H). applys* finite_of_list_covers. Qed.


Definition finite_inv_list_covers_and_card : forall (E:set A),
  finite E ->
  exists L, list_covers E L /\ card E = length L.
Proof.
  introv (L&H). sets m: (card E).
  forwards* (R&P): mmin_spec_nat m.
Qed.

Lemma finite_inv_list_covers : forall (E:set A),
  finite E ->
  exists L, list_covers E L.
Proof using. introv (L&HN). exists L. intros. applys* HN. Qed.


Lemma finite_empty :
  finite (\{} : set A).
Proof using.
  intros. apply finite_of_ex_list_covers. set_unf.
  exists (@nil A). introv M. inverts M.
Qed.

Lemma finite_single : forall (a : A),
  finite \{a}.
Proof using.
  intros. apply finite_of_ex_list_covers. set_unf.
  exists (a::nil). introv M. hnf in M. subst*.
Qed.

Lemma finite_union : forall E F,
  finite E ->
  finite F ->
  finite (E \u F).
Proof using.
  introv H1 H2. apply finite_of_ex_list_covers.
  lets (L1&E1): finite_inv_list_covers H1.
  lets (L2&E2): finite_inv_list_covers H2.
  exists (L1++L2). unfolds list_covers.
  introv M.
  rewrite @in_union_eq in M; try typeclass.
  rewrite* mem_app_eq.
Qed.

Lemma finite_inter : forall E F,
  finite E \/ finite F ->
  finite (E \n F).
Proof using.
  introv H. apply finite_of_ex_list_covers. destruct H.
  lets (L&EQ): finite_inv_list_covers H. exists L. unfold list_covers. set_unf. autos*.
  lets (L&EQ): finite_inv_list_covers H. exists L. unfold list_covers. set_unf. autos*.
Qed.

Lemma finite_incl : forall E F,
  E \c F ->
  finite F ->
  finite E.
Proof using.
  introv HI HF. apply finite_of_ex_list_covers.
  lets (L&EQ): finite_inv_list_covers HF. unfold list_covers.
  set_unf. exists* L. introv Ex. applys EQ. applys~ HI.
Qed.

Lemma finite_remove : forall E F,
  finite E ->
  finite (E \- F).
Proof using.
  introv HE. apply finite_of_ex_list_covers.
  lets (L&EQ): finite_inv_list_covers HE. unfold list_covers. set_unf. exists* L.
Qed.

Section Finite_remove_inv.
Local Opaque remove_inst single_inst.

Lemma finite_remove_inv : forall E F,
  finite (E \- F) ->
  finite F ->
  finite E.
Proof using.
  introv H1 H2. lets (L1&R1): finite_inv_list_covers H1.
  lets (L2&R2): finite_inv_list_covers H2.
  applys finite_of_list_covers (L1 ++ L2).
  intros y Hy. rewrite~ mem_app_eq. tests: (y \in F).
    autos~.
    forwards~ M: R1 y. rewrite~ @in_remove_eq. typeclass.
Qed.

End Finite_remove_inv.

Lemma finite_remove_one_inv : forall E x,
  finite (E \-- x) ->
  finite E.
Proof using.
  introv H. applys finite_remove_inv H. applys finite_single.
Qed.



Lemma list_repr_nil:
  list_repr \{} (@nil A).
Proof using.
  rewrite <- to_list_empty.
  eapply eq_to_list_inv; eauto using finite_empty.
Qed.

Definition list_covers_inv_card : forall (E:set A) L,
  list_covers E L ->
  (card E <= length L)%nat.
Proof using.
  introv H. sets m: (card E). set_unf.
  forwards* (R&P): mmin_spec_nat m.
  simpls. applys P. exists L. splits~.
Qed.

Definition finite_inv_list_repr_and_card : forall (E:set A),
  finite E ->
  exists L, list_repr E L /\ card E = length L.
Proof.
  introv H. forwards (L1&HL1&EL1): finite_inv_list_covers_and_card H.
  sets L2: (remove_duplicates L1).
  forwards~ (ND&EQ&LE): remove_duplicates_spec L1 L2.
  sets L3: (filter (fun x => x \in E) L2).
  asserts: (length L3 <= length L2)%nat. applys length_filter.
  asserts R3: (list_repr E L3).
    split.
      applys~ noduplicates_filter.
      intros x. iff M.
        unfold L3 in M. lets~ (_&?): mem_filter_inv M.
        applys~ mem_filter. rewrite~ EQ.
  forwards C3: list_covers_of_list_repr R3.
  exists L3. splits*.
  forwards: list_covers_inv_card C3. math.
Qed.

Lemma list_repr_inv_card : forall (E:set A) (L:list A),
  list_repr E L ->
  card E = length L.
Proof using.
  introv HR. lets (ND&EQ): HR.
  forwards~ (L'&(ND'&HR')&EQ'): finite_inv_list_repr_and_card E.
    applys* finite_of_list_repr.
  unfold card. simpl. rewrite EQ'.
  applys~ noduplicates_length_eq.
  intros x. rewrite EQ. rewrite* HR'.
Qed.

Definition finite_inv_card_ge : forall (E:set A) n,
  finite E ->
  (forall L, list_covers E L -> (length L >= n)%nat) ->
  (card E >= n)%nat.
Proof using.
  introv H. sets m: (card E).
  forwards* (R&P): mmin_spec_nat m.
    lets (L&EL): finite_inv_list_covers H. exists~ (length L) L.
  simpls. introv HL. destruct R as (L&CR&ER).
  forwards~: HL L. math.
Qed.

Definition list_covers_inv_card_eq : forall (E:set A) L,
  list_covers E L ->
  (forall L', list_covers E L' -> (length L' >= length L)%nat) ->
  card E = length L.
Proof using.
  introv HC HG.
  forwards~: list_covers_inv_card HC.
  forwards~: finite_inv_card_ge HG.
    applys* finite_of_list_covers.
  math.
Qed.

Lemma card_eq_length_to_list : forall (E:set A),
  finite E ->
  card E = length (to_list E).
Proof using.
  introv FE. applys list_repr_inv_card. applys~ eq_to_list_inv.
Qed.


Global Instance card_empty_inst : Card_empty (T:=set A).
Proof using.
  constructor. rewrite card_eq_length_to_list.
  lets E: to_list_empty. set_unf. rewrite E. rew_list~.
  applys finite_empty.
Qed.

Global Instance card_single_inst : Card_single (T:=set A).
Proof using.
  constructor. intros a. rewrite card_eq_length_to_list.
  lets E: to_list_single a. set_unf. rewrite E. rew_list~.
  applys finite_single.
Qed.

End Instances.

Hint Resolve finite_empty finite_single finite_union
  finite_inter finite_incl finite_remove : finite.

Section Autorewrite.
Variables (A : Type).
Implicit Types x y : A.
Implicit Types E F : set A.

Lemma set_in_empty_eq : forall x,
  x \in (\{}:set A) = False.
Proof using. apply in_empty_eq. Qed.

Lemma set_in_single_eq : forall x y,
  x \in (\{y}:set A) = (x = y).
Proof using. apply in_single_eq. Qed.

Lemma set_in_inter_eq : forall x E F,
  x \in (E \n F) = (x \in E /\ x \in F).
Proof using. apply in_inter_eq. Qed.

Lemma set_in_union_eq : forall x E F,
  x \in (E \u F) = (x \in E \/ x \in F).
Proof using. apply in_union_eq. Qed.

Lemma set_in_remove_eq : forall x E F,
  x \in (E \- F) = (x \in E /\ ~ x \in F).
Proof using. apply in_remove_eq. Qed.

Lemma set_in_extens_eq : forall E F,
  (E = F) = (forall x, x \in E <-> x \in F).
Proof using.
  extens. iff M.
  subst*.
  applys @in_extens_eq. typeclass. intros. extens*.
Qed.

Lemma set_incl_in_eq : forall E F,
  (E \c F) = (forall x, x \in E -> x \in F).
Proof using. apply incl_in_eq. Qed.

Lemma set_disjoint_eq : forall E F,
  (E \# F) = (forall x, x \in E -> x \in F -> False).
Proof using. apply disjoint_eq. Qed.

End Autorewrite.

Hint Rewrite in_set_st_eq set_in_empty_eq set_in_single_eq
  set_in_inter_eq set_in_union_eq set_in_remove_eq set_in_extens_eq
  set_incl_in_eq set_disjoint_eq : rew_set.


Ltac rew_set_tactic tt :=
  autorewrite_in_star_patch ltac:(fun tt => autorewrite with rew_set).

Ltac set_specialize_hyps A x :=
  repeat match goal with H: forall _:?A, _ |- _ =>
    specializes H x
  end.

Ltac set_specialize_classic x :=
  repeat match goal with E: set _ |- _ =>
    match goal with
    | H: x \in E \/ ~ x \in E |- _ => fail 1
    | _ => lets: (prop_inv (x \in E))
    end
  end.

Ltac set_specialize use_classic :=
  match goal with |- forall _:?A, _ =>
    let x := fresh "x" in intros x;
    set_specialize_hyps A x;
    match use_classic with
    | true => set_specialize_classic x
    | false => idtac
    end
  end.

Ltac set_prove_setup use_classic :=
  intros;
  rew_set_tactic tt;
  try set_specialize use_classic;
  rew_set_tactic tt.

Ltac set_prove_conclude :=
  solve [ intros; subst; tauto ].

Ltac set_prove :=
  set_prove_setup false; set_prove_conclude.

Ltac set_prove_classic :=
  set_prove_setup true; set_prove_conclude.

Lemma card_le_of_incl : forall A (E F:set A),
  finite F ->
  E \c F ->
  (card E <= card F)%nat.
Proof using.
  introv FF CF. lets FE: finite_incl CF FF.
  lets (LF&RF&QF): finite_inv_list_covers_and_card FF.
  rewrite QF. applys list_covers_inv_card. introv Ex.
  applys RF. applys* @incl_inv. typeclass.
Qed.

Lemma card_union_le : forall A (E F:set A),
  finite E ->
  finite F ->
  card (E \u F) <= (card E + card F)%nat.
Proof using.
  introv FE FF.
  lets (LE&RE&QE): finite_inv_list_covers_and_card FE.
  lets (LF&RF&QF): finite_inv_list_covers_and_card FF.
  lets H: list_covers_inv_card (E \u F) (LE++LF) __.
    unfolds list_covers. intros. apply mem_app.
    rewrite in_union_eq in H. autos*.
  rew_list in H. math.
Qed.

Lemma card_disjoint_union : forall A (E F:set A),
  finite E ->
  finite F ->
  E \# F ->
  card (E \u F) = (card E + card F)%nat.
Proof using.
  introv FE FF EF.
  forwards: card_union_le FE FF.
  cuts: (card (E \u F) >= (card E + card F)%nat). math. clear H.
  forwards (L&LC&LL): finite_inv_list_covers_and_card (E \u F). applys~ finite_union.
  rewrite LL. clear LL.
  sets PE: (fun x => x \in E). sets LE: (filter PE L).
  sets PF: (fun x => x \in F). sets LF: (filter PF L).
  forwards: list_covers_inv_card E LE.
    unfold LE, PE. introv Ex. forwards: LC x. set_prove. applys~ mem_filter.
  forwards: list_covers_inv_card F LF.
    unfold LF, PF. introv Fx. forwards: LC x. set_prove. applys~ mem_filter.
  forwards LEF: filter_length_two_disjoint PE PF L.
    introv _ HEx HFx. unfolds PE, PF. applys* @disjoint_inv. typeclass.
  subst LE LF. math.
Qed.

Lemma card_inter_le_l : forall A (E F:set A),
  finite E ->
  card (E \n F) <= card E.
Proof using.
  intros. applys~ card_le_of_incl. set_prove.
Qed.

Lemma card_inter_le_r : forall A (E F:set A),
  finite F ->
  card (E \n F) <= card F.
Proof using.
  intros. rewrite inter_comm. apply~ card_inter_le_l.
Qed.

Lemma card_ge_one : forall A (E:set A) x,
  x \in E ->
  finite E ->
  1 <= card E.
Proof using.
  intros.
  rewrite <- (card_single x).
  applys~ card_le_of_incl.
  set_prove.
Qed.


Lemma card_disjoint_union_single : forall A (E:set A) x,
  finite E ->
  x \notin E ->
  (card (E \u \{x}) = card E + 1)%nat.
Proof using.
  intros.
  replace 1 with (card \{x}) by eauto using card_single.
  applys~ card_disjoint_union. applys finite_single.
  rewrite disjoint_single_r_eq. auto.
Qed.

Lemma card_diff_single : forall A (E:set A) x,
  finite E ->
  x \in E ->
  (card (E \-- x) = card E - 1)%nat.
Proof using.
  intros.
  assert (h1: (E \-- x) \u \{x} = E).
  { rewrite union_comm. erewrite eq_union_single_remove_one by eauto. reflexivity. }
  forwards h2: card_disjoint_union_single (E \-- x) x.
  { eauto with finite. }
  { unfold notin. rewrite set_in_remove_eq.
    rew_logic. right.
    eapply in_single_self. }
  rewrite h1 in h2.
  math.
Qed.

Lemma fold_eq_fold_to_list : forall A B (m:monoid_op B) (f:A->B) (E: set A),
  fold m f E = LibList.fold m f (to_list E).
Proof using. reflexivity. Qed.

Lemma fold_eq_fold_list_repr : forall A B (m:monoid_op B) (f:A->B) (E: set A) L,
  Comm_monoid m ->
  list_repr E L ->
  fold m f E = LibList.fold m f L.
Proof using.
  introv HM EL. rewrite fold_eq_fold_to_list.
  forwards~ (N&EQ2): eq_to_list_inv E. applys* finite_of_list_repr.
  destruct EL as (ND&EQ1).
  applys~ LibList.fold_equiv. intros. rewrite EQ2. rewrite* EQ1.
Qed.

Lemma fold_induction:
  forall A B (m : monoid_op B) (f : A -> B) (P : B -> Prop),
  Comm_monoid m ->
  P (monoid_neutral m) ->
  (forall x a, P x -> P (monoid_oper m (f a) x)) ->
  forall E,
  finite E ->
  P (fold m f E).
Proof using.   introv Hm Hbase Hstep Hfinite.
  assert (forall xs, P (LibList.fold m f xs)).
  { induction xs; unfold LibList.fold; simpl; eauto. }
  forwards: list_repr_to_list_of_finite Hfinite.
  erewrite fold_eq_fold_list_repr by eauto.
  eauto.
Qed.

Lemma fold_congruence : forall A B (m:monoid_op B) (f g:A -> B) (E:set A),
  Comm_monoid m ->
  finite E ->
  (forall x, x \in E -> f x = g x) ->
  fold m f E = fold m g E.
Proof using.   introv Hm HE h. do 2 rewrite fold_eq_fold_to_list.
  eapply LibList.fold_congruence. intros.
  eapply h. rewrite finite_eq_in_iff_mem_to_list in HE. rewrite* HE.
Qed.

Lemma fold_empty : forall A B (m:monoid_op B) (f:A->B),
  fold m f (\{}:set A) = monoid_neutral m.
Proof using.
  intros. rewrite fold_eq_fold_to_list.
  rewrite to_list_empty. rewrite~ LibList.fold_nil.
Qed.

Lemma fold_single : forall A B (m:monoid_op B) (f:A->B) (x:A),
  Monoid m ->
  fold m f \{x} = f x.
Proof using.
  intros. rewrite fold_eq_fold_to_list.
  rewrite to_list_single. rewrite~ fold_cons.
  rewrite fold_nil. rewrite~ monoid_neutral_r.
Qed.

Lemma fold_union : forall A B (m:monoid_op B) (f:A->B) (E F:set A),
  Comm_monoid m ->
  finite E ->
  finite F ->
  E \# F ->
  fold m f (E \u F) = monoid_oper m (fold m f E) (fold m f F).
Proof using.
  introv HM HE HF HD.
  rewrites (>> fold_eq_fold_to_list E).
  rewrites (>> fold_eq_fold_to_list F).
  hint list_repr_to_list_of_finite.
  forwards~ HR: list_repr_disjoint_union HD.
  rewrites~ (>> fold_eq_fold_list_repr HR).
  rewrite~ LibList.fold_app. typeclass.
Qed.

Lemma fold_isolate : forall A (E:set A) x,
  finite E ->
  x \in E ->
  forall B (m : monoid_op B),
  Comm_monoid m ->
  forall (f : A -> B),
  fold m f E = monoid_oper m (f x) (fold m f (E \- \{x})).
Proof using.   intros.
  rewrite (eq_union_single_remove_one E x) at 1 by eauto.
  erewrite <- (fold_single f x) by typeclass.
  eapply fold_union; eauto using remove_disjoint with finite.
Qed.

Hint Rewrite in_set_st_eq : rew_set.

Tactic Notation "rew_set" :=
  autorewrite with rew_set.
Tactic Notation "rew_set" "in" hyp(H) :=
  autorewrite with rew_set in H.
Tactic Notation "rew_set" "in" "*" :=
  autorewrite with rew_set in *.

Section ForeachProp.
Variables (A : Type).
Implicit Types P Q : A -> Prop.
Implicit Types E F : set A.

Lemma foreach_empty : forall P,
  @foreach A (set A) _ P \{}.
Proof using. intros_all. false. Qed.

Lemma foreach_single : forall P X,
  P X ->
  @foreach A (set A) _ P (\{ X }).
Proof using. intros_all. rewrite in_single_eq in H0. subst*. Qed.

Lemma foreach_union : forall P E F,
  foreach P E ->
  foreach P F ->
  foreach P (E \u F).
Proof using. intros_all. destruct~ (in_union_inv H1). Qed.

Lemma foreach_union_inv : forall P E F,
  foreach P (E \u F) ->
  foreach P E /\ foreach P F.
Proof using.
  introv H. split; introv K.
  apply H. rewrite~ @in_union_eq. typeclass.
  apply H. rewrite~ @in_union_eq. typeclass.
Qed.

Lemma foreach_union_eq : forall P E F,
  foreach P (E \u F) = (foreach P E /\ foreach P F).
Proof using.
  intros. extens. iff.
  apply~ foreach_union_inv.
  intuition eauto using foreach_union.
Qed.

Lemma foreach_single_eq : forall P X,
  foreach P (\{X}:set A) = P X.
Proof using.
  intros. extens. iff.
  apply H. apply in_single_self.
  apply~ foreach_single.
Qed.

Lemma foreach_of_pred_incl: forall P Q E,
  foreach P E ->
  pred_incl P Q ->
  foreach Q E.
Proof using. introv H L K. apply~ L. Qed.

Lemma foreach_remove_of_foreach_all : forall P E F,
  foreach P E ->
  foreach P (E \- F).
Proof using. introv M H. applys M. rewrite in_remove_eq in H. autos*. Qed.

Lemma foreach_remove : forall P E F,
  (forall x, x \in E -> x \notin F -> P x) ->
  foreach P (E \- F).
Proof using. introv M Px. rewrite in_remove_eq in Px. applys* M. Qed.

Lemma notin_of_foreach_not : forall P x E,
  foreach P E ->
  ~ P x ->
  x \notin E.
Proof using. introv M N I. applys N. applys~ M. Qed.

End ForeachProp.

Hint Resolve foreach_empty foreach_single foreach_union.
Hint Rewrite foreach_union_eq foreach_single_eq : rew_foreach.

Tactic Notation "rew_foreach" :=
  autorewrite with rew_foreach.
Tactic Notation "rew_foreach" "in" hyp(H) :=
  autorewrite with rew_foreach in H.
Tactic Notation "rew_foreach" "in" "*" :=
  autorewrite_in_star_patch ltac:(fun tt => autorewrite with rew_foreach).
Tactic Notation "rew_foreach" "~" :=
  rew_foreach; auto_tilde.
Tactic Notation "rew_foreach" "*" :=
  rew_foreach; auto_star.
Tactic Notation "rew_foreach" "~" "in" constr(H) :=
  rew_foreach in H; auto_tilde.
Tactic Notation "rew_foreach" "*" "in" constr(H) :=
  rew_foreach in H; auto_star.
Tactic Notation "rew_foreach" "~" "in" "*" :=
  rew_foreach in *; auto_tilde.
Tactic Notation "rew_foreach" "*" "in" "*" :=
  rew_foreach in *; auto_star.