Constructing a complete lattice

Stream: maths

[Heather Macbeth]

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?

[Mario Carneiro]

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

[Mario Carneiro]

as well as sup and inf and top and bot

[Mario Carneiro]

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

[Heather Macbeth]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Heather Macbeth]

OK, thanks!

[Heather Macbeth]

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

[Mario Carneiro]

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 _)

[Mario Carneiro]

to take a random example, src#subfield.complete_lattice

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Heather Macbeth]

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?

[Mario Carneiro]

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)

[Mario Carneiro]

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

[Heather Macbeth]

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 ....

[Bryan Gin-ge Chen]

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

[Heather Macbeth]

#4859

[Aaron Anderson]

(deleted)