I defined a Lattice
typeclass in Coq:
Class PartialOrder A : Type := {
le : A -> A -> Prop;
}.
Notation "x <= y" := (le x y).
Class Lattice A `{PartialOrder A} : Type := {
top : A;
bottom : A;
join : A -> A -> A;
meet : A -> A -> A;
def_meet : forall a b : A,
(meet a b) <= a /\ (meet a b) <= b /\
(forall w : A, (w <= a) /\ (w <= b) -> w <= (meet a b));
def_join : forall a b : A,
a <= (join a b) /\ b <= (join a b) /\
(forall w : A, (a <= w) /\ (b <= w) -> (join a b) <= w);
def_top : forall a : A, le a top;
def_bottom : forall a : A, le bottom a;
exists_meet : forall a b : A, exists c : A , join a b = c;
exists_join : forall a b : A, exists c : A , meet a b = c;
}.
and provided bool
as an instance.
I would now like to define complete lattices, but this requires a law stating that for any set S
(not necessarily finite, so induction on the above definition is not enough), S
has a join and meet. How should I approach this?