Zulip Chat Archive

Stream: maths

Topic: bounds


view this post on Zulip Kevin Buzzard (Nov 17 2018 at 11:23):

This is more of a funny story than anything else.

This week just gone at Imperial, we were looking at the real numbers and the completeness axiom in my class. Some of the students were involved in a (maths not Lean) project of constructing the real numbers as Dedekind cuts. The sheet started by defining totally ordered sets (the linear_order class in Lean) and the "least upper bound property" -- any non-empty bounded-above subset has a least upper bound. The sheet then remarked something I'd never realised -- there is no point defining also the "greatest lower bound property", because this follows from the least upper bound property. For the reals I had always imagined that this was proved by just considering {xxS}\{-x\,\mid\,x\in S\} but actually there is a direct proof which only uses total orders.

-- from order/bounds.lean

variables {α : Type*} [preorder α]
def upper_bounds (s : set α) : set α := { x | a  s, a  x }
def lower_bounds (s : set α) : set α := { x | a  s, x  a }
def is_least (s : set α) (a : α) : Prop := a  s  a  lower_bounds s
def is_greatest (s : set α) (a : α) : Prop := a  s  a  upper_bounds s
def is_lub (s : set α) : α  Prop := is_least (upper_bounds s)
def is_glb (s : set α) : α  Prop := is_greatest (lower_bounds s)

theorem warm_up (S : Type) [linear_order S] :
( E : set S, ( a, a  E)  ( b, b  upper_bounds E)   s : S, is_lub E s) 
( E : set S, ( a, a  E)  ( b, b  lower_bounds E)   s : S, is_glb E s) := sorry

Of course the proof requires a mathematical idea -- knowing any non-empty bounded-above set has a sup, and given a non-empty bounded-below set, we need to produce an inf without this involution which we have on the reals.

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 11:26):

So I could see what the idea must be, and knocked up a tactic proof without too much trouble.

And then because the bounds definitions applied not just to linear_order but to preorder, Chris asked whether my proof also worked for partial orders or preorders. So the question became -- what do you actually need to assume about your order to prove this warm-up question? I'll post our conclusions later on today if nobody else fancies trying to figure this out :-)

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 11:26):

No spoilers Kenny/Chris, if you're reading :-)

view this post on Zulip Johannes Hölzl (Nov 17 2018 at 11:58):

This is a standard construction at least for complete lattices, there often one defines the supremum or infimum and derives the other exterma. And these structures where the extrema only exists for non-empty bounded sets are called "conditionally complete lattices"

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 13:54):

Right. So the question is: you might well know already that if, in a lattice, all non-empty bounded-above sets have a sup, then all non-empty bounded-below sets have an inf. This is a pleasant exercise. The question is whether you can get away with less than a lattice.

view this post on Zulip Mario Carneiro (Nov 17 2018 at 13:59):

if every set has a least upper bound, then it's already a lattice

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 13:59):

I am only demanding on my order that every non-empty bounded above set has a least upper bound.

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:00):

then you get a conditionally complete lattice

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:00):

but I need enough from my order to be able to deduce from this that every non-empty bounded-below set has a greatest lower bound.

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:01):

You might have to be careful about how you say bounded below, but the usual proof should go through

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:01):

I explain exactly what I mean by all of these terms in the original post

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:01):

The question is how much you can relax the typeclasses and still be able to fill in the sorry

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:02):

e.g. can you prove

variables {α : Type*} [preorder α]
def upper_bounds (s : set α) : set α := { x | a  s, a  x }
def lower_bounds (s : set α) : set α := { x | a  s, x  a }
def is_least (s : set α) (a : α) : Prop := a  s  a  lower_bounds s
def is_greatest (s : set α) (a : α) : Prop := a  s  a  upper_bounds s
def is_lub (s : set α) : α  Prop := is_least (upper_bounds s)
def is_glb (s : set α) : α  Prop := is_greatest (lower_bounds s)

theorem warm_up (S : Type) [preorder S] :
( E : set S, ( a, a  E)  ( b, b  upper_bounds E)   s : S, is_lub E s) 
( E : set S, ( a, a  E)  ( b, b  lower_bounds E)   s : S, is_glb E s) := sorry

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:04):

I think so

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:04):

so now begin dropping the axioms of a preorder

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:05):

and how far can you get?

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:05):

if you take E := lower_bounds E then it's nonempty, and an element of E is an upper bound for lower_bounds E

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:05):

right. And which axioms for a preorder do you use in this proof?

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:06):

if a in E and b in lower_bounds E then b <= a so a is an upper bound of lower_bounds E

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:06):

it uses nothing

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:07):

variables {α : Type*} [has_le α]
def upper_bounds (s : set α) : set α := { x | a  s, a  x }
def lower_bounds (s : set α) : set α := { x | a  s, x  a }
def is_least (s : set α) (a : α) : Prop := a  s  a  lower_bounds s
def is_greatest (s : set α) (a : α) : Prop := a  s  a  upper_bounds s
def is_lub (s : set α) : α  Prop := is_least (upper_bounds s)
def is_glb (s : set α) : α  Prop := is_greatest (lower_bounds s)

theorem warm_up (S : Type) [has_le S] :
( E : set S, ( a, a  E)  ( b, b  upper_bounds E)   s : S, is_lub E s) 
( E : set S, ( a, a  E)  ( b, b  lower_bounds E)   s : S, is_glb E s) :=
λ H E ⟨⟨a, haE, b, hbuE⟩⟩,
let s, hs1, hs2 := H (lower_bounds E) ⟨⟨b, hbuE, a, λ s hs, hs a haE⟩⟩ in
s, λ t htE, hs2 t (λ z hzLE, hzLE t htE), hs1

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:07):

punchline achieved

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:07):

it could be any relation

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:07):

This made me wonder why preorder was assumed in bounds.lean

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:08):

because preorder is our weakest "lawful" order class

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:08):

surely has_le is weaker?

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:08):

It's surely an order class

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:08):

because of the notation

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:09):

you yourself know that has_add and has_mul are two completely different classes

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:09):

that's why you had to define groups twice

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:10):

if it's not a preorder, you probably shouldn't be using <=

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:11):

plus all the terminology there doesn't really make sense without some transitivity

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:29):

I am surprised that this is your attitude. I think the notation implies a "way of thinking" about the structure, but why can't I define the "upper bounds" of a set with has_le to be the obvious things? I thought that this was the mathlib philosophy -- you define things in the max generality that they parse, and for these definitions like upper_bounds we need nothing more than the predicate.

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:29):

Octonians aren't associative, and yet people still use * to multiply them

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:32):

octonions aren't completely lawless though

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:33):

If we cared about them we would define loops or power-associative monoids or whatever

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:35):

I think it helps to be at least a little application-driven here. If it's only ever used on preorders then why the suprious generalization?

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:35):

note also that typeclass inference is a bit longer for lower classes, although this is probably a small effect

view this post on Zulip Mario Carneiro (Nov 17 2018 at 14:36):

I would recommend using pure notation classes only in lawless situations like meta programming

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:49):

Oh that's an interesting comment. So there is a place for the has_lt typeclass beyond just a notational trick?

view this post on Zulip Kevin Buzzard (Nov 17 2018 at 14:49):

It's just in lawless metaland :-)

view this post on Zulip Kevin Buzzard (Mar 17 2019 at 17:10):

I think it helps to be at least a little application-driven here. If it's only ever used on preorders then why the suprious generalization?

In #789 I PR'ed monoid_equiv and Chris suggested I change it to mul_equiv. I want linear_ordered_comm_group_equiv but should this be extending le_equiv or preorder_equiv? Note the conversation above.

view this post on Zulip Kevin Buzzard (Mar 17 2019 at 17:11):

@Mario Carneiro . I just seem to be getting conflicting ideas about this one.


Last updated: May 12 2021 at 08:14 UTC