(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** * Order Theory with Classes.

   This module implements the lattice on the powerset of a type a.

   Author: Matthieu Sozeau <sozeau@lri.fr>
   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
                91405 Orsay, France 

*)

Require Import Coq.Program.Program.

Require Export Order.Lattice.
Require Export Order.Quotients.

Require Import Ensembles.

Implicit Arguments Empty_set [[U]].
Implicit Arguments Full_set [[U]].
Implicit Arguments Couple [[U]].
Implicit Arguments Singleton [[U]].
Implicit Arguments Union [[U]].
Implicit Arguments Intersection [[U]].
Implicit Arguments Full_intro [[U]].

Parameter A : Type.

Definition empty_infimum : infimum (@empty_subset A).
Proof. 
  reduce_goal.
  inversion H.
Qed.

Definition full_supremum : supremum (@full_subset A).
Proof. reduce_goal. exact I. 
Qed.

Definition union (s s' : subset A) : subset A :=
  fun x => x ∈ s \/ x ∈ s'.

Infix "∪" := union (at level 55).

Definition intersection (s s' : subset A) : subset A :=
  fun x => x ∈ s /\ x ∈ s'.

Infix "∩" := intersection (at level 55).

Infix "⊆" := subset_inclusion (at level 55).
Notation " x  ⊇  y " := (flip subset_inclusion x y) (at level 55).

Ltac subsets :=
  unfold flip, subset_inclusion, subset_equality, intersection, union, in_subset in * ; intuition.

Tactic Notation "rewrite" "*" hyp(H) := repeat (setoid_rewrite H at 1).

Instance binary_glb : BinaryGlb _ intersection.
Proof. firstorder. Qed.

Instance binary_lub : BinaryLub _ union.
Proof. firstorder. Qed.

Program Instance meet_semi : MeetSemiLattice _ intersection.

  Next Obligation.
  Proof. firstorder. Qed.

Program Instance join_semi : JoinSemiLattice _ union.

  Next Obligation.
  Proof. firstorder. Qed.

Program Instance subset_lattice : Lattice _ meet_semi join_semi.

Print BoundedLattice.