Я хочу доказать this theorem в теореме Lean. Во-первых, мне нужно определить такие вещи, как частично упорядоченные множества, чтобы я мог определить infimum/supremum. Как это делается в Lean? The tutorial упоминает setoids, которые являются типами с отношением эквивалентности . Но мне непонятно, как это могло бы помочь.Как определить частично упорядоченные множества в Lean?
Я не пользователь Lean, но вот как бы я определил его в Agda. Он может не переводить напрямую - в теориях типов много разнообразия - но это должно быть хотя бы указатель!
Мы будем работать с двоичными логическими отношениями, которые являются жителями этого типа синонима:
Rel : Set -> Set1
Rel A = A -> A -> Set
И мы должны будем пропозициональное равенство:
data _==_ {A : Set} (x : A) : A -> Set where
refl : x == x
Можно сказать, что это значит для логического отношения - reflexive, antisymmetric и 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, совершенные нагрузки синтаксических ошибок и, в конечном итоге, достигли этого (возможно, не идиоматического, но простого) перевода. Функции становятся definition s и record s становятся structure s.
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)
Я использую built-in versions определений для рефлексивности (и т.д.), которые я определил себя в Agda выше. Я также замечаю, что Lean, похоже, счастлив позволить мне опустить уровень вселенной Type в обратном типе Rel выше, что приятно.
Спасибо за ваш ответ! Как утверждать, что у одного из этих Posets есть подмножество? 'определение UpperBound {A: Тип} {P: Rel A}: = принять K: Poset A P, принять S: Poset A P, предположим, что S ⊂ K,' не работает. Я предполагаю, что мне нужно определить оператор подмножества, я думаю, он должен быть оператором инфикса, который принимает один набор, и один Poset, и утверждает, что все элементы набора находятся в Poset. Но как я утверждаю, что что-то находится в Poset?'take x: A, Предположим, что x ∈ K,' тоже не работает ... –
Возможно, это требует отдельных вопросов. Одним из хороших способов определения подмножества является логический предикат типа «Pred A = A -> Set». Чтобы определить членство, любое 'x: A' является доказательством того, что' A' не пусто. –
Стандартная библиотека Lean уже содержит определения various orders. Однако в то время как there are определения inf и sup для реалов, я не думаю, что они есть для ℚ, но (или применимые общие определения, поскольку ни один из этих типов не является complete_lattice).
Кстати, как вы планируете определять реальные цифры? –