Как определить частично упорядоченные множества в Lean?

Question

Я хочу доказать эту теорему в доказательстве теоремы Лин. Во-первых, мне нужно определить такие вещи, как частично упорядоченные множества, чтобы я мог определить infimum / supremum. Как это делается в Lean? В учебнике упоминаются сетоиды, которые являются типами со связанным отношением эквивалентности. Но мне не ясно, как это могло бы помочь.

Answer 1

Я не пользователь Lean, но вот как я определил бы это в 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 _<=_

Poset - это просто набор, оснащенный отношением частичного порядка.

record Poset : Set1 where
  field
    carrier : Set
    _<=_ : Rel carrier
    isPartialOrder : IsPartialOrder _<=_

---

Для записи (ха-ха), вот как пример сетоида из учебника переводится на 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, допустил множество синтаксических ошибок и в конце концов пришел к этому (вероятно, не идиоматическому, но прямому) переводу. Функции становятся definitionс и recordстали 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 выше. Я также замечаю, что Лин, кажется, счастлив позволить мне опустить уровень вселенной Type в возвращаемом типе Rel выше, что приятно.

Answer 2

Стандартная библиотека Lean уже содержит определения различных порядков. Тем не менее, в то время как есть определения inf а также sup для реальных, я не думаю, что есть для ℚ, пока (или применимые общие определения, так как ни один из этих типов не является complete_lattice).