Require Import FSetProperties Zerob Sumbool DecidableTypeEx.

Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E).
Module Import MP := WProperties_fun E M.
Import FM Dec.F.
Import M.

Definition Add := MP.Add.

Section BasicProperties.

Variable s s' s'': t.
Variable x y z : elt.

Lemma mem_eq:
  E.eq x y -> mem x s=mem y s.

Lemma equal_mem_1:
  (forall a, mem a s=mem a s') -> equal s s'=true.

Lemma equal_mem_2:
  equal s s'=true -> forall a, mem a s=mem a s'.

Lemma subset_mem_1:
  (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.

Lemma subset_mem_2:
  subset s s'=true -> forall a, mem a s=true -> mem a s'=true.

Lemma empty_mem: mem x empty=false.

Lemma is_empty_equal_empty: is_empty s = equal s empty.

Lemma choose_mem_1: choose s=Some x -> mem x s=true.

Lemma choose_mem_2: choose s=None -> is_empty s=true.

Lemma add_mem_1: mem x (add x s)=true.

Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.

Lemma remove_mem_1: mem x (remove x s)=false.

Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.

Lemma singleton_equal_add:
  equal (singleton x) (add x empty)=true.

Lemma union_mem:
  mem x (union s s')=mem x s || mem x s'.

Lemma inter_mem:
  mem x (inter s s')=mem x s && mem x s'.

Lemma diff_mem:
  mem x (diff s s')=mem x s && negb (mem x s').

Lemma mem_3 : ~In x s -> mem x s=false.

Lemma mem_4 : mem x s=false -> ~In x s.

Lemma equal_refl: equal s s=true.

Lemma equal_sym: equal s s'=equal s' s.

Lemma equal_trans:
 equal s s'=true -> equal s' s''=true -> equal s s''=true.

Lemma equal_equal:
 equal s s'=true -> equal s s''=equal s' s''.

Lemma equal_cardinal:
 equal s s'=true -> cardinal s=cardinal s'.


Lemma subset_refl: subset s s=true.

Lemma subset_antisym:
 subset s s'=true -> subset s' s=true -> equal s s'=true.

Lemma subset_trans:
 subset s s'=true -> subset s' s''=true -> subset s s''=true.

Lemma subset_equal:
 equal s s'=true -> subset s s'=true.

Lemma choose_mem_3:
 is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.

Lemma choose_mem_4: choose empty=None.

Lemma add_mem_3:
 mem y s=true -> mem y (add x s)=true.

Lemma add_equal:
 mem x s=true -> equal (add x s) s=true.

Lemma remove_mem_3:
 mem y (remove x s)=true -> mem y s=true.

Lemma remove_equal:
 mem x s=false -> equal (remove x s) s=true.

Lemma add_remove:
 mem x s=true -> equal (add x (remove x s)) s=true.

Lemma remove_add:
 mem x s=false -> equal (remove x (add x s)) s=true.

Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).

Lemma singleton_mem_1: mem x (singleton x)=true.

Lemma singleton_mem_2: ~E.eq x y -> mem y (singleton x)=false.

Lemma singleton_mem_3: mem y (singleton x)=true -> E.eq x y.

Lemma union_sym:
 equal (union s s') (union s' s)=true.

Lemma union_subset_equal:
 subset s s'=true -> equal (union s s') s'=true.

Lemma union_equal_1:
 equal s s'=true-> equal (union s s'') (union s' s'')=true.

Lemma union_equal_2:
 equal s' s''=true-> equal (union s s') (union s s'')=true.

Lemma union_assoc:
 equal (union (union s s') s'') (union s (union s' s''))=true.

Lemma add_union_singleton:
 equal (add x s) (union (singleton x) s)=true.

Lemma union_add:
 equal (union (add x s) s') (add x (union s s'))=true.


Lemma union_subset_1: subset s (union s s')=true.

Lemma union_subset_2: subset s' (union s s')=true.

Lemma union_subset_3:
 subset s s''=true -> subset s' s''=true ->
  subset (union s s') s''=true.

Lemma inter_sym: equal (inter s s') (inter s' s)=true.

Lemma inter_subset_equal:
 subset s s'=true -> equal (inter s s') s=true.

Lemma inter_equal_1:
 equal s s'=true -> equal (inter s s'') (inter s' s'')=true.

Lemma inter_equal_2:
 equal s' s''=true -> equal (inter s s') (inter s s'')=true.

Lemma inter_assoc:
 equal (inter (inter s s') s'') (inter s (inter s' s''))=true.

Lemma union_inter_1:
 equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.

Lemma union_inter_2:
 equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.

Lemma inter_add_1: mem x s'=true ->
 equal (inter (add x s) s') (add x (inter s s'))=true.

Lemma inter_add_2: mem x s'=false ->
 equal (inter (add x s) s') (inter s s')=true.


Lemma inter_subset_1: subset (inter s s') s=true.

Lemma inter_subset_2: subset (inter s s') s'=true.

Lemma inter_subset_3:
 subset s'' s=true -> subset s'' s'=true ->
  subset s'' (inter s s')=true.

Lemma diff_subset: subset (diff s s') s=true.

Lemma diff_subset_equal:
 subset s s'=true -> equal (diff s s') empty=true.

Lemma remove_inter_singleton:
 equal (remove x s) (diff s (singleton x))=true.

Lemma diff_inter_empty:
 equal (inter (diff s s') (inter s s')) empty=true.

Lemma diff_inter_all:
 equal (union (diff s s') (inter s s')) s=true.

End BasicProperties.

#[global]
Hint Immediate empty_mem is_empty_equal_empty add_mem_1
   remove_mem_1 singleton_equal_add union_mem inter_mem
   diff_mem equal_sym add_remove remove_add : set.
#[global]
Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
   choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
   subset_refl subset_equal subset_antisym
   add_mem_3 add_equal remove_mem_3 remove_equal : set.

Lemma set_rec: forall (P:t->Type),
 (forall s s', equal s s'=true -> P s -> P s') ->
 (forall s x, mem x s=false -> P s -> P (add x s)) ->
 P empty -> forall s, P s.

Lemma exclusive_set : forall s s' x,
 ~(In x s/\In x s') <-> mem x s && mem x s'=false.

Section Fold.
Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
Variables (i:A).
Variables (s s':t)(x:elt).

Lemma fold_empty: (fold f empty i) = i.

Lemma fold_equal:
 equal s s'=true -> eqA (fold f s i) (fold f s' i).

Lemma fold_add:
 mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).

Lemma add_fold:
  mem x s=true -> eqA (fold f (add x s) i) (fold f s i).

Lemma remove_fold_1:
 mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).

Lemma remove_fold_2:
 mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).

Lemma fold_union:
 (forall x, mem x s && mem x s'=false) ->
 eqA (fold f (union s s') i) (fold f s (fold f s' i)).

End Fold.

Lemma add_cardinal_1:
 forall s x, mem x s=true -> cardinal (add x s)=cardinal s.

Lemma add_cardinal_2:
 forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).

Lemma remove_cardinal_1:
 forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.

Lemma remove_cardinal_2:
 forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.

Lemma union_cardinal:
 forall s s', (forall x, mem x s && mem x s'=false) ->
 cardinal (union s s')=cardinal s+cardinal s'.

Lemma subset_cardinal:
 forall s s', subset s s'=true -> cardinal s<=cardinal s'.

Section Bool.

Variable f:elt->bool.
Variable Comp: Proper (E.eq==>Logic.eq) f.

Local Definition Comp' : Proper (E.eq==>Logic.eq) (fun x =>negb (f x)).

Local Hint Resolve Comp' : core.
Local Hint Unfold compat_bool : core.

Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.

Lemma for_all_filter:
 forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).

Lemma exists_filter :
 forall s, exists_ f s=negb (is_empty (filter f s)).

Lemma partition_filter_1:
 forall s, equal (fst (partition f s)) (filter f s)=true.

Lemma partition_filter_2:
 forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.

Lemma filter_add_1 : forall s x, f x = true ->
 filter f (add x s) [=] add x (filter f s).

Lemma filter_add_2 : forall s x, f x = false ->
 filter f (add x s) [=] filter f s.

Lemma add_filter_1 : forall s s' x,
 f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).

Lemma add_filter_2 : forall s s' x,
 f x=false -> (Add x s s') -> filter f s [=] filter f s'.

Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
  forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s.

Lemma filter_union: forall s s', filter f (union s s') [=] union (filter f s) (filter f s').

Lemma for_all_mem_1: forall s,
 (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.

Lemma for_all_mem_2: forall s,
 (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true.

Lemma for_all_mem_3:
 forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.

Lemma for_all_mem_4:
 forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.

Lemma for_all_exists:
 forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).

End Bool.
Section Bool'.

Variable f:elt->bool.
Variable Comp: compat_bool E.eq f.

Hint Resolve Comp' : core.

Lemma exists_mem_1:
 forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.

Lemma exists_mem_2:
 forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false.

Lemma exists_mem_3:
 forall s x, mem x s=true -> f x=true -> exists_ f s=true.

Lemma exists_mem_4:
 forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.

End Bool'.

Section Sum.

Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0.
Notation compat_opL := (compat_op E.eq Logic.eq).
Notation transposeL := (transpose Logic.eq).

Lemma sum_plus :
  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
    forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.

Lemma sum_filter : forall f, (compat_bool E.eq f) ->
  forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).

Lemma fold_compat :
  forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
  (f g:elt->A->A),
  (compat_op E.eq eqA f) -> (transpose eqA f) ->
  (compat_op E.eq eqA g) -> (transpose eqA g) ->
  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) ->
  (eqA (fold f s i) (fold g s i)).

Lemma sum_compat :
  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
  forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.

End Sum.

End WEqProperties_fun.

Module WEqProperties (M:WS) := WEqProperties_fun M.E M.
Module EqProperties := WEqProperties.