如何在Coq中定义完全格？解决任意集合交并存在性问题

核心思路 #

完全格的核心要求是任意子集（包括无限子集）都存在上确界（并）和下确界（交）。在Coq中，我们可以通过扩展原有Lattice类型类，添加针对任意子集的上确界/下确界操作及对应公理来实现。

步骤1：修正原有格定义的冗余 #

你原有的Lattice定义中，exists_meet和exists_join是冗余的——因为join和meet已经是A -> A -> A的函数，对于任意a b，join a b本身就是满足条件的c，无需额外声明存在性，可以直接删除这两个字段。

步骤2：定义完全格类型类 #

我们可以让CompleteLattice继承自已有的Lattice，避免重复编写格的基础结构和公理，只需要新增任意子集的上确界/下确界操作及公理即可：

Class CompleteLattice A `{PartialOrder A} `{Lattice A} : Type := {
  (* 任意子集的上确界（并）：用谓词S: A->Prop表示A的子集，S x意味着x属于该子集 *)
  sup : (A -> Prop) -> A;
  (* 任意子集的下确界（交） *)
  inf : (A -> Prop) -> A;

  (* 上确界的公理：满足两个条件 *)
  def_sup : forall S : A -> Prop,
      (* 1. 子集S中的所有元素都小于等于上确界sup S *)
      (forall x : A, S x -> x <= sup S) /\
      (* 2. 任何大于等于S中所有元素的w，都大于等于sup S（即sup S是最小上界） *)
      (forall w : A, (forall x : A, S x -> x <= w) -> sup S <= w);

  (* 下确界的公理：满足两个条件 *)
  def_inf : forall S : A -> Prop,
      (* 1. 下确界inf S小于等于子集S中的所有元素 *)
      (forall x : A, S x -> inf S <= x) /\
      (* 2. 任何小于等于S中所有元素的w，都小于等于inf S（即inf S是最大下界） *)
      (forall w : A, (forall x : A, S x -> w <= x) -> w <= inf S);
}.

如果不想依赖原有Lattice，也可以直接定义包含完整结构的CompleteLattice：

Class CompleteLattice 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, a <= top;
  def_bottom : forall a : A, bottom <= a;

  (* 完全格新增操作 *)
  sup : (A -> Prop) -> A;
  inf : (A -> Prop) -> A;

  (* 完全格公理 *)
  def_sup : forall S : A -> Prop,
      (forall x : A, S x -> x <= sup S) /\
      (forall w : A, (forall x : A, S x -> x <= w) -> sup S <= w);
  def_inf : forall S : A -> Prop,
      (forall x : A, S x -> inf S <= x) /\
      (forall w : A, (forall x : A, S x -> w <= x) -> w <= inf S);
}.

步骤3：实现bool类型的完全格实例 #

基于你已有的BoolPartialOrder和BoolLattice，可以扩展出BoolCompleteLattice：

Instance BoolCompleteLattice : CompleteLattice bool := {
  sup := fun S => 
    if S false then 
      if S true then true else false 
    else true;
  inf := fun S => 
    if S true then 
      if S false then false else true 
    else false;
  def_sup := fun S =>
    conj
      (* 验证子集元素都<=sup S *)
      (fun x => match x with
                | false => fun H => H -> (false <= sup S)
                | true => fun H => H -> (true <= sup S)
                end)
      (* 验证sup S是最小上界 *)
      (fun w => fun H => match w with
                        | true => I
                        | false => fun _ => sup S <= false
                        end);
  def_inf := fun S =>
    conj
      (* 验证inf S<=子集所有元素 *)
      (fun x => match x with
                | false => fun H => H -> (inf S <= false)
                | true => fun H => H -> (inf S <= true)
                end)
      (* 验证inf S是最大下界 *)
      (fun w => fun H => match w with
                        | false => I
                        | true => fun _ => true <= inf S
                        end);
}.

说明 #

• Coq中用**谓词A -> Prop**表示任意子集：S x为真当且仅当x属于子集S，这种方式可以覆盖有限和无限子集。
• 原有格的二元join/meet可以通过完全格的sup/inf推导：例如join a b = sup (fun x => x = a \/ x = b)，你可以在Coq中证明这个等价性。

内容的提问来源于stack exchange，提问作者mell_o_tron