Zulip Chat Archive

Stream: general

Topic: Knaster-Tarski

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

Kenny Lau (Mar 29 2018 at 04:44):

pooh favoh jeez ki now fazeeaish eesoo

Kenny Lau (Mar 29 2018 at 04:44):

(that's how I pronounce it)

Kenny Lau (Mar 29 2018 at 04:52):

@Kevin Buzzard if you're interested

Kenny Lau (Mar 29 2018 at 04:52):

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

Mario Carneiro (Mar 29 2018 at 04:54):

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

Kenny Lau (Mar 29 2018 at 04:54):

bom!

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

Kenny Lau (Mar 29 2018 at 04:55):

I thought it's a theorem of complete lattices

Mario Carneiro (Mar 29 2018 at 04:55):

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

Kenny Lau (Mar 29 2018 at 04:56):

nice

Kenny Lau (Mar 29 2018 at 04:56):

that's the theorem about normal ordinal functions right

Kenny Lau (Mar 29 2018 at 04:56):

does it have a name?

Kenny Lau (Mar 29 2018 at 04:56):

maybe you can prove your lfp using this :D

Kenny Lau (Mar 29 2018 at 04:56):

nvm it isn't a complete lattice

Mario Carneiro (Mar 29 2018 at 04:56):

is_normal.nfp_fp is what I was thinking of

Mario Carneiro (Mar 29 2018 at 04:57):

Dunno, it's not a complete lattice

Kenny Lau (Mar 29 2018 at 04:57):

interesting

Mario Carneiro (Mar 29 2018 at 04:57):

Maybe that means there's a hidden abstraction?

Kenny Lau (Mar 29 2018 at 04:57):

well to be fair

Mario Carneiro (Mar 29 2018 at 04:57):

like a sup-continuous monotone function

Kenny Lau (Mar 29 2018 at 04:57):

your set is well-ordered

Kenny Lau (Mar 29 2018 at 04:57):

hmm

Kenny Lau (Mar 29 2018 at 04:58):

but my function isn't sup-continuous

Mario Carneiro (Mar 29 2018 at 04:59):

Are you sure? Seems like it follows from the assumptions

Mario Carneiro (Mar 29 2018 at 05:00):

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

Kenny Lau (Mar 29 2018 at 05:00):

look at my aux 3

Mario Carneiro (Mar 29 2018 at 05:03):

Why do next and previous take an unused proof argument?

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?

Mario Carneiro (Mar 29 2018 at 05:05):

Then you could skip the subtype.val '' part

Kenny Lau (Mar 29 2018 at 05:07):

then how can I use it

Kenny Lau (Mar 29 2018 at 05:07):

Why do next and previous take an unused proof argument?

fixed

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

Kenny Lau (Mar 29 2018 at 05:08):

sublattice?

Mario Carneiro (Mar 29 2018 at 05:08):

and then you have that construction generally for all sublattices

Kenny Lau (Mar 29 2018 at 05:08):

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

Mario Carneiro (Mar 29 2018 at 05:09):

I don't think they exist

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

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

Kenny Lau (Mar 29 2018 at 05:11):

wait, misinterpreted

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

Mario Carneiro (Mar 29 2018 at 05:11):

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

Mario Carneiro (Mar 29 2018 at 05:12):

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

Mario Carneiro (Mar 29 2018 at 05:12):

It still strikes me as a generic construction

Kenny Lau (Mar 29 2018 at 05:14):

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

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?

Mario Carneiro (Mar 29 2018 at 05:18):

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

Kenny Lau (Mar 29 2018 at 05:23):

oh

Kenny Lau (Mar 29 2018 at 05:42):

@Mario Carneiro so what is the verdict?

Mario Carneiro (Mar 29 2018 at 05:43):

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

Kenny Lau (Mar 29 2018 at 05:43):

and in general?

Kenny Lau (Mar 29 2018 at 05:43):

do you find ways of abstracting Knaster-Tarski?

Mario Carneiro (Mar 29 2018 at 05:44):

Not anything obvious

Kenny Lau (Mar 29 2018 at 05:44):

and is it worth pushing?

Mario Carneiro (Mar 29 2018 at 05:44):

I wonder if it works in conditionally complete lattices

Mario Carneiro (Mar 29 2018 at 05:44):

yes, PR it

Kenny Lau (Mar 29 2018 at 05:44):

what is cc lattices?

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

Mario Carneiro (Mar 29 2018 at 05:45):

real numbers, basically

Mario Carneiro (Mar 29 2018 at 05:45):

sup of nonempty bounded sets

Kenny Lau (Mar 29 2018 at 05:45):

bot uses top, top uses bot

Mario Carneiro (Mar 29 2018 at 05:45):

?

Kenny Lau (Mar 29 2018 at 05:45):

I think they can do without each other then

Kenny Lau (Mar 29 2018 at 05:46):

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

Kenny Lau (Mar 29 2018 at 05:46):

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

Mario Carneiro (Mar 29 2018 at 05:47):

sounds legit

Kenny Lau (Mar 29 2018 at 05:47):

[0,infty) is downward complete right

Kenny Lau (Mar 29 2018 at 05:48):

same example applies

Kenny Lau (Mar 29 2018 at 05:52):

[0,1] is complete right

Mario Carneiro (Mar 29 2018 at 05:53):

yes

Kenny Lau (Mar 29 2018 at 05:53):

hmm

Kenny Lau (Mar 29 2018 at 05:53):

you don’t even need continuity

Mario Carneiro (Mar 29 2018 at 05:53):

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

Kenny Lau (Mar 29 2018 at 05:53):

:open_mouth:

Kenny Lau (Mar 29 2018 at 05:54):

maths is beautiful

Kenny Lau (Mar 29 2018 at 06:13):

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

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] : \mathbb{R}$ would be a complete lattice.

Kenny Lau (Mar 29 2018 at 07:01):

fair enough

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.

Kenny Lau (Mar 29 2018 at 07:07):

so you're just going to close my PR?

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.

Kenny Lau (Mar 29 2018 at 07:08):

oh ok

Kenny Lau (Mar 29 2018 at 07:08):

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

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.

Kenny Lau (Mar 29 2018 at 08:43):

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

Johannes Hölzl (Mar 29 2018 at 08:48):

something like sup_le_f_sup_of_fixed_points?

Kenny Lau (Mar 29 2018 at 08:48):

ach fur gottesliebe

Kenny Lau (Mar 29 2018 at 08:49):

that's 10 times as long

Kevin Buzzard (Mar 29 2018 at 08:49):

and more descriptive too ;-)

Kenny Lau (Mar 29 2018 at 08:50):

do you use f in names?

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 ?

Kenny Lau (Mar 29 2018 at 08:50):

my mind replaces f with apply in names

Kenny Lau (Mar 29 2018 at 08:50):

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

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) :=... :-)

Kevin Buzzard (Mar 29 2018 at 08:51):

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

Kenny Lau (Mar 29 2018 at 08:51):

I never typed it :P

Kevin Buzzard (Mar 29 2018 at 08:51):

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

Kenny Lau (Mar 29 2018 at 08:52):

right

Last updated: Dec 20 2023 at 11:08 UTC