ImpAlg.Powerset

Set Implicit Arguments.
Set Contextual Implicit.
Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Export Relation_Definitions.
Require Import Sets.Ensembles.
Require Import Sets.Powerset.
Require Import ImpAlg.Lattices.

Section Powerset.
Context `{X:Type}.

Infix "⊆":=(Included X) (at level 75).

Global Instance Powerset_Order (A:@Ens X) : @Lattices.Order (Ensemble X):=
{ ord := Included X;}.
Proof.
- auto with sets.
- auto with sets.
- auto with sets.
Defined.

Lemma Intersection_sym (A B:@Ens X) : Intersection X A B = Intersection X B A.
Proof.
apply Extensionality_Ensembles.
split;intros x H; inversion H;auto with sets.
Qed.

Lemma Intersection_associative (A B C:@Ens X) :
Intersection X A (Intersection X B C)= Intersection X (Intersection X A B) C.
Proof.
apply Extensionality_Ensembles.
split;intros x H; inversion H as [y H0 H1 H2];try (inversion H1);try (inversion H0);
repeat(apply Intersection_intro);auto with sets.
Qed.

Lemma Intersection_absorptive (A B :@Ens X) :
Intersection X A (Union X A B)= A.
Proof.
apply Extensionality_Ensembles.
split;intros x H.
- inversion H. inversion H1; auto with sets.
- apply Intersection_intro; auto.
apply Union_introl;auto.
Qed.

Lemma Intersection_idempotent (A :@Ens X) :
Intersection X A A= A.
Proof.
apply Extensionality_Ensembles.
split;intros x H.
- now inversion H.
- apply Intersection_intro; auto.
Qed.

Hint Resolve Intersection_sym Intersection_associative Intersection_absorptive Intersection_idempotent:sets.

Lemma Union_sym (A B:@Ens X) : Union X A B = Union X B A.
Proof.
apply Extensionality_Ensembles.
split;intros x H; inversion H;auto with sets.
Qed.

Lemma Union_associative (A B C:@Ens X) :
Union X A (Union X B C)= Union X (Union X A B) C.
Proof.
apply Extensionality_Ensembles.
split;intros x H; inversion H as [y H0 H1| y H0 H1];try (inversion H1);try (inversion H0);
auto with sets.
Qed.

Lemma Union_absorptive (A B :@Ens X) :
Union X A (Intersection X A B)= A.
Proof.
apply Extensionality_Ensembles.
split;intros x H.
- inversion H; auto with sets. inversion H0; auto.
- apply Union_introl; auto.
Qed.

Lemma Union_idempotent (A :@Ens X) :
Union X A A= A.
Proof.
apply Extensionality_Ensembles.
split;intros x H.
- now inversion H.
- apply Union_introl; auto.
Qed.

Hint Resolve Union_sym Union_associative Union_absorptive Union_idempotent:sets.

Lemma Intersection_included (A B:Ensemble X) : Included X A B ↔ A = Intersection X A B.
Proof.
split;intro H.
- apply Extensionality_Ensembles;split;auto with sets.
- intros x Hx. rewrite H in Hx. inversion Hx. auto.
Qed.

Global Instance Powerset_Lattice (A:@Ens X) : @Lattice _ (Powerset_Order A):=
{meet:=Intersection X;join:=Union X}.
Proof.
- auto with sets.
- auto with sets.
- auto with sets.
- auto with sets.
- auto with sets.
- auto with sets.
- auto with sets.
- auto with sets.
- intros. apply Intersection_included.
Defined.

Definition Intersection_set (A:@Ens (@Ens X)):=
    fun (x:X) => ∀ B, A B → B x.

Definition Union_set (A:@Ens (@Ens X)) :=
    fun (x:X) => ∃ B, A B ∧ B x.

Lemma Intersection_set_lb : ∀ (A : Ens) B , A B → Included X (Intersection_set A) B.
Proof.
intros A B H x Hx.
apply Hx.
apply H.
Qed.

Lemma Intersection_set_glb:
  ∀ (A : Ens) B , (∀ C , A C → Included X B C) → Included X B (Intersection_set A).
Proof.
intros A B H x Hx C HC.
apply H;assumption.
Qed.

Lemma Union_set_ub : ∀ (A : Ens) B , A B → Included X B (Union_set A).
Proof.
intros A B H x Hx.
exists B;split;assumption.
Qed.

Lemma Union_set_lub :
  ∀ (A : Ens) B , (∀ C , A C → Included X C B) → Included X (Union_set A) B.
Proof.
intros A B H x [C [HC Hx]].
apply (H C HC). assumption.
Qed.

Hint Resolve Intersection_set_lb Intersection_set_glb Union_set_ub Union_set_lub : sets.

Global Instance Powerset_CompleteLattice (A:@Ens X) :
 @CompleteLattice _ _ (@Powerset_Lattice A)
:= {meet_set:=Intersection_set ;join_set:=Union_set;
       meet_elim:=Intersection_set_lb; meet_intro:=Intersection_set_glb;
       join_elim:=Union_set_ub; join_intro:=Union_set_lub;
}.

End Powerset.