How do I define partially ordered sets in Lean?

I wish to prove 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 mentions setoids, which are types with an associated equivalence relation. But it is not clear to me how this could help.

Solution

I'm not a Lean user, but here's how I'd define it in Agda. It may not translate directly - there's a lot of variety in type theories - but it should at least be a pointer!

We'll be working with binary logical relations, which are inhabitants of this type synonym:

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

And we'll need propositional equality:

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

One can say what it means for a logical relation to be 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

To be a partial order, it must be all three.

record IsPartialOrder {A : Set} (_<=_ : Rel A) : Set where
  field
    reflexive : Refl _<=_
    antisymmetric : Antisym _<=_
    transitive : Trans _<=_

A poset is just a set equipped with a partial ordering relation.

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

For the record (ha ha), here is how the setoid example from the tutorial translates into 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: I installed Lean, committed a load of syntax errors, and eventually arrived at this (probably not idiomatic, but straightforward) translation. Functions become definitions and records become 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)

I'm using the built-in versions of the definitions for reflexivity (etc) that I defined myself in Agda above. I also notice that Lean seems happy to let me omit the universe level of Type in the return type of Rel above, which is a nice touch.