Coq 中的完整原子布尔代数

Question

在CoqId我进入了

Variables s p e t f: Type.

我现在想要解释类型

e

的元素集具有完整原子布尔代数的结构。当然，要做到这一点，我们需要在解释类型

e

的元素集合中有一个底部元素 BOT 和一个顶部元素 TOP。也就是说，解释类型

e

的元素集必须形成一个布尔代数，其中它的每个子集都必须有一个连接（一个上确界），并且对于这个布尔代数中不是 BOT 的任何元素，有一个不是 BOT 的元素 c，并且不是存在一个不是 BOT 的元素 d，并且 c 在布尔代数的排序中低于 d。

我意识到这些是术语解释的语义条件，c、d BOT 和 TOP 是类型术语的模型理论解释

e

.

然后我的问题是我需要在 CoqId 中做什么，以确保类型

e

的行为方式使得作为模型理论解释的元素集形成一个完整的原子布尔代数。我想我需要一个表示 BOT 的术语和一个表示 TOP 的术语，

e

类型的术语之间的排序关系，一个构成

e

类型的任意子集的总和的运算符和一个否定运算符输入

e

.

如果你们有任何想法，我会非常感兴趣。