Zulip Chat Archive

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]?