## Stream: new members

### Topic: opposite preorder

#### Iocta (Aug 03 2020 at 00:59):

I am learning about preorders, and I read there is a concept called "opposite preorder", which is, Given a preorder (P, <=), the opposite is a preorder (P, <=op) having p <=op q iff q <= p. I am wondering how to write this in lean. I found preorders in lean. Is that definition suitable for defining 'opposite preorder' with? How to do that?

#### Reid Barton (Aug 03 2020 at 01:02):

it's called docs#order_dual in mathlib

#### Adam Topaz (Aug 03 2020 at 01:13):

Oooh should this be a job for docs#opposite ?

#### Reid Barton (Aug 03 2020 at 01:15):

opposite is already sort of conceptually dubious but it definitely shouldn't reverse both <= and *

#### Adam Topaz (Aug 03 2020 at 01:15):

Oh yeah fair enough. Didn't consider the case of an ordered ring.

#### Adam Topaz (Aug 03 2020 at 01:18):

Well... If you think of a poset as a category, then opposite does make sense.

#### Yury G. Kudryashov (Aug 03 2020 at 03:23):

Possibly we should split opposite in category theory and in group theory and turn ᵒᵖ into two localized notations.

#### Iocta (Aug 03 2020 at 18:08):

A couple questions

import data.set.basic
import data.set.lattice
import data.setoid.partition
import order.filter.basic
import tactic.basic
import tactic
import init.logic init.classical init.meta.name init.algebra.classes

variable X : Type
variable s : set X
variable {P : set X}

-- XXX Don't I mean [preorder P], not [preorder X]?
def is_upper [preorder X] (P: set X) : Prop :=
∀ p ∈ P, ∀ (q : X), q ≥ p → q ∈ P

def uparrow [preorder X] (p : X) (hp: p ∈ P) : set X :=
{p' ∈ P | p ≤ p'}

-- XXX Why doesn't this work?
example [preorder X] (p : X) : ∀ p ∈ P, is_upper (uparrow p) := sorry

failed to synthesize type class instance for
X : Type,
P : set X,
_inst_1 : preorder X,
p : X,
p : Type
⊢ has_mem Type (set X)
cats.lean:23:50
failed to synthesize type class instance for
X : Type,
P : set X,
_inst_1 : preorder X,
p : X,
p : Type,
H : p ∈ P
⊢ preorder p


#### Reid Barton (Aug 03 2020 at 18:16):

Check the type of uparrow. It has more explicit arguments than you seem to think

#### Jalex Stark (Aug 03 2020 at 18:19):

it might help you to squash your three variable statements into one variables statement

#### Iocta (Aug 03 2020 at 18:29):

uparrow : Π (X : Type) {P : set X} [_inst_1 : preorder X] (p : X), p ∈ P → set X


has two of (these) so I think it needs two arguments
but

example [preorder X] (p : X) : ∀ p ∈ P, is_upper (uparrow X p) := sorry
type mismatch at application
is_upper (uparrow X p)
term
uparrow X p
has type
p ∈ ?m_1 → set X : Type
but is expected to have type
Type : Type 1


#### Jalex Stark (Aug 03 2020 at 18:30):

do you know what the type of uparrow X p is?

#### Iocta (Aug 03 2020 at 18:31):

 p ∈ ?m_1 → set X : Type


apparently

#### Iocta (Aug 03 2020 at 18:34):

does that mean I'm supposed to change it from forall to introducing a specific hp : p \in P so I can reference it by name?

#### Jalex Stark (Aug 03 2020 at 18:36):

it's a function of one argument

#### Jalex Stark (Aug 03 2020 at 18:36):

so you can just pass in the argument

#### Jalex Stark (Aug 03 2020 at 18:36):

as in uparrow X p hp

#### Kevin Buzzard (Aug 03 2020 at 18:37):

@Iocta :

uparrow : Π (X : Type) {P : set X} [_inst_1 : preorder X] (p : X), p ∈ P → set X


is exactly the same as

uparrow : Π (X : Type) {P : set X} [_inst_1 : preorder X] (p : X) (hp : p ∈ P), set X


#### Iocta (Aug 03 2020 at 18:39):

Sorry if I'm being dense, I don't know what this means:

example [preorder X] (p : X) (hp: p ∈ P) : is_upper (uparrow X p hp) := sorry
type expected at
is_upper ↥(uparrow X p hp)
term has type
set ↥(uparrow X p hp) → Prop


#### Reid Barton (Aug 03 2020 at 18:40):

Check the type of is_upper...

#### Kevin Buzzard (Aug 03 2020 at 18:48):

@Iocta Lean is just using logic here, and you can use logic too to figure out exactly which inputs each function wants, and the error messages explain when you have not given each function the right inputs.

#### Kevin Buzzard (Aug 03 2020 at 18:49):

Hovering over the name of a function will tell you exactly what the inputs it wants are

#### Iocta (Aug 03 2020 at 19:22):

variables [preorder X] (p : X) (hp: p ∈ P) (S: uparrow p hp)
-- Why can I say this
example [preorder X] : is_upper (uparrow p hp) := sorry
-- but not this?
example [preorder X] : is_upper S := sorry


#### Iocta (Aug 03 2020 at 19:23):

type mismatch at application
is_upper S
term
S
has type
↥(uparrow p hp)
but is expected to have type
set ?m_1


#### Iocta (Aug 03 2020 at 19:23):

isn't ↥(uparrow p hp) a set?

#### Adam Topaz (Aug 03 2020 at 19:24):

The strange arrow means subtype. It's the subtype associated to the set uparrow _ _.

#### Reid Barton (Aug 03 2020 at 19:25):

whatever else is happening, if is_upper (uparrow p hp) makes sense and S : uparrow p hp, then surely is_upper S will almost never make sense!

#### Iocta (Aug 03 2020 at 19:26):

oh I see, they're at different levels

#### Kevin Buzzard (Aug 03 2020 at 19:26):

@Iocta do you know the difference between a type and a term? https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/

#### Iocta (Aug 03 2020 at 19:26):

yeah, just realized that

#### Kevin Buzzard (Aug 03 2020 at 19:26):

In Lean, if X : Type then X is a type, but if A : set X then A is a term, not a type.

#### Kevin Buzzard (Aug 03 2020 at 19:27):

So even though we might informally think of X as a "set" and A as a "subset" and hence a "set", they are at different levels as you say.

#### Kevin Buzzard (Aug 03 2020 at 19:27):

The weird arrow promotes a term to a type, in the cases when this can be done

#### Kevin Buzzard (Aug 03 2020 at 19:28):

e.g it would promote A : set X to a type called a subtype; to give a term of this subtype you have to give a pair consisting of x : X and then a proof that x \in A.

#### Kevin Buzzard (Aug 03 2020 at 19:28):

But a random term can't be promoted to a type

#### Iocta (Aug 03 2020 at 19:33):

example [preorder X] : is_upper (uparrow p hp) := sorry
example [preorder X] : ∀ p ∈ P, is_upper (uparrow p H) := sorry


that H is what i was looking for before "does that mean I'm supposed to change it from forall to introducing a specific hp : p \in P so I can reference it by name"

#### Iocta (Aug 03 2020 at 19:54):

Currently X has_le, but I think I mean for P to has_le instead, since the whole point of the exercise is that the ordering of Xs is flexible. Therefore do I want to make P a subtype of X that has_leinstead of a set X, so then I can say [preorder P]?

#### Kevin Buzzard (Aug 03 2020 at 20:01):

I don't know what you want because I don't know what you're doing

#### Iocta (Aug 03 2020 at 20:07):

I want to talk about "the opposite preorder of P": Given a preorder (P, <=), the opposite is a preorder (P, <=op) having p <=op q iff q <= p

#### Iocta (Aug 03 2020 at 20:08):

which Reid said above is order_dual

#### Kevin Buzzard (Aug 03 2020 at 20:08):

https://github.com/leanprover-community/mathlib/blob/c6381aa1175c78083b91732aebefb793156a656a/src/order/basic.lean#L219

#### Reid Barton (Aug 03 2020 at 20:08):

I would just get rid of P (or X)

er, wait

#### Reid Barton (Aug 03 2020 at 20:09):

I now agree with Kevin

haha :-)

#### Reid Barton (Aug 03 2020 at 20:10):

is_upper looks sensible, but why is there a P in uparrow?

#### Kevin Buzzard (Aug 03 2020 at 20:10):

The preorder instance on the dual is https://github.com/leanprover-community/mathlib/blob/c6381aa1175c78083b91732aebefb793156a656a/src/order/basic.lean#L235-L240

#### Iocta (Aug 03 2020 at 20:16):

I was trying to express "P := (X, <=) is a preorder" but maybe that's pointless and I should just say X is orderable in the first place

#### Kevin Buzzard (Aug 03 2020 at 20:17):

P : set X means P is a subset of X, not P=X as a set

#### Iocta (Aug 03 2020 at 20:19):

I get that part; I'll just skip P as suggested

#### Kevin Buzzard (Aug 03 2020 at 20:20):

[preorder X] means "(X,<=) is a preorder"

#### Iocta (Aug 03 2020 at 20:23):

oh. I see

Last updated: May 11 2021 at 23:11 UTC