Zulip Chat Archive

Stream: general

Topic: Knaster-Tarski


view this post on Zulip Kenny Lau (Mar 29 2018 at 04:43):

https://github.com/kckennylau/Lean/blob/master/Knaster-Tarski.lean
@Mario Carneiro por favor diz que nao fazias isso

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:44):

pooh favoh jeez ki now fazeeaish eesoo

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:44):

(that's how I pronounce it)

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:52):

@Kevin Buzzard if you're interested

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:52):

it's related to the link I pm'ed you

view this post on Zulip Mario Carneiro (Mar 29 2018 at 04:54):

Actually I'm a bit surprised it's not there

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:54):

bom!

view this post on Zulip Mario Carneiro (Mar 29 2018 at 04:55):

I'm certain there's something like it somewhere, but maybe it's not stated on complete lattices

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:55):

I thought it's a theorem of complete lattices

view this post on Zulip Mario Carneiro (Mar 29 2018 at 04:55):

There is a lfp function in ordinal with a similar proof attached

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:56):

nice

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:56):

that's the theorem about normal ordinal functions right

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:56):

does it have a name?

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:56):

maybe you can prove your lfp using this :D

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:56):

nvm it isn't a complete lattice

view this post on Zulip Mario Carneiro (Mar 29 2018 at 04:56):

is_normal.nfp_fp is what I was thinking of

view this post on Zulip Mario Carneiro (Mar 29 2018 at 04:57):

Dunno, it's not a complete lattice

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:57):

interesting

view this post on Zulip Mario Carneiro (Mar 29 2018 at 04:57):

Maybe that means there's a hidden abstraction?

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:57):

well to be fair

view this post on Zulip Mario Carneiro (Mar 29 2018 at 04:57):

like a sup-continuous monotone function

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:57):

your set is well-ordered

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:57):

hmm

view this post on Zulip Kenny Lau (Mar 29 2018 at 04:58):

but my function isn't sup-continuous

view this post on Zulip Mario Carneiro (Mar 29 2018 at 04:59):

Are you sure? Seems like it follows from the assumptions

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:00):

Anyway, I think this is why it isn't abstracted :)

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:00):

look at my aux 3

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:03):

Why do next and previous take an unused proof argument?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:05):

Wouldn't it be nicer to state aux3 for subsets of fixed_points f rather than sets in the subtype?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:05):

Then you could skip the subtype.val '' part

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:07):

then how can I use it

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:07):

Why do next and previous take an unused proof argument?

fixed

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:07):

For the big ol complete_lattice proof, I don't think that's the claim you want. Rather, fixed_points f is a complete sublattice of the powerset

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:08):

sublattice?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:08):

and then you have that construction generally for all sublattices

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:08):

I'm not aware of the existence of sublattices in Lean?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:09):

I don't think they exist

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:09):

But you could just skip the complete_lattice construction and just prove that the sup of fixed points is a fixed point

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:10):

Wouldn't it be nicer to state aux3 for subsets of fixed_points f rather than sets in the subtype?

nope, unprovable

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:11):

wait, misinterpreted

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:11):

But you could just skip the complete_lattice construction and just prove that the sup of fixed points is a fixed point

they aren't

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:11):

oh, I see, you need that next thing in the middle

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:12):

Hm, it's something like a retract from set A to fixed_points f

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:12):

It still strikes me as a generic construction

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:14):

https://github.com/kckennylau/Lean/blob/master/Knaster-Tarski.lean

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:15):

Wouldn't it be nicer to state aux3 for subsets of fixed_points f rather than sets in the subtype?

done. compare aux3 and aux4. aux4 has not been changed. which one is better?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:18):

Sup (f '' A) is also expressible as an indexed sup, ⨆ x ∈ A, f x

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:23):

oh

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:42):

@Mario Carneiro so what is the verdict?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:43):

I prefer aux3 since it is more likely to be used as a lemma

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:43):

and in general?

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:43):

do you find ways of abstracting Knaster-Tarski?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:44):

Not anything obvious

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:44):

and is it worth pushing?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:44):

I wonder if it works in conditionally complete lattices

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:44):

yes, PR it

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:44):

what is cc lattices?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:45):

@Johannes Hölzl should also weigh in, he's more involved in complete lattice theory than me

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:45):

real numbers, basically

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:45):

sup of nonempty bounded sets

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:45):

bot uses top, top uses bot

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:45):

?

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:45):

I think they can do without each other then

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:46):

the least fixed point is from the top element of the original lattice

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:46):

f(x)=x+1 has no fixed points

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:47):

sounds legit

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:47):

[0,infty) is downward complete right

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:48):

same example applies

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:52):

[0,1] is complete right

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:53):

yes

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:53):

hmm

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:53):

you don’t even need continuity

view this post on Zulip Mario Carneiro (Mar 29 2018 at 05:53):

wait, doesn't that imply banach's fp theorem in 1D?

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:53):

:open_mouth:

view this post on Zulip Kenny Lau (Mar 29 2018 at 05:54):

maths is beautiful

view this post on Zulip Kenny Lau (Mar 29 2018 at 06:13):

https://github.com/leanprover/mathlib/pull/88

view this post on Zulip Johannes Hölzl (Mar 29 2018 at 06:59):

There is already order/fixed_points.lean in mathlib. It contains lattice.lfp and lattice.gfp to compute the least and greatest fixed point of a function. For conditionally complete lattices: we could add a subtype instance for intervals on conditionally complete lattices. Then [0,1]:R[0, 1] : \mathbb{R} would be a complete lattice.

view this post on Zulip Kenny Lau (Mar 29 2018 at 07:01):

fair enough

view this post on Zulip Johannes Hölzl (Mar 29 2018 at 07:06):

Your next and previous function can be represented using the gfp and lfp: e.g. gfp (λz, x ⊔ f z) = Sup {z | z ≤ x ⊔ f z}. Then you can use the lfp and gfp properties.

view this post on Zulip Kenny Lau (Mar 29 2018 at 07:07):

so you're just going to close my PR?

view this post on Zulip Johannes Hölzl (Mar 29 2018 at 07:08):

No, I don't want to close it. I would like to see the fixed point lattice in order/fixed_points.lean. And using the constants and proofs we already have.

view this post on Zulip Kenny Lau (Mar 29 2018 at 07:08):

oh ok

view this post on Zulip Kenny Lau (Mar 29 2018 at 07:08):

are you going to edit it or am I going to edit it?

view this post on Zulip Johannes Hölzl (Mar 29 2018 at 07:10):

Of course, if you want you can edit it! I have a couple more changes: rename aux1..4 to something useful and replace is_ord_hom by the assumption monotone f, also going from type class to just assumption.

view this post on Zulip Kenny Lau (Mar 29 2018 at 08:43):

how would you rename aux1..4? @Johannes Hölzl

view this post on Zulip Johannes Hölzl (Mar 29 2018 at 08:48):

something like sup_le_f_sup_of_fixed_points?

view this post on Zulip Kenny Lau (Mar 29 2018 at 08:48):

ach fur gottesliebe

view this post on Zulip Kenny Lau (Mar 29 2018 at 08:49):

that's 10 times as long

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 08:49):

and more descriptive too ;-)

view this post on Zulip Kenny Lau (Mar 29 2018 at 08:50):

do you use f in names?

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 08:50):

Wait -- aren't you and I editing some schemes files with function names like structure_sheaf_of_rings_on_affine_scheme ?

view this post on Zulip Kenny Lau (Mar 29 2018 at 08:50):

my mind replaces f with apply in names

view this post on Zulip Kenny Lau (Mar 29 2018 at 08:50):

yes, and it's always you who type it :P

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 08:51):

definition structure_sheaf_of_rings_on_affine_scheme (R : Type*) [comm_ring R] : is_sheaf_of_rings (structure_presheaf_of_rings_on_affine_scheme R) :=... :-)

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 08:51):

well Mario told me I couldn't use tag00EJ...

view this post on Zulip Kenny Lau (Mar 29 2018 at 08:51):

I never typed it :P

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 08:51):

Perhaps tag00EJ is as bad as aux1 right? ;-)

view this post on Zulip Kenny Lau (Mar 29 2018 at 08:52):

right


Last updated: May 13 2021 at 00:41 UTC