0

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?

3
  • See this SO answer regarding set libraries in Coq.
    – Ana Borges
    Nov 2 at 14:59
  • @AnaBorges Thanks. According to that answer, the only fit would be Ensembles, since I want to model infinite sets. Why did you define it "a bit clunky"? Should I avoid it? Nov 3 at 8:48
  • @AnaBorges Ah, I probably understood. I made a Complete Lattice typeclass with Ensembles, and it's pretty much impossible to instantiate it on finite sets like bool. It should not be that much of a problem in the long run, as I intend on only working with infinite lattices, but I guess that's a big limitation.. Nov 3 at 11:07

1 Answer 1

0

You might want to take some inspiration from what has been done into mathcomp regarding (partial) orders. See, for instance, order.v.

2
  • Thanks. In general though, how do I do stuff with sets? Is there a particular library you would suggest that models arbitrary sets and basic stuff like inclusion, subset etc? I could also do that from scratch (e.g. modeling sets of A as A -> Prop), and it would probably be helpful as I'm an absolute beginner with Coq, but maybe that's a bit too much for now :) Nov 2 at 13:33
  • For mathematical reasoning in Coq, you can look at the mathcomp book, available at this link; finite sets are discussed there. For Standard Coq, you can also look at Sets. Nov 2 at 13:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.