如何在精益中定义偏序集？
如何在精益中定义偏序集？
提问于 2016-03-27 18:48:53
我希望在精益定理证明器中证明这个定理。首先，我需要定义像偏序集这样的东西，这样我就可以定义infimum/上界。在精益中是如何做到这一点的？本教程提到了setoid，它们是具有关联的等价关系的类型。但我不清楚这会有什么帮助。
回答 2
Stack Overflow用户
回答已采纳
发布于 2016-04-01 17:11:18
我不是精益用户，但我在Agda中如何定义它。它可能不会直接翻译--类型理论有很多变化--但它至少应该是一个指针！
我们将处理二进制逻辑关系，它们是此类同义词的居民：
Rel : Set -> Set1
Rel A = A -> A -> Set我们需要命题平等：
data _==_ {A : Set} (x : A) : A -> Set where
refl : x == xRefl : {A : Set} -> Rel A -> Set
Refl {A} _~_ = {x : A} -> x ~ x
Antisym : {A : Set} -> Rel A -> Set
Antisym {A} _~_ = {x y : A} -> x ~ y -> y ~ x -> x == y
Trans : {A : Set} -> Rel A -> Set
Trans {A} _~_ = {x y z : A} -> x ~ y -> y ~ z -> x ~ z要成为一个局部秩序，它必须是全部三个。
record IsPartialOrder {A : Set} (_<=_ : Rel A) : Set where
field
reflexive : Refl _<=_
antisymmetric : Antisym _<=_
transitive : Trans _<=_偏序集只是一个具有偏序关系的集合。
record Poset : Set1 where
field
carrier : Set
_<=_ : Rel carrier
isPartialOrder : IsPartialOrder _<=_为了记录( ha )，下面是教程中的刚毛示例如何转换为Agda：
Sym : {A : Set} -> Rel A -> Set
Sym {A} _~_ = {x y : A} -> x ~ y -> y ~ x
record IsEquivalence {A : Set} (_~_ : Rel A) : Set where
field
reflexive : Refl _~_
symmetric : Sym _~_
transitive : Trans _~_
record Setoid : Set1 where
field
carrier : Set
_~_ : Rel carrier
isEquivalence : IsEquivalence _~_Update：我安装了精益，提交了大量语法错误，并最终完成了这个翻译(可能不是惯用的，但很简单)。函数变成definition，record变成structure。
definition Rel (A : Type) : Type := A -> A -> Prop
definition IsPartialOrder {A : Type}(P : Rel A) :=
reflexive P ∧ anti_symmetric P ∧ transitive P
structure Poset :=
(A : Type)
(P : Rel A)
(ispo : IsPartialOrder P)我使用的是自反性(等)定义的内置版本，我在上面的Agda中定义了自己。我还注意到，精益似乎很乐意让我在上面的返回类型Type中省略宇宙级别的Rel，这是一个很好的触摸。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/36251229
复制相关文章
相似问题
腾讯云开发者
