Subset.v

intros H; split; subset_unfold; intros x Hx1; specialize (H x); intuition.
intros [_ H] x Hx1 Hx2; specialize (H x Hx1); now destruct H as [_ H].
Qed.

Lemma disj_diff_r :
  forall (A B C : U -> Prop),
    disj A B -> disj (diff A C) (diff B C).
Proof.
intros A B C H x HAx HBx; apply (H x); now apply (diff_lb_l _ C).
Qed.

Lemma diff_empty :
  forall (A B : U -> Prop),
    diff A B = emptyset <-> incl A B.
Proof.
intros; rewrite <- empty_emptyset; split; intros H.
intros x Hx1; apply NNPP; intros Hx2; now apply (H x).
intros x [Hx1 Hx2]; auto.
Qed.

Lemma diff_empty_diag :
  forall (A : U -> Prop),
    diff A A = emptyset.
Proof.
intros; now rewrite diff_empty.
Qed.

Lemma full_diff :
  forall (A B : U -> Prop),
    diff A B = fullset <-> A = fullset /\ B = emptyset.
Proof.
intros; do 2 rewrite <- full_fullset; rewrite <- empty_emptyset.
split; intros H.
split; intros x; now destruct (H x) as [H1 H2].
intros x; destruct H as [H1 H2]; split; [apply H1 | exact (H2 x)].
Qed.

Lemma compl_diff :
  forall (A B : U -> Prop),
    compl (diff A B) = union (compl A) B.
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma diff_empty_l :
  forall (A : U -> Prop),
    diff emptyset A = emptyset.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_empty_r :
  forall (A : U -> Prop),
    diff A emptyset = A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_full_l:
  forall (A : U -> Prop),
    diff fullset A = compl A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_full_r:
  forall (A : U -> Prop),
    diff A fullset = emptyset.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_compl_l :
  forall (A B : U -> Prop),
    diff (compl A) B = diff (compl B) A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_compl_r :
  forall (A B : U -> Prop),
    diff A (compl B) = diff B (compl A).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma diff_compl :
  forall (A B : U -> Prop),
    diff (compl A) (compl B) = diff B A.
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma diff_union_l :
  forall (A B C : U -> Prop),
    diff (union A B) C = union (diff A C) (diff B C).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_union_r :
  forall (A B C : U -> Prop),
    diff A (union B C) = inter (diff A B) (diff A C).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_inter_l :
  forall (A B C : U -> Prop),
    diff (inter A B) C = inter (diff A C) (diff B C).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_inter_r :
  forall (A B C : U -> Prop),
    diff A (inter B C) = union (diff A B) (diff A C).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma diff_union_l_diag :
  forall (A B : U -> Prop),
    diff (union A B) A = diff B A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_union_r_diag :
  forall (A B : U -> Prop),
    diff (union A B) B = diff A B.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_inter_l_diag :
  forall (A B : U -> Prop),
    diff A (inter A B) = diff A B.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_inter_r_diag :
  forall (A B : U -> Prop),
    diff B (inter A B) = diff B A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma union_diff_l :
  forall (A B C : U -> Prop),
    union (diff A B) C = diff (union A C) (diff B C).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma union_diff_r :
  forall (A B C : U -> Prop),
    union A (diff B C) = diff (union A B) (diff C A).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma distrib_inter_diff_l :
  forall (A B C : U -> Prop),
    inter A (diff B C) = diff (inter A B) (inter A C).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma distrib_inter_diff_r :
  forall (A B C : U -> Prop),
    inter (diff A B) C = diff (inter A C) (inter B C).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff2_l :
  forall (A B C : U -> Prop),
    diff (diff A B) C = diff A (union B C).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff2_r :
  forall (A B C : U -> Prop),
    diff A (diff B C) = union (inter A C) (diff A B).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma diff2_r_inter :
  forall (A B C : U -> Prop),
    incl A B ->
    diff A (diff B C) = inter A C.
Proof.
intros A B C H; apply diff_empty in H.
rewrite diff2_r, H; apply union_empty_r.
Qed.

Lemma diff2 :
  forall (A B C D : U -> Prop),
    diff (diff A B) (diff C D) =
      union (diff (inter A (compl C)) B)
            (diff (inter A D) B).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma diff2_diag_l :
  forall (A B C : U -> Prop),
    diff (diff A B) (diff A C) = diff (inter A C) B.
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma diff2_cancel_left :
  forall (A B C : U -> Prop),
    incl A B ->
    diff (diff B C) (diff B A) = diff A C.
Proof.
intros; now rewrite diff2_diag_l, inter_comm, (proj1 (inter_left _ _)).
Qed.

Lemma diff2_diag_r :
  forall (A B C : U -> Prop),
    diff (diff A C) (diff B C) = diff (inter A (compl B)) C.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

End Diff_Facts.


Section Sym_diff_Facts.

(** Facts about symmetric difference. *)

Context {U : Type}. (* Universe. *)

Lemma sym_diff_equiv_def_union :
  forall (A B : U -> Prop),
    sym_diff A B = union (diff A B) (diff B A).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma sym_diff_equiv_def_diff :
  forall (A B : U -> Prop),
    sym_diff A B = diff (union A B) (inter A B).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma union_equiv_def_sym_diff :
  forall (A B : U -> Prop),
    union A B = sym_diff (sym_diff A B) (inter A B).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma inter_equiv_def_sym_diff :
  forall (A B : U -> Prop),
    inter A B = diff (union A B) (sym_diff A B).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma diff_equiv_def_sym_diff_inter :
  forall (A B : U -> Prop),
    diff A B = sym_diff A (inter A B).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma diff_equiv_def_sym_diff_union :
  forall (A B : U -> Prop),
    diff A B = sym_diff (union A B) B.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

(* ((U -> Prop) -> Prop, sym_diff) is a Boolean group,
  ie an abelian group with the emptyset as neutral, and inv = id. *)

Lemma sym_diff_assoc :
  forall (A B C : U -> Prop),
    sym_diff (sym_diff A B) C = sym_diff A (sym_diff B C).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma sym_diff_comm :
  forall (A B : U -> Prop),
    sym_diff A B = sym_diff B A.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma sym_diff_inv :
  forall (A : U -> Prop),
    sym_diff A A = emptyset.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma sym_diff_empty_l :
  forall (A : U -> Prop),
    sym_diff emptyset A = A.
Proof.
intros; rewrite sym_diff_equiv_def_union, diff_empty_l, diff_empty_r.
apply union_empty_l.
Qed.

Lemma sym_diff_empty_r :
  forall (A : U -> Prop),
    sym_diff A emptyset = A.
Proof.
intros; rewrite sym_diff_comm; apply sym_diff_empty_l.
Qed.

Lemma sym_diff_full_l :
  forall (A : U -> Prop),
    sym_diff fullset A = compl A.
Proof.
intros; rewrite sym_diff_equiv_def_diff, union_full_l, inter_full_l.
symmetry; apply compl_equiv_def_diff.
Qed.

Lemma sym_diff_full_r :
  forall (A : U -> Prop),
    sym_diff A fullset = compl A.
Proof.
intros; rewrite sym_diff_comm; apply sym_diff_full_l.
Qed.

Lemma sym_diff_eq_reg_l :
  forall (A B C : U -> Prop),
    sym_diff A B = sym_diff A C -> B = C.
Proof.
intros A B C H.
rewrite <- (sym_diff_empty_l B), <- (sym_diff_empty_l C), <- (sym_diff_inv A).
do 2 rewrite sym_diff_assoc.
now f_equal.
Qed.

Lemma sym_diff_eq_reg_r :
  forall (A B C : U -> Prop),
    sym_diff A B = sym_diff C B -> A = C.
Proof.
intros A B C H; apply sym_diff_eq_reg_l with B.
now rewrite (sym_diff_comm _ A), (sym_diff_comm _ C).
Qed.

Lemma sym_diff_compl_l :
  forall (A : U -> Prop),
    sym_diff (compl A) A = fullset.
Proof.
intros; rewrite <- sym_diff_full_l, sym_diff_assoc, sym_diff_inv.
apply sym_diff_empty_r.
Qed.

Lemma sym_diff_compl_r :
  forall (A : U -> Prop),
    sym_diff A (compl A) = fullset.
Proof.
intros; rewrite sym_diff_comm; apply sym_diff_compl_l.
Qed.

Lemma sym_diff_compl :
  forall (A B : U -> Prop),
    sym_diff (compl A) (compl B) = sym_diff A B.
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma super_distrib_union_sym_diff_l :
  forall (A B C : U -> Prop),
    incl (sym_diff (union A C) (union B C))
         (union (sym_diff A B) C).
Proof.
intros; subset_auto.
Qed.

Lemma super_distrib_union_sym_diff_r :
  forall (A B C : U -> Prop),
    incl (sym_diff (union A B) (union A C))
         (union A (sym_diff B C)).
Proof.
intros; subset_auto.
Qed.

Lemma super_distrib_union_sym_diff :
  forall (A B C D : U -> Prop),
    incl (sym_diff (union A C) (union B D))
         (union (sym_diff A B) (sym_diff C D)).
Proof.
intros; subset_auto.
Qed.

Lemma sub_distrib_sym_diff_union_l :
  forall (A B C : U -> Prop),
    incl (sym_diff (union A B) C)
         (union (sym_diff A C) (sym_diff B C)).
Proof.
intros; subset_auto.
Qed.

Lemma sub_distrib_sym_diff_union_r :
  forall (A B C : U -> Prop),
    incl (sym_diff A (union B C))
         (union (sym_diff A B) (sym_diff A C)).
Proof.
intros; subset_auto.
Qed.

Lemma sub_distrib_sym_diff_union :
  forall (A B C D : U -> Prop),
    incl (sym_diff (union A B) (union C D))
         (union (sym_diff A C) (sym_diff B D)).
Proof.
intros; subset_auto.
Qed.

(* ((U -> Prop) -> Prop, sym_diff, inter) is a Boolean ring,
  ie an abelian ring with fullset as neutral for intersection. *)

Lemma distrib_inter_sym_diff_l :
  forall (A B C : U -> Prop),
    inter (sym_diff A B) C = sym_diff (inter A C) (inter B C).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma distrib_inter_sym_diff_r :
  forall (A B C : U -> Prop),
    inter A (sym_diff B C) = sym_diff (inter A B) (inter A C).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma distrib_inter_sym_diff :
  forall (A B C D : U -> Prop),
    inter (sym_diff A B) (sym_diff C D) =
    sym_diff (sym_diff (inter A C) (inter A D))
             (sym_diff (inter B C) (inter B D)).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma super_distrib_sym_diff_inter_l :
  forall (A B C : U -> Prop),
    incl (inter (sym_diff A C) (sym_diff B C))
         (sym_diff (inter A B) C).
Proof.
intros; subset_auto.
Qed.

Lemma super_distrib_sym_diff_inter_r :
  forall (A B C : U -> Prop),
    incl (inter (sym_diff A B) (sym_diff A C))
         (sym_diff A (inter B C)).
Proof.
intros; subset_auto.
Qed.

Lemma super_distrib_sym_diff_inter :
  forall (A B C D : U -> Prop),
    incl (inter (inter (sym_diff A C) (sym_diff A D))
                (inter (sym_diff B C) (sym_diff B D)))
         (sym_diff (inter A B) (inter C D)).
Proof.
intros; subset_auto.
Qed.

(* ((U -> Prop) -> Prop, sym_diff, inter) is a Boolean algebra. *)

Lemma sym_diff_union :
  forall (A B : U -> Prop),
    sym_diff A B = union A B <-> disj A B.
Proof.
intros; rewrite sym_diff_equiv_def_diff, <- disj_diff, (disj_sym (union _ _)).
apply disj_inter_union.
Qed.

Lemma disj_sym_diff_inter :
  forall (A B : U -> Prop),
    disj (sym_diff A B) (inter A B).
Proof.
intros; subset_auto.
Qed.

Lemma union_sym_diff_inter :
  forall (A B : U -> Prop),
    union (sym_diff A B) (inter A B) = union A B.
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma partition_sym_diff_inter :
  forall (A B : U -> Prop),
    partition (union A B) (sym_diff A B) (inter A B).
Proof.
intros; split.
symmetry; apply union_sym_diff_inter.
apply disj_sym_diff_inter.
Qed.

Lemma sym_diff_cancel_middle :
  forall (A B C : U -> Prop),
    sym_diff (sym_diff A B) (sym_diff B C) = sym_diff A C.
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma sym_diff2 :
  forall (A B C D : U -> Prop),
    sym_diff (sym_diff A B) (sym_diff C D) =
      sym_diff A (sym_diff B (sym_diff C D)).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma sym_diff_triangle_ineq :
  forall (A B C : U -> Prop),
    incl (sym_diff A C) (union (sym_diff A B) (sym_diff B C)).
Proof.
intros; intros x; subset_auto.
Qed.

Lemma sym_diff_diff_diag_l :
  forall (A B C : U -> Prop),
    incl (union B C) A ->
    sym_diff (diff A B) (diff A C) = sym_diff B C.
Proof.
intros A B C H; apply incl_union in H.
rewrite sym_diff_equiv_def_union.
repeat rewrite diff2_cancel_left; try easy.
now rewrite <- sym_diff_equiv_def_union, sym_diff_comm.
Qed.

End Sym_diff_Facts.


Section Partition_Facts.

(** Facts about partition. *)

Context {U : Type}. (* Universe. *)

Lemma partition_sym :
  forall (A B C : U -> Prop),
    partition A B C -> partition A C B.
Proof.
intros A B C; unfold partition.
now rewrite union_comm, disj_sym.
Qed.

Lemma partition_inter_l :
  forall (A B C D : U -> Prop),
    partition A B C -> partition (inter D A) (inter D B) (inter D C).
Proof.
intros A B C D [H1 H2]; split.
rewrite H1; apply distrib_inter_union_l.
now apply disj_inter_l.
Qed.

Lemma partition_inter_r :
  forall (A B C D : U -> Prop),
    partition A B C -> partition (inter A D) (inter B D) (inter C D).
Proof.
intros A B C D.
rewrite (inter_comm A), (inter_comm B), (inter_comm C).
apply partition_inter_l.
Qed.

Lemma partition_diff :
  forall (A B C D : U -> Prop),
    partition A B C -> partition (diff A D) (diff B D) (diff C D).
Proof.
intros; now apply partition_inter_r.
Qed.

End Partition_Facts.


Section Prod_Facts.

(** Facts about Cartesian product. *)

Context {U1 U2 : Type}. (* Universes. *)

Lemma inhabited_prod :
  inhabited U1 -> inhabited U2 -> inhabited (U1 * U2).
Proof.
intros [x1] [x2]; apply (inhabits (x1, x2)).
Qed.

Lemma prod_emptyset_l :
  forall A2, prod emptyset A2 = @emptyset (U1 * U2).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma prod_emptyset_r :
  forall A1, prod A1 emptyset = @emptyset (U1 * U2).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma prod_fullset :
  prod fullset fullset = @fullset (U1 * U2).
Proof.
apply subset_ext; subset_auto.
Qed.

Lemma prod_fullset_l :
  forall A2, prod fullset A2 = fun x : U1 * U2 => A2 (snd x).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma prod_fullset_r :
  forall A1, prod A1 fullset = fun x : U1 * U2 => A1 (fst x).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma prod_inter :
  forall (A1 B1 : U1 -> Prop) (A2 B2 : U2 -> Prop),
    inter (prod A1 A2) (prod B1 B2) = prod (inter A1 B1) (inter A2 B2).
Proof.
intros; apply subset_ext; subset_auto.
Qed.

Lemma prod_compl_union :
  forall (A1 : U1 -> Prop) (A2 : U2 -> Prop),
    compl (prod A1 A2) = union (prod (compl A1) A2) (prod fullset (compl A2)).
Proof.
intros; apply subset_ext; intros x; subset_auto.
Qed.

Lemma prod_compl_disj :
  forall (A1 : U1 -> Prop) (A2 : U2 -> Prop),
    disj (prod (compl A1) A2) (prod fullset (compl A2)).
Proof.
subset_auto.
Qed.

Lemma prod_compl_partition :
  forall (A1 : U1 -> Prop) (A2 : U2 -> Prop),
    partition (compl (prod A1 A2))
      (prod (compl A1) A2) (prod fullset (compl A2)).
Proof.
intros; split.
apply prod_compl_union.
apply prod_compl_disj.
Qed.

Lemma prod_swap :
  forall (A1 : U1 -> Prop) (A2 : U2 -> Prop),
    (fun x21 : U2 * U1 => prod A1 A2 (swap (fun x : U1 * U2 => x) x21)) = prod A2 A1.
Proof.
intros; apply subset_ext; subset_auto.
Qed.

End Prod_Facts.