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

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


set dependent-type theorem-proving lean
person Janus Troelsen    schedule 27.03.2016    source источник
comment
Кстати, а как вы планируете определять действительные числа?   -  person Benjamin Hodgson♦    schedule 03.04.2016

Ответы (2)


arrow_upward
5
arrow_downward

Я не использую 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 _<=_

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

person Benjamin Hodgson♦    schedule 01.04.2016
comment
Спасибо за ваш ответ! Как я могу утверждать, что у одного из этих Poset есть подмножество? definition UpperBound {A:Type}{P : Rel A} := take K : Poset A P, take S : Poset A P, assume S ⊂ K, не работает. Я предполагаю, что мне нужно определить оператор подмножества, я думаю, это должен быть инфиксный оператор, который принимает один набор и один Poset и утверждает, что все элементы набора находятся в Poset. Но как я могу утверждать, что что-то есть в Poset? take x : A, assume x ∈ K, тоже не работает ... - person Janus Troelsen; 05.04.2016
comment
Возможно, это оправдывает отдельные вопросы. Хороший способ определения подмножества - использование логического предиката типа Pred A = A -> Set. Чтобы определить членство, любое x : A является доказательством того, что A не пусто. - person Benjamin Hodgson♦; 06.04.2016

arrow_upward
1
arrow_downward

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

person Sebastian Ullrich    schedule 02.04.2016