Subset_system.v

(**
This file is part of the Elfic library

Copyright (C) Boldo, Clément, Faissole, Martin, Mayero

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(* TODO:
  1. use Ensembles / Powerset formalism?
     Naah, rather use Subset instead.
  2. use setoids?
  3. Type classes or canonical structures might help in inheriting properties
     of simpler subset systems, e.g. Psyst -> Ring -> Algebra -> Sigma_algebra. *)

Require Import nat_compl.
Require Import Subset Subset_finite Subset_seq.
Require Import Subset_system_base Subset_system_gen.


Section Subset_systems_Def1.

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

Variable gen : (U -> Prop) -> Prop. (* Generator. *)
Variable A0 : U -> Prop. (* Witness (for pi systems). *)

(* Psyst is the pi-system generated by gen,
 ie the smallest pi-system containing gen. *)
Inductive Psyst : (U -> Prop) -> Prop :=   (* Unfortunately, Pi was not a good ident… *)
  | Psyst_Gen : Incl gen Psyst
  | Psyst_Mem : Psyst A0
  | Psyst_Inter : Inter Psyst.

(* Ring is the ring (of sets) generated by gen,
 ie the smallest ring containing gen. *)
Inductive Ring : (U -> Prop) -> Prop :=
  | Ring_Gen : Incl gen Ring
  | Ring_wEmpty : wEmpty Ring
  | Ring_Diff : Diff Ring
  | Ring_Union : Union Ring.

(* Algebra is the (set) algebra generated by gen,
 ie the smallest algebra containing gen. *)
Inductive Algebra : (U -> Prop) -> Prop :=
  | Algebra_Gen : Incl gen Algebra
  | Algebra_wEmpty : wEmpty Algebra
  | Algebra_Compl : Compl Algebra
  | Algebra_Union : Union Algebra.

(* Monotone_class is the monotone class generated by gen,
 ie the smallest monotone class containing gen. *)
Inductive Monotone_class : (U -> Prop) -> Prop :=
  | Monotone_class_Gen : Incl gen Monotone_class
  | Monotone_class_Inter_monot_seq : Inter_monot_seq Monotone_class
  | Monotone_class_Union_monot_seq : Union_monot_seq Monotone_class.

(* Lsyst is the lambda-system generated by gen,
 ie the smallest lambda-system containing gen. *)
Inductive Lsyst : (U -> Prop) -> Prop :=   (* Lambda was an even worse ident! *)
  | Lsyst_Gen : Incl gen Lsyst
  | Lsyst_wFull : wFull Lsyst
  | Lsyst_Compl : Compl Lsyst
  | Lsyst_Union_disj_seq : Union_disj_seq Lsyst.

(* Sigma_ring is the sigma-ring generated by gen,
 ie the smallest sigma-ring containing gen. *)
Inductive Sigma_ring : (U -> Prop) -> Prop :=
  | Sigma_ring_Gen : Incl gen Sigma_ring
  | Sigma_ring_wEmpty : wEmpty Sigma_ring
  | Sigma_ring_Diff : Diff Sigma_ring
  | Sigma_ring_Union_seq : Union_seq Sigma_ring.

(* Sigma_algebra is the sigma-algebra generated by gen,
 ie the smallest sigma-algebra containing gen. *)
Inductive Sigma_algebra : (U -> Prop) -> Prop :=
  | Sigma_algebra_Gen : Incl gen Sigma_algebra
  | Sigma_algebra_wEmpty : wEmpty Sigma_algebra
  | Sigma_algebra_Compl : Compl Sigma_algebra
  | Sigma_algebra_Union_seq : Union_seq Sigma_algebra.

(*
(* Open is a collection of open subsets of U. *)
Inductive Open : (U -> Prop) -> Prop :=
  | Open_wEmpty : wEmpty Open
  | Open_wFull : wFull Open
  | Open_Inter_finite : Inter_finite Open
  | Open_Union_any : forall {Idx : Type}, @Union_any Idx U Open.

(* Close is a collection of closed subsets of U. *)
Inductive Close : (U -> Prop) -> Prop :=
  | Close_wEmpty : wEmpty Close
  | Close_wFull : wFull Close
  | Close_Union_finite : Union_finite Close
  | Close_Inter_any : forall {Idx : Type}, @Inter_any Idx U Close.
*)

End Subset_systems_Def1.


Section Subset_systems_Def2.

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

Variable P : (U -> Prop) -> Prop. (* Subset system. *)
Variable A0 : U -> Prop. (* Witness. *)

Definition is_Psyst : Prop := Psyst P A0 = P.

Definition is_Semi_ring : Prop :=
  wEmpty P /\ Inter P /\ Part_diff_finite P.

Definition is_Ring : Prop := Ring P = P.

Definition is_Semi_algebra : Prop :=
  wFull P /\ Inter P /\ Part_compl_finite P.

Definition is_Algebra : Prop := Algebra P = P.

Definition is_Monotone_class : Prop := Monotone_class P = P.

Definition is_Lsyst : Prop := Lsyst P = P.

Definition is_Sigma_ring : Prop := Sigma_ring P = P.

Definition is_Sigma_algebra : Prop := Sigma_algebra P = P.

End Subset_systems_Def2.


Hint Constructors Psyst : subset_systems.
Hint Unfold is_Semi_ring : subset_systems.
Hint Constructors Ring : subset_systems.
Hint Unfold is_Semi_algebra : subset_systems.
Hint Constructors Algebra : subset_systems.
Hint Constructors Monotone_class : subset_systems.
Hint Constructors Lsyst : subset_systems.
Hint Constructors Sigma_ring : subset_systems.
Hint Constructors Sigma_algebra : subset_systems.
(*Print HintDb subset_systems.*)


Section Subset_systems_Facts1.

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

Variable P : (U -> Prop) -> Prop. (* Subset system. *)

Lemma Psyst_equiv :
  forall (A0 : U -> Prop),
    is_Psyst P A0 <-> P A0 /\ Inter P.
Proof.
split.
(* *)
intros H; rewrite <- H; auto with subset_systems.
(* *)
intros [H1 H2]; apply Ext; split.
intros H3; induction H3; try easy.
now apply H2.
apply Psyst_Gen.
Qed.

Lemma Ring_equiv :
  is_Ring P <-> wEmpty P /\ Diff P /\ Union P.
Proof.
split.
(* *)
intros H; rewrite <- H; auto with subset_systems.
(* *)
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Ring_Gen.
Qed.

Lemma Algebra_equiv :
  is_Algebra P <-> wEmpty P /\ Compl P /\ Union P.
Proof.
split.
(* *)
intros H; rewrite <- H; auto with subset_systems.
(* *)
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Algebra_Gen.
Qed.

Lemma Monotone_class_equiv :
  is_Monotone_class P <-> Inter_monot_seq P /\ Union_monot_seq P.
Proof.
split.
(* *)
intros H; split; rewrite <- H.
apply Monotone_class_Inter_monot_seq.
apply Monotone_class_Union_monot_seq.
(* *)
intros [H1 H2]; apply Ext; split.
intros H3; induction H3; try easy; [now apply H1 | now apply H2].
apply Monotone_class_Gen.
Qed.

Lemma Lsyst_equiv :
  is_Lsyst P <-> wFull P /\ Compl P /\ Union_disj_seq P.
Proof.
split.
(* *)
intros H; repeat split; rewrite <- H.
apply Lsyst_wFull.
apply Lsyst_Compl.
apply Lsyst_Union_disj_seq.
(* *)
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Lsyst_Gen.
Qed.

Lemma Sigma_ring_equiv :
  is_Sigma_ring P <-> wEmpty P /\ Diff P /\ Union_seq P.
Proof.
split.
(* *)
intros H; repeat split; rewrite <- H.
apply Sigma_ring_wEmpty.
apply Sigma_ring_Diff.
apply Sigma_ring_Union_seq.
(* *)
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy.
now apply H2.
now apply H3.
apply Sigma_ring_Gen.
Qed.

Lemma Sigma_algebra_equiv :
  is_Sigma_algebra P <-> wEmpty P /\ Compl P /\ Union_seq P.
Proof.
split.
(* *)
intros H; repeat split; rewrite <- H.
apply Sigma_algebra_wEmpty.
apply Sigma_algebra_Compl.
apply Sigma_algebra_Union_seq.
(* *)
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Sigma_algebra_Gen.
Qed.

End Subset_systems_Facts1.


Section Subset_systems_Facts2.

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

Variable gen0 gen1 : (U -> Prop) -> Prop. (* Generators. *)
Variable A0 : U -> Prop. (* Witness. *)

Lemma Psyst_lub_alt :
  Incl gen0 (Psyst gen1 A0) ->
  Incl (Psyst gen0 A0) (Psyst gen1 A0).
Proof.
intros H A HA; induction HA.
now apply H.
apply Psyst_Mem.
now apply Psyst_Inter.
Qed.

Lemma Ring_lub_alt :
  Incl gen0 (Ring gen1) ->
  Incl (Ring gen0) (Ring gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Ring_wEmpty.
now apply Ring_Diff.
now apply Ring_Union.
Qed.

Lemma Algebra_lub_alt :
  Incl gen0 (Algebra gen1) ->
  Incl (Algebra gen0) (Algebra gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Algebra_wEmpty.
now apply Algebra_Compl.
now apply Algebra_Union.
Qed.

Lemma Monotone_class_lub_alt :
  Incl gen0 (Monotone_class gen1) ->
  Incl (Monotone_class gen0) (Monotone_class gen1).
Proof.
intros H A HA; induction HA.
now apply H.
now apply Monotone_class_Inter_monot_seq.
now apply Monotone_class_Union_monot_seq.
Qed.

Lemma Lsyst_lub_alt :
  Incl gen0 (Lsyst gen1) ->
  Incl (Lsyst gen0) (Lsyst gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Lsyst_wFull.
now apply Lsyst_Compl.
now apply Lsyst_Union_disj_seq.
Qed.

Lemma Sigma_ring_lub_alt :
  Incl gen0 (Sigma_ring gen1) ->
  Incl (Sigma_ring gen0) (Sigma_ring gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Sigma_ring_wEmpty.
now apply Sigma_ring_Diff.
now apply Sigma_ring_Union_seq.
Qed.

Lemma Sigma_algebra_lub_alt :
  Incl gen0 (Sigma_algebra gen1) ->
  Incl (Sigma_algebra gen0) (Sigma_algebra gen1).
Proof.
intros H A HA; induction HA.
now apply H.
apply Sigma_algebra_wEmpty.
now apply Sigma_algebra_Compl.
now apply Sigma_algebra_Union_seq.
Qed.

End Subset_systems_Facts2.


Section Subset_systems_Facts3.

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

Variable P : (U -> Prop) -> Prop. (* Subset system. *)
Variable gen : (U -> Prop) -> Prop. (* Generator. *)
Variable A0 : U -> Prop. (* Witness. *)

Lemma Psyst_lub :
  is_Psyst P A0 -> Incl gen P -> Incl (Psyst gen A0) P.
Proof.
intros H; rewrite <- H; apply Psyst_lub_alt.
Qed.

Lemma Ring_lub :
  is_Ring P -> Incl gen P -> Incl (Ring gen) P.
Proof.
intros H; rewrite <- H; apply Ring_lub_alt.
Qed.

Lemma Algebra_lub :
  is_Algebra P -> Incl gen P -> Incl (Algebra gen) P.
Proof.
intros H; rewrite <- H; apply Algebra_lub_alt.
Qed.

Lemma Monotone_class_lub :
  is_Monotone_class P -> Incl gen P -> Incl (Monotone_class gen) P.
Proof.
intros H; rewrite <- H; apply Monotone_class_lub_alt.
Qed.

Lemma Lsyst_lub :
  is_Lsyst P -> Incl gen P -> Incl (Lsyst gen) P.
Proof.
intros H; rewrite <- H; apply Lsyst_lub_alt.
Qed.

Lemma Sigma_ring_lub :
  is_Sigma_ring P -> Incl gen P -> Incl (Sigma_ring gen) P.
Proof.
intros H; rewrite <- H; apply Sigma_ring_lub_alt.
Qed.

Lemma Sigma_algebra_lub :
  is_Sigma_algebra P -> Incl gen P -> Incl (Sigma_algebra gen) P.
Proof.
intros H; rewrite <- H; apply Sigma_algebra_lub_alt.
Qed.

End Subset_systems_Facts3.


Section Subset_systems_Facts4.

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

Variable gen : (U -> Prop) -> Prop. (* Generator. *)
Variable A0 : U -> Prop. (* Witness. *)

Lemma Psyst_idem :
  is_Psyst (Psyst gen A0) A0.
Proof.
apply Ext_equiv; split; [now apply Psyst_lub_alt | apply Psyst_Gen].
Qed.

Lemma Ring_idem :
  is_Ring (Ring gen).
Proof.
apply Ext_equiv; split; [now apply Ring_lub_alt | apply Ring_Gen].
Qed.

Lemma Algebra_idem :
  is_Algebra (Algebra gen).
Proof.
apply Ext_equiv; split; [now apply Algebra_lub_alt | apply Algebra_Gen].
Qed.

Lemma Monotone_class_idem :
  is_Monotone_class (Monotone_class gen).
Proof.
apply Ext_equiv; split; [now apply Monotone_class_lub_alt | apply Monotone_class_Gen].
Qed.

Lemma Lsyst_idem :
  is_Lsyst (Lsyst gen).
Proof.
apply Ext_equiv; split; [now apply Lsyst_lub_alt | apply Lsyst_Gen].
Qed.

Lemma Sigma_ring_idem :
  is_Sigma_ring (Sigma_ring gen).
Proof.
apply Ext_equiv; split; [now apply Sigma_ring_lub_alt | apply Sigma_ring_Gen].
Qed.

Lemma Sigma_algebra_idem :
  is_Sigma_algebra (Sigma_algebra gen).
Proof.
apply Ext_equiv; split; [now apply Sigma_algebra_lub_alt | apply Sigma_algebra_Gen].
Qed.

Variable gen0 gen1 : (U -> Prop) -> Prop. (* Generators. *)

Lemma Psyst_monot :
  Incl gen0 gen1 -> Incl (Psyst gen0 A0) (Psyst gen1 A0).
Proof.
intros; apply Psyst_lub_alt, Incl_trans with gen1; [easy | apply Psyst_Gen].
Qed.

Lemma Ring_monot :
  Incl gen0 gen1 -> Incl (Ring gen0) (Ring gen1).
Proof.
intros; apply Ring_lub_alt, Incl_trans with gen1; [easy | apply Ring_Gen].
Qed.

Lemma Algebra_monot :
  Incl gen0 gen1 -> Incl (Algebra gen0) (Algebra gen1).
Proof.
intros; apply Algebra_lub_alt, Incl_trans with gen1; [easy | apply Algebra_Gen].
Qed.

Lemma Monotone_class_monot :
  Incl gen0 gen1 -> Incl (Monotone_class gen0) (Monotone_class gen1).
Proof.
intros; apply Monotone_class_lub_alt, Incl_trans with gen1; [easy | apply Monotone_class_Gen].
Qed.

Lemma Lsyst_monot :
  Incl gen0 gen1 -> Incl (Lsyst gen0) (Lsyst gen1).
Proof.
intros; apply Lsyst_lub_alt, Incl_trans with gen1; [easy | apply Lsyst_Gen].
Qed.

Lemma Sigma_ring_monot :
  Incl gen0 gen1 -> Incl (Sigma_ring gen0) (Sigma_ring gen1).
Proof.
intros; apply Sigma_ring_lub_alt, Incl_trans with gen1; [easy | apply Sigma_ring_Gen].
Qed.

Lemma Sigma_algebra_monot :
  Incl gen0 gen1 -> Incl (Sigma_algebra gen0) (Sigma_algebra gen1).
Proof.
intros; apply Sigma_algebra_lub_alt, Incl_trans with gen1; [easy | apply Sigma_algebra_Gen].
Qed.

Lemma Psyst_ext :
  Incl gen0 (Psyst gen1 A0) ->
  Incl gen1 (Psyst gen0 A0) ->
  Psyst gen0 A0 = Psyst gen1 A0.
Proof.
intros; apply Ext_equiv; split; now apply Psyst_lub_alt.
Qed.

Lemma Ring_ext :
  Incl gen0 (Ring gen1) ->
  Incl gen1 (Ring gen0) ->
  Ring gen0 = Ring gen1.
Proof.
intros; apply Ext_equiv; split; now apply Ring_lub_alt.
Qed.

Lemma Algebra_ext :
  Incl gen0 (Algebra gen1) ->
  Incl gen1 (Algebra gen0) ->
  Algebra gen0 = Algebra gen1.
Proof.
intros; apply Ext_equiv; split; now apply Algebra_lub_alt.
Qed.

Lemma Monotone_class_ext :
  Incl gen0 (Monotone_class gen1) ->
  Incl gen1 (Monotone_class gen0) ->
  Monotone_class gen0 = Monotone_class gen1.
Proof.
intros; apply Ext_equiv; split; now apply Monotone_class_lub_alt.
Qed.

Lemma Sigma_ring_ext :
  Incl gen0 (Sigma_ring gen1) ->
  Incl gen1 (Sigma_ring gen0) ->
  Sigma_ring gen0 = Sigma_ring gen1.
Proof.
intros; apply Ext_equiv; split; now apply Sigma_ring_lub_alt.
Qed.

Lemma Lsyst_ext :
  Incl gen0 (Lsyst gen1) ->
  Incl gen1 (Lsyst gen0) ->
  Lsyst gen0 = Lsyst gen1.
Proof.
intros; apply Ext_equiv; split; now apply Lsyst_lub_alt.
Qed.

Lemma Sigma_algebra_ext :
  Incl gen0 (Sigma_algebra gen1) ->
  Incl gen1 (Sigma_algebra gen0) ->
  Sigma_algebra gen0 = Sigma_algebra gen1.
Proof.
intros; apply Ext_equiv; split; now apply Sigma_algebra_lub_alt.
Qed.

End Subset_systems_Facts4.


Section Subset_system_alt_Facts1.

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

Variable gen : (U -> Prop) -> Prop. (* Generator. *)

Lemma Algebra_equiv_alt :
  Algebra gen = Gen is_Algebra gen.
Proof.
apply Ext_equiv; split; intros A HA.
(* *)
induction HA.
now apply Gen_ni_gen.
1,2,3: intros SS HSS1 HSS2; rewrite <- HSS1.
apply Algebra_wEmpty.
apply Algebra_Compl; now apply (Algebra_monot gen SS).
apply Algebra_Union; now apply (Algebra_monot gen SS).
(* *)
apply HA.
apply Algebra_idem.
apply Algebra_Gen.
Qed.

End Subset_system_alt_Facts1.


Section Subset_system_alt_Facts2.

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

Lemma is_Algebra_Inter_compat :
  @IInter_compat U is_Algebra.
Proof.
intros Idx HIdx; rewrite Algebra_equiv; repeat split.
(* *)
intros SS HSS; rewrite <- (HIdx SS HSS); apply Algebra_wEmpty.
(* *)
intros A HA SS HSS; rewrite <- (HIdx SS HSS).
now apply Algebra_Compl, Algebra_Gen, HA.
(* *)
intros A B HA HB SS HSS; rewrite <- (HIdx SS HSS).
now apply Algebra_Union; apply Algebra_Gen; [apply HA | apply HB].
Qed.

Variable gen0 gen1 : (U -> Prop) -> Prop. (* Generators. *)

Lemma Algebra_lub_alt_bis :
  Incl gen0 (Algebra gen1) ->
  Incl (Algebra gen0) (Algebra gen1).
Proof.
intros; rewrite (Algebra_equiv_alt gen0), (Algebra_equiv_alt gen1).
apply (Gen_lub_alt is_Algebra).
apply is_Algebra_Inter_compat.
now rewrite <- Algebra_equiv_alt.
Qed.

End Subset_system_alt_Facts2.


Section Psyst_Facts.

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

Variable gen : (U -> Prop) -> Prop. (* Generator. *)
Variable A0 : U -> Prop. (* Witness. *)

Lemma Psyst_Nonempty :
  Nonempty (Psyst gen A0).
Proof.
exists A0; apply Psyst_Mem.
Qed.

Lemma Psyst_Inter_finite :
  Inter_finite (Psyst gen A0).
Proof.
apply Inter_finite_equiv, Psyst_Inter.
Qed.

Lemma Psyst_Inter_monot_finite :
  Inter_monot_finite (Psyst gen A0).
Proof.
apply Inter_finite_monot, Psyst_Inter_finite.
Qed.

Lemma Psyst_wEmpty :
  Compl (Psyst gen A0) -> wEmpty (Psyst gen A0).
Proof.
intros H; apply Nonempty_wEmpty; [easy | apply Psyst_Inter | ].
exists A0; apply Psyst_Mem.
Qed.

Variable P : (U -> Prop) -> Prop. (* Subset system. *)

Lemma is_Psyst_wEmpty :
  is_Psyst P A0 -> is_Psyst (fun A => P A \/ A = emptyset) emptyset.
Proof.
intros H; rewrite Psyst_equiv in *; split.
now right.
now apply Inter_with_empty.
Qed.

End Psyst_Facts.


Section is_Semi_ring_Facts.

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

Variable P : (U -> Prop) -> Prop. (* Subset system. *)

Lemma is_Semi_ring_wEmpty :
  is_Semi_ring P -> wEmpty P.
Proof.
(* auto with subset_systems. (* is not working! *) *)
(*now unfold is_Semi_ring.*)
now intros [H _].
Qed.

Lemma is_Semi_ring_Inter :
  is_Semi_ring P -> Inter P.
Proof.
now intros [_ [H _]].
Qed.

Lemma is_Semi_ring_Part_diff_finite :
  is_Semi_ring P -> Part_diff_finite P.
Proof.
now intros [_ [_ H]].
Qed.

Lemma is_Semi_ring_is_Psyst :
  is_Semi_ring P -> is_Psyst P emptyset.
Proof.
intros; apply Psyst_equiv; split.
now apply is_Semi_ring_wEmpty.
now apply is_Semi_ring_Inter.
Qed.

Lemma is_Semi_ring_Inter_finite :
  is_Semi_ring P -> Inter_finite P.
Proof.
intros; rewrite <- is_Semi_ring_is_Psyst; try easy.
apply Psyst_Inter_finite.
Qed.

Lemma is_Semi_ring_Inter_monot_finite :
  is_Semi_ring P -> Inter_monot_finite P.
Proof.
intros; rewrite <- is_Semi_ring_is_Psyst; try easy.
apply Psyst_Inter_monot_finite.
Qed.

End is_Semi_ring_Facts.


Section Ring_Facts1.

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

Variable gen : (U -> Prop) -> Prop. (* Generator. *)

Lemma Ring_Inter :
  Inter (Ring gen).
Proof.
apply Diff_Inter, Ring_Diff.
Qed.

Lemma Ring_is_Psyst :
  is_Psyst (Ring gen) emptyset.
Proof.
apply Psyst_equiv; split; try easy.
apply Ring_wEmpty.
apply Ring_Inter.
Qed.

Lemma Ring_Inter_finite :
  Inter_finite (Ring gen).
Proof.
rewrite <- Ring_is_Psyst; apply Psyst_Inter_finite.
Qed.

Lemma Ring_Compl_loc :
  Compl_loc (Ring gen).
Proof.
apply Diff_Compl_loc, Ring_Diff.
Qed.

Lemma Ring_Sym_diff :
  Sym_diff (Ring gen).
Proof.
apply Sym_diff_Diff_equiv; [apply Ring_Union | apply Ring_Diff].
Qed.

Lemma Ring_Union_disj :
  Union_disj (Ring gen).
Proof.
apply Union_Union_disj, Ring_Union.
Qed.

Lemma Ring_Inter_monot_finite :
  Inter_monot_finite (Ring gen).
Proof.
apply Inter_finite_monot, Ring_Inter_finite.
Qed.

Lemma Ring_Union_finite :
  Union_finite (Ring gen).
Proof.
apply Union_finite_equiv, Ring_Union.
Qed.

Lemma Ring_Union_monot_finite :
  Union_monot_finite (Ring gen).
Proof.
apply Union_finite_monot, Ring_Union_finite.
Qed.

Lemma Ring_Union_disj_finite :
  Union_disj_finite (Ring gen).
Proof.
apply Union_finite_disj, Ring_Union_finite.
Qed.

Variable P : (U -> Prop) -> Prop. (* Subset system. *)

Lemma Ring_equiv_def :
  is_Ring P <->
  (Nonempty P \/ wEmpty P) /\
  (Diff P /\ Union P \/
   Diff P /\ Union_disj P \/
   Sym_diff P /\ Inter P \/
   Compl_loc P /\ Union_disj P /\ Inter P).
Proof.
rewrite Ring_equiv; split.
(* *)
intros [H1 H2]; repeat split.
now right.
now left.
(* *)
intros [[H1 | H1] [[H2 H3] | [[H2 H3] | [[H2 H3] | [H2 [H3 H4]]]]]]; repeat split; try easy.
1,2,4,7: apply Nonempty_wEmpty_Diff; try easy.
1,4,9: now apply Sym_diff_Diff.
2,5,6,9: apply Union_disj_Union; try easy.
1,2,3,5,7: now apply Compl_loc_Diff.
1,2: now apply Sym_diff_Union.
Qed.

Lemma is_Psyst_Sym_diff_is_Ring :
  forall (A0 : U -> Prop),
    is_Psyst P A0 -> Sym_diff P -> is_Ring P.
Proof.
intros A0 H1 H2; rewrite Ring_equiv_def; split.
left; rewrite <- H1; apply Psyst_Nonempty.
right; right; left; split; try easy.
rewrite <- H1; apply Psyst_Inter.
Qed.

End Ring_Facts1.


Section Ring_Facts2.

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

Variable gen : (U -> Prop) -> Prop. (* Generator. *)

Lemma Incl_Psyst_Ring :
  Incl (Psyst gen emptyset) (Ring gen).
Proof.
rewrite <- Ring_is_Psyst; apply Psyst_monot, Ring_Gen.
Qed.

Lemma Incl_Ring_Psyst :
  let P := Psyst gen emptyset in
  Sym_diff P -> Incl (Ring gen) P.
Proof.
intros P H1; assert (H2 : is_Ring P).
  apply Ring_equiv; repeat split.
  apply Psyst_Mem.
  apply Sym_diff_Diff; try easy; apply Psyst_Inter.
  apply Sym_diff_Union; try easy; apply Psyst_Inter.
apply Ring_lub; [easy | apply Psyst_Gen].
Qed.

Lemma Ring_Psyst :
  Ring (Psyst gen emptyset) = Ring gen.
Proof.
intros; apply Ext_equiv; split.
now apply Ring_lub_alt, Incl_Psyst_Ring.
apply Ring_monot, Psyst_Gen.
Qed.

End Ring_Facts2.


Section Ring_Facts3.

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

Variable gen : (U -> Prop) -> Prop. (* Generator. *)

Hypothesis H : is_Semi_ring gen.

(* Explicit_ring represents Union_disj_finite_closure gen. *)

Lemma Explicit_ring_Gen :
  Incl gen (Union_disj_finite_closure gen).
Proof.
intros A HA.
exists (repeat_1 A), 0; repeat split; try easy.
now rewrite union_finite_0.
apply disj_finite_0.
Qed.

Lemma Explicit_ring_wEmpty :
  wEmpty (Union_disj_finite_closure gen).
Proof.
destruct H as [H1 _].
now apply Explicit_ring_Gen.
Qed.

Lemma Explicit_ring_Diff :
  Diff (Union_disj_finite_closure gen).
Proof.
destruct H as [_ [H2 H3]].
now apply Diff_Union_disj_finite_closure.
Qed.

Lemma Explicit_ring_Union_disj :
  Union_disj (Union_disj_finite_closure gen).
Proof.
apply Union_disj_Union_disj_finite_closure.
Qed.

Lemma Ring_explicit_aux1 :
  Incl (Ring gen) (Union_disj_finite_closure gen).
Proof.
apply Ring_lub.
apply Ring_equiv_def; split.
right; apply Explicit_ring_wEmpty.
right; left; split; [apply Explicit_ring_Diff | apply Explicit_ring_Union_disj].
apply Explicit_ring_Gen.
Qed.

Lemma Ring_explicit_aux2 :
  Incl (Union_finite_closure gen) (Ring gen).
Proof.
intros A [B [N [HB1 HB2]]].
rewrite HB2; apply Ring_Union_finite.
intros; now apply Ring_Gen, HB1.
Qed.

Lemma Ring_explicit_aux :
  Ring gen = Union_disj_finite_closure gen /\
  Union_disj_finite_closure gen = Union_finite_closure gen.
Proof.
split; apply Ext_equiv; split.
2: apply Incl_trans with (Union_finite_closure gen).
5: apply Incl_trans with (Ring gen).
1,6: apply Ring_explicit_aux1.
1,3: apply Union_finite_closure_Incl.
1,2: apply Ring_explicit_aux2.
Qed.

Lemma Ring_explicit :
  Ring gen = Union_disj_finite_closure gen.
Proof.
apply Ring_explicit_aux.
Qed.

Lemma Ring_explicit_alt :
  Ring gen = Union_finite_closure gen.
Proof.
destruct Ring_explicit_aux as [H1 H2].
now rewrite H1.
Qed.

End Ring_Facts3.


Section Semi_algebra_Facts.

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

Variable gen : (U -> Prop) -> Prop. (* Generator. *)

Lemma is_Semi_algebra_equiv_def_Part_diff_finite :
  is_Semi_algebra gen <-> wFull gen /\ Inter gen /\ Part_diff_finite gen.
Proof.
split.
(* *)
intros [H1 [H2 H3]]; repeat split; try easy.
now apply Part_compl_Part_diff_finite.
(* *)
intros [H1 [H2 H3]]; repeat split; try easy.
now apply Part_diff_Part_compl_finite.
Qed.

Lemma is_Semi_algebra_equiv_def_Semi_ring :
  is_Semi_algebra gen <-> is_Semi_ring gen /\ wFull gen.
Proof.
rewrite is_Semi_algebra_equiv_def_Part_diff_finite; unfold is_Semi_ring.
repeat split; try easy.
apply wFull_wEmpty_finite; try easy.
now apply Part_diff_Part_compl_finite.
Qed.

Lemma is_Semi_algebra_is_Semi_ring :
  is_Semi_algebra gen -> is_Semi_ring gen.
Proof.
now rewrite is_Semi_algebra_equiv_def_Semi_ring.
Qed.

(*
Lemma Semi_algebra_is_Psyst_gen :
  forall (A0 : U -> Prop),
    Semi_algebra gen A0 -> is_Psyst (Semi_algebra gen) A0.
Proof.
intros A0 HA0; apply Psyst_equiv; split; try easy.
apply Semi_algebra_Inter.
Qed.

Lemma Semi_algebra_is_Psyst :
  is_Psyst (Semi_algebra gen) fullset.
Proof.
apply Semi_algebra_is_Psyst_gen, Semi_algebra_wFull.
Qed.

Lemma Semi_algebra_Inter_finite :
  Inter_finite (Semi_algebra gen).
Proof.
rewrite <- Semi_algebra_is_Psyst; apply Psyst_Inter_finite.
Qed.

Lemma Semi_algebra_Part_diff_finite :
  Part_diff_finite (Semi_algebra gen).
Proof.
Aglopted.
*)

End Semi_algebra_Facts.


Hint Resolve <- Ring_equiv : subset_systems. (* Apparently not working... *)


Section Algebra_Facts1.

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

Variable gen : (U -> Prop) -> Prop. (* Generator. *)