我如何在精益中定义偏序集？

Question

我想证明 this theorem in the Lean theorem prover. First, I need to define things like partially ordered sets so that I can define infimum/supremum. How is this done in Lean? The tutorial 提到了 setoids，它们是具有关联等价关系。但我不清楚这有什么帮助。

Answer 1

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

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

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

我们需要命题相等：

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

可以说出逻辑关系是什么意思reflexive, antisymmetric, and transitive。

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 _<=_

一个poset只是一个具有偏序关系的集合。

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 _~_

Update：我安装了 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 中自己定义的自反性（等）定义的 built-in versions。我还注意到 Lean 似乎很乐意让我在上面 Rel 的 return 类型中省略 Type 的宇宙级别，这是一个很好的接触。

Answer 2

Lean 的标准库已经包含 various orders. However, while there are 的定义 inf 和 sup 的实数定义，我认为没有用于 ℚ 的定义，但是（或适用的一般定义，因为这些类型都不是 complete_lattice).

我如何在精益中定义偏序集？

How do I define partially ordered sets in Lean?

set

theorem-proving

dependent-type

lean