如何在 Coq 中推理集合？ - 定义完整格子

Question

我在 Coq 中定义了一个

Lattice

类型类：

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;
}.

并提供

bool

作为实例。

我现在想定义完全格，但这需要一条定律，说明对于任何集合

S

（不一定是有限的，因此对上述定义的归纳是不够的），

S

有一个连接和满足。我应该如何处理这个问题？

Answer 1

您可能想从 mathcomp 中有关（部分）订单的工作中获得一些灵感。例如，参见 order.v。