1

我希望在精益定理证明器中证明这个定理。首先，我需要定义偏序集之类的东西，以便我可以定义下确界/上确界。这是如何在精益中完成的？本教程提到了 setoid，它们是具有相关等价关系的类型。但我不清楚这有什么帮助。

4

2 回答 2

5

我不是精益用户，但这是我在 Agda 中定义它的方式。它可能无法直接翻译——类型理论有很多种——但它至少应该是一个指针！

我们将使用二进制逻辑关系，它们是这种类型的同义词：

Rel : Set -> Set1
Rel A = A -> A -> Set

我们需要命题相等：

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

可以说一个逻辑关系是自反的、反对称的和传递的意味着什么。

Refl : {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 _<=_

作为记录（哈哈），以下是教程中的setoid示例如何转换为 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 _~_

更新：我安装了 Lean，犯了很多语法错误，最终得到了这个（可能不是惯用的，但直截了当的）翻译。函数变成definitions，records变成structures。

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 中定义的自反性（等）定义的内置版本。我还注意到 Lean 似乎很乐意让我Type在上面的返回类型中省略宇宙级别Rel，这是一个很好的接触。

于 2016-04-01T17:11:18.740 回答
1

精益的标准库已经包含了各种订单的定义。然而，虽然实数有inf和的定义sup，但我认为 ℚ 还没有定义（或适用的一般定义，因为这两种类型都不是 a complete_lattice）。

于 2016-04-02T23:17:05.030 回答