Set_system_finite.v

(**
This file is part of the Elfic library

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

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.
*)

Require Import Set_system_base Set_system_def.


Section Set_system_Facts1.

Context {U : Type}.
Variable P : set_system U.

Lemma Psyst_equiv :
  forall (A0 : set U),
    is_Psyst P A0 <-> P A0 /\ Inter P.
Proof.
split.
(* *)
intros H; rewrite <- H; auto with set_system.
(* *)
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 set_system.
(* *)
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 set_system.
(* *)
intros [H1 [H2 H3]]; apply Ext; split.
intros H4; induction H4; try easy; [now apply H2 | now apply H3].
apply Algebra_Gen.
Qed.

End Set_system_Facts1.


Section Set_system_Facts2.

Context {U : Type}.
Variable gen0 gen1 : set_system U.
Variable A0 : set U.

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.

End Set_system_Facts2.


Section Set_system_Facts3.

Context {U : Type}.
Variable P gen : set_system U.
Variable A0 : set U.

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.

End Set_system_Facts3.


Section Set_system_Facts4.

Context {U : Type}.
Variable gen : set_system U.
Variable A0 : set U.

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.

Variable gen0 gen1 : set_system U. (* 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 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.

End Set_system_Facts4.


Section Set_system_alt_Facts1.

Context {U : Type}.
Variable gen : set_system U.

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 Set_system_alt_Facts1.


Section Set_system_alt_Facts2.

Context {U : Type}.

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 : set_system U. (* 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 Set_system_alt_Facts2.


Section Psyst_Facts.

Context {U : Type}.
Variable gen : set_system U.
Variable A0 : set U.

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 : set_system U.

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}.
Variable P : set_system U.

Lemma is_Semi_ring_wEmpty :
  is_Semi_ring P -> wEmpty P.
Proof.
(* auto with set_system. (* 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}.
Variable gen : set_system U.

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 : set_system U.

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 : set U),
    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}.
Variable gen : set_system U.

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}.
Variable gen : set_system U.
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; replace A with (cst_seq A 0) by easy.
rewrite <- (union_finite_0 (cst_seq A)); apply Udfc; try easy.
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 Union_disj_finite_closure_Diff.
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 HA; induction HA as [B N HB]; apply Ring_Union_finite.
intros; now apply Ring_Gen, HB.
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}.
Variable gen : set_system U.

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 : set U),
    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.


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


Section Algebra_Facts1.

Context {U : Type}.
Variable gen : set_system U.

Lemma Algebra_Diff :
  Diff (Algebra gen).
Proof.
apply Union_Diff_equiv; auto with set_system.
Qed.

Local Hint Resolve Algebra_Diff : set_system.
(*Print HintDb set_system.*)

Lemma Algebra_is_Ring :
  is_Ring (Algebra gen).
Proof.
(* auto with set_system.*) apply Ring_equiv; auto with set_system.
Qed.

Lemma Algebra_Compl_loc :
  Compl_loc (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Compl_loc.
Qed.

Lemma Algebra_Sym_diff :
  Sym_diff (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Sym_diff.
Qed.

Lemma Algebra_Inter :
  Inter (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Inter.
Qed.

Lemma Algebra_Union_disj :
  Union_disj (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_disj.
Qed.

Lemma Algebra_Inter_finite :
  Inter_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Inter_finite.
Qed.

Lemma Algebra_Inter_monot_finite :
  Inter_monot_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Inter_monot_finite.
Qed.

Lemma Algebra_Union_finite :
  Union_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_finite.
Qed.

Lemma Algebra_Union_monot_finite :
  Union_monot_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_monot_finite.
Qed.

Lemma Algebra_Union_disj_finite :
  Union_disj_finite (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_Union_disj_finite.
Qed.

Lemma Algebra_wFull :
  wFull (Algebra gen).
Proof.
apply wFull_wEmpty_equiv.
apply Algebra_Compl.
apply Algebra_wEmpty.
Qed.

Lemma Algebra_Compl_rev :
  Compl_rev (Algebra gen).
Proof.
apply Compl_equiv, Algebra_Compl.
Qed.

Lemma Algebra_is_Psyst :
  is_Psyst (Algebra gen) emptyset.
Proof.
rewrite <- Algebra_is_Ring; apply Ring_is_Psyst.
Qed.

Lemma Algebra_equiv_def :
  is_Algebra gen <-> wFull gen /\ Diff gen.
Proof.
split.
(* *)
intros H; rewrite <- H; split; [apply Algebra_wFull | apply Algebra_Diff].
(* *)
intros [H1 H2]; assert (H3 : Compl gen) by now apply Compl_loc_Compl.
rewrite Algebra_equiv; repeat split; try easy.
now apply wFull_wEmpty_equiv.
now apply Union_Diff_equiv.
Qed.

End Algebra_Facts1.


Section Algebra_Facts2.

Context {U : Type}.
Variable gen : set_system U.

Lemma Incl_Ring_Algebra :
  Incl (Ring gen) (Algebra gen).
Proof.
rewrite <- Algebra_is_Ring; apply Ring_lub_alt.
intros A HA; now apply Ring_Gen, Algebra_Gen.
Qed.

Lemma Incl_Psyst_Algebra :
  Incl (Psyst gen emptyset) (Algebra gen).
Proof.
apply Incl_trans with (Ring gen).
apply Incl_Psyst_Ring.
apply Incl_Ring_Algebra.
Qed.

Lemma Upgrade_Ring_is_Algebra :
  forall (P : set_system U),
    is_Ring P ->
    (wFull P \/ Compl P) ->
    is_Algebra P.
Proof.
intros P H1 [H2 | H2].
rewrite Algebra_equiv_def; now rewrite Ring_equiv in H1.
rewrite Algebra_equiv; repeat split.
rewrite <- H1; apply Ring_wEmpty.
1,2: now rewrite Ring_equiv in H1.
Qed.

Lemma Algebra_of_Ring :
  Algebra (Ring gen) = Algebra gen.
Proof.
apply Ext_equiv; split.
rewrite <- (Algebra_idem gen).
apply Algebra_monot, Incl_Ring_Algebra.
apply Algebra_monot, Ring_Gen.
Qed.

Lemma Upgrade_Ring_Algebra :
  (wFull (Ring gen) \/ Compl (Ring gen)) ->
  Ring gen = Algebra gen.
Proof.
intros H.
generalize (Upgrade_Ring_is_Algebra (Ring gen)); intros H3.
rewrite <- H3; try easy.
apply Algebra_of_Ring.
apply Ring_idem.
Qed.

Lemma Incl_Algebra_Psyst :
  let P := Psyst gen emptyset in
  Compl P -> Incl (Algebra gen) P.
Proof.
intros P H1; assert (H2 : is_Algebra P).
  apply Algebra_equiv; repeat split; try easy.
  now apply Psyst_wEmpty.
  apply Union_Inter_equiv; [easy | apply Psyst_Inter].
apply Algebra_lub; [easy | apply Psyst_Gen].
Qed.

Lemma Algebra_Psyst :
  Algebra (Psyst gen emptyset) = Algebra gen.
Proof.
apply Ext_equiv; split.
now apply Algebra_lub_alt, Incl_Psyst_Algebra.
apply Algebra_monot, Psyst_Gen.
Qed.

End Algebra_Facts2.


Section Algebra_Facts3.

Context {U : Type}.
Variable gen : set_system U.
Hypothesis H : is_Semi_algebra gen.

Lemma Algebra_explicit_aux :
  Algebra gen = Union_disj_finite_closure gen /\
  Union_disj_finite_closure gen = Union_finite_closure gen.
Proof.
rewrite is_Semi_algebra_equiv_def_Semi_ring in H.
destruct H as [H1 H2]; clear H.
destruct (Ring_explicit_aux gen H1) as [H3 H4].
split; try easy; clear H4.
rewrite <- H3; symmetry; rewrite Upgrade_Ring_Algebra; try easy.
left; now apply Ring_Gen.
Qed.

Lemma Algebra_explicit :
  Algebra gen = Union_disj_finite_closure gen.
Proof.
apply Algebra_explicit_aux.
Qed.

Lemma Algebra_explicit_alt :
  Algebra gen = Union_finite_closure gen.
Proof.
destruct Algebra_explicit_aux as [H1 H2].
now rewrite H1.
Qed.

End Algebra_Facts3.


Section More_Facts.

Context {U : Type}.
Variable gen : set_system U.

Lemma Algebra_Prop : forall P, Algebra gen (prop_cst P).
Proof.
intros P; case (excluded_middle_informative P); intros.
rewrite (set_ext (prop_cst P) fullset); [apply Algebra_wFull | easy].
rewrite (set_ext (prop_cst P) emptyset); [apply Algebra_wEmpty | easy].
Qed.

End More_Facts.


Section Trace_Facts.

Context {U : Type}.
Variable P : set_system U.
Variable A0 A : set U.

Lemma Trace_Psyst : is_Psyst P A0 -> is_Psyst (Trace A P) (trace A A0).
Proof.
rewrite 2!Psyst_equiv; intros [HP1 HP2]; split; try easy.
apply Trace_Inter; easy.
Qed.

Lemma Trace_Ring : is_Ring P -> is_Ring (Trace A P).
Proof.
rewrite 2!Ring_equiv; intros [HP1 [HP2 HP3]]; repeat split.
apply Trace_wEmpty; easy.
apply Trace_Diff; easy.
apply Trace_Union; easy.
Qed.

Lemma Trace_Algebra : is_Algebra P -> is_Algebra (Trace A P).
Proof.
rewrite 2!Algebra_equiv; intros [HP1 [HP2 HP3]]; repeat split.
apply Trace_wEmpty; easy.
apply Trace_Compl; easy.
apply Trace_Union; easy.
Qed.

End Trace_Facts.