Zulip Chat Archive

Stream: maths

Topic: Constructing a complete lattice


view this post on Zulip Heather Macbeth (Oct 31 2020 at 20:57):

Can someone explain this docstring to me?
https://github.com/leanprover-community/mathlib/blob/be161d119ac3ee06db86b7429201e4ea281e13f2/src/order/complete_lattice.lean#L71

/-- Create a `complete_lattice` from a `partial_order` and `Inf` function
that returns the greatest lower bound of a set. Usually this constructor provides
poor definitional equalities, so it should be used with
`.. complete_lattice_of_Inf α _`. -/
def complete_lattice_of_Inf (α : Type*) [H1 : partial_order α]
  [H2 : has_Inf α] (is_glb_Inf :  s : set α, is_glb s (Inf s)) :
  complete_lattice α :=

Context: I want to make a complete lattice. There's already a partial order structure, and I can easily write down what the has_Sup and has_Inf instances are. Will it cause definitional problems if I simply pick one of these, say the has_Inf, and then use complete_lattice_of_Inf to make the complete lattice structure?

view this post on Zulip Mario Carneiro (Oct 31 2020 at 20:58):

It means that the has_Sup instance will not be the one you would otherwise have written down

view this post on Zulip Mario Carneiro (Oct 31 2020 at 20:58):

as well as sup and inf and top and bot

view this post on Zulip Mario Carneiro (Oct 31 2020 at 20:59):

However, there is complete_lattice.copy that you can use to edit these fields after constructing most of the structure using complete_lattice_of_Inf

view this post on Zulip Heather Macbeth (Oct 31 2020 at 21:00):

Is it bad to take (eg) the inf that comes from this definition, which is inf := λ a b, Inf {a, b}? Isn't that the same as what I would write down by hand?

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:01):

It seems unlikely that this is what you would write down in any concrete instance unless you had nothing other than Inf to work with

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:01):

for instance the inf for set is \cap which is not the same as \bigcap {x, y}

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:02):

I mean if you don't have any particular reason to care what the values are it's fine to just let it be

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:03):

but if you ever unfold it and end up with something weird you might consider changing the definition to something more sensible

view this post on Zulip Heather Macbeth (Oct 31 2020 at 21:03):

OK, thanks!

view this post on Zulip Heather Macbeth (Oct 31 2020 at 21:04):

What does "it should be used with .. complete_lattice_of_Inf α _." mean, in particular? (From the docstring I quoted above.)

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:06):

It's suggesting that you write

instance : complete_lattice my_T :=
{ inf := better_inf,
  sup := better_sup,
  -- don't care to fix Sup, bot, top
  ..complete_lattice_of_Inf my_T _ }

which is equivalent to my suggestion of using complete_lattice.copy better_inf <proof> Sup rfl (complete_lattice_of_Inf my_T _)

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:08):

to take a random example, src#subfield.complete_lattice

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:08):

notice that top and inf are overridden but bot and sup are not because there isn't any much better expression for the sup of subfields

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:09):

but it's definitely nice to have the inf of subfields be defeq to the binary intersection

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:10):

so that you can use <hK, hL> to construct and destruct proofs of x \in K \inf L

view this post on Zulip Heather Macbeth (Oct 31 2020 at 21:11):

I see! So when you do it this way, it is overwriting selected fields. Does it require some kind of compatibility proof of the old fields with the new fields? Eg, do I need to overwrite le_inf too?

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:12):

You do if the new expression is not defeq to the old one (which is usually the case because otherwise there isn't much need to override)

view this post on Zulip Mario Carneiro (Oct 31 2020 at 21:13):

complete_lattice.copy requires you prove the new field is equal to the old one, while using {inf := new_inf, ..} requires proving the new inf also satisfies the inf axioms

view this post on Zulip Heather Macbeth (Oct 31 2020 at 21:15):

I see. Thanks. I think for my WIP code I'll do it the lazy way, and change it field by field if I find myself using them. When I PR I'll do it the right way ....

view this post on Zulip Bryan Gin-ge Chen (Oct 31 2020 at 21:53):

I agree that this docstring is obscure. It'd be great if we added some of the info from the conversation above to it.

view this post on Zulip Heather Macbeth (Oct 31 2020 at 22:20):

#4859

view this post on Zulip Aaron Anderson (Nov 01 2020 at 02:41):

(deleted)


Last updated: May 09 2021 at 10:11 UTC