Zulip Chat Archive

Stream: new members

Topic: opposite preorder


view this post on Zulip 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?

view this post on Zulip Reid Barton (Aug 03 2020 at 01:02):

it's called docs#order_dual in mathlib

view this post on Zulip Adam Topaz (Aug 03 2020 at 01:13):

Oooh should this be a job for docs#opposite ?

view this post on Zulip Reid Barton (Aug 03 2020 at 01:15):

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

view this post on Zulip Adam Topaz (Aug 03 2020 at 01:15):

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

view this post on Zulip Adam Topaz (Aug 03 2020 at 01:18):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 03 2020 at 18:16):

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

view this post on Zulip Jalex Stark (Aug 03 2020 at 18:19):

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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Aug 03 2020 at 18:30):

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

view this post on Zulip Iocta (Aug 03 2020 at 18:31):

 p  ?m_1  set X : Type

apparently

view this post on Zulip 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?

view this post on Zulip Jalex Stark (Aug 03 2020 at 18:36):

it's a function of one argument

view this post on Zulip Jalex Stark (Aug 03 2020 at 18:36):

so you can just pass in the argument

view this post on Zulip Jalex Stark (Aug 03 2020 at 18:36):

as in uparrow X p hp

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 03 2020 at 18:40):

Check the type of is_upper...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Iocta (Aug 03 2020 at 19:23):

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

view this post on Zulip Adam Topaz (Aug 03 2020 at 19:24):

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

view this post on Zulip 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!

view this post on Zulip Iocta (Aug 03 2020 at 19:26):

oh I see, they're at different levels

view this post on Zulip 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/

view this post on Zulip Iocta (Aug 03 2020 at 19:26):

yeah, just realized that

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 19:28):

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

view this post on Zulip 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"

view this post on Zulip 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]?

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 20:01):

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

view this post on Zulip 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

view this post on Zulip Iocta (Aug 03 2020 at 20:08):

which Reid said above is order_dual

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 20:08):

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

view this post on Zulip Reid Barton (Aug 03 2020 at 20:08):

I would just get rid of P (or X)

view this post on Zulip Reid Barton (Aug 03 2020 at 20:09):

er, wait

view this post on Zulip Reid Barton (Aug 03 2020 at 20:09):

I now agree with Kevin

view this post on Zulip Iocta (Aug 03 2020 at 20:09):

haha :-)

view this post on Zulip Reid Barton (Aug 03 2020 at 20:10):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 20:17):

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

view this post on Zulip Iocta (Aug 03 2020 at 20:19):

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

view this post on Zulip Kevin Buzzard (Aug 03 2020 at 20:20):

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

view this post on Zulip Iocta (Aug 03 2020 at 20:23):

oh. I see


Last updated: May 11 2021 at 23:11 UTC