Where is sSup defined on submodules?

Stream: new members

[Kevin Buzzard]

Lean does not do magic, but I can't figure out how it's doing this. In Mathlib.Algebra.Module.Submodule.Lattice we have docs#Submodule.completeLattice which defines a complete lattice structure on the submodules of a module over a (semi)ring. I was asked at Xena where the sSup field is coming from. I cannot figure it out and all the smart people already left for dinner :-/ The declaration in the mathlib file is

instance completeLattice : CompleteLattice (Submodule R M) :=
  { (inferInstance : OrderTop (Submodule R M)),
    (inferInstance : OrderBot (Submodule R M)) with
    sup := fun a b ↦ sInf { x | a ≤ x ∧ b ≤ x }
    le_sup_left := fun _ _ ↦ le_sInf' fun _ ⟨h, _⟩ ↦ h
    le_sup_right := fun _ _ ↦ le_sInf' fun _ ⟨_, h⟩ ↦ h
    sup_le := fun _ _ _ h₁ h₂ ↦ sInf_le' ⟨h₁, h₂⟩
    inf := (· ⊓ ·)
    le_inf := fun _ _ _ ↦ Set.subset_inter
    inf_le_left := fun _ _ ↦ Set.inter_subset_left
    inf_le_right := fun _ _ ↦ Set.inter_subset_right
    le_sSup := fun _ _ hs ↦ le_sInf' fun _ hq ↦ by exact hq _ hs
    sSup_le := fun _ _ hs ↦ sInf_le' hs
    le_sInf := fun _ _ ↦ le_sInf'
    sInf_le := fun _ _ ↦ sInf_le' }

Before this instance, sSup doesn't work on sets of submodules. Afterwards, it does. But neither OrderTop nor OrderBot supply it and it's not in the list of explicit fields either. I know the trick mathematically -- I can even see it in #print completeLattice -- there is a sInf defined by this point on submodules (before the completeLattice instance), and the sSup of S is just the sInf of all the submodules which contain every element of S. But where in mathlib is this code and why is it running?

[Edward van de Meent]

i think this might be unification at work?

[Riccardo Brasca]

There is Submodule.instInfSet that seems relevant

[Edward van de Meent]

commenting out the last four fields and replacing them with sorry seems to make it complain it doesn't know what sSup is

[Edward van de Meent]

specifically, it looks like the value of the sSup_le field is what allows it to infer the value of sSup?

[Edward van de Meent]

i do agree, this behaviour seems quite magical

[Etienne Marion]

I agree with Edward, sSup_le (and le_sSup also works) allow to infer the definition of sSup. This seems to rely on the Set _ vs _ → Prop definitional equality so that the hypothesis hs is interpreted as a belonging to the set of submodules containing all elements of s without making this set explicit, via sInf_le'.

[Edward van de Meent]

actually, replacing sSup_le with sorry makes the le_sSup field error, so i'm not sure that it also works?

[Edward van de Meent]

it will complain that it doesn't know hq : x✝ ∈ ?m.39162 x✝² is a function. It is after lean is able to fill in the metavariable (because membership of an intersection is defeq to a forall statement), but not before.

[Etienne Marion]

You’re right my bad

[Riccardo Brasca]

Indeed one can do

instance completeLattice : CompleteLattice (Submodule R M) :=
  { (inferInstance : OrderTop (Submodule R M)),
    (inferInstance : OrderBot (Submodule R M)) with
    sup := fun a b ↦ sInf { x | a ≤ x ∧ b ≤ x }
    le_sup_left := fun _ _ ↦ le_sInf' fun _ ⟨h, _⟩ ↦ h
    le_sup_right := fun _ _ ↦ le_sInf' fun _ ⟨_, h⟩ ↦ h
    sup_le := fun _ _ _ h₁ h₂ ↦ sInf_le' ⟨h₁, h₂⟩
    inf := (· ⊓ ·)
    le_inf := fun _ _ _ ↦ Set.subset_inter
    inf_le_left := fun _ _ ↦ Set.inter_subset_left
    inf_le_right := fun _ _ ↦ Set.inter_subset_right
    le_sSup := fun _ _ hs ↦ le_top --note the new proof
    sSup_le := sorry
    le_sInf := fun _ _ ↦ le_sInf'
    sInf_le := fun _ _ ↦ sInf_le' }

example {R M : Type} [CommRing R] [AddCommGroup M] [Module R M] (S : Set (Submodule R M)) :
  sSup S = ⊤ := rfl

[Edward van de Meent]

right, so it does try to unify at le_sSup, but the "correct" value only allows unification after sSup_le is unified

[Anatole Dedecker]

In any case, I think we would be very happy with a PR actually adding the definition...

[Riccardo Brasca]

Yes, I even think a linter saying something would be a good thing. Maybe forcing to write at least sSup := _ (that works just fine), to flag that this is find by unification (maybe the actual definition is very long and it can be useful to not write it explicitly). Not writing anything just seems confusing.

[Edward van de Meent]

#21850 adds an explicit value to the field

[Kevin Buzzard]

Wait so what is going on here? Can I not define le when making a partial order as long as one of the proofs makes it clear what it must be? Is this a general phenomenon? I had no idea that you could just randomly skip fields and that unification would attempt to fill them in

[Junyan Xu]

The { ..., sup := ... } is probably just a syntax sugar for an application of the function CompleteLattice.mk, so you can omit some fields just like you can use underscores for some arguments if they can be inferred.

[Kevin Buzzard]

Yes but IIRC docs#CompleteLattice.mk asks for SupSet to be found via typeclass inference which was what confused me (edit: I'm not at Lean right now and the docs won't let me check this)

[Riccardo Brasca]

What I find confusing in this example is that Lean infers data from a proof. I understand why this works, but it goes against the slogan "proofs don't matter", and it looks to me code smell.

[Kevin Buzzard]

Looks like it's fixed now though :-)

[Kevin Buzzard]

I would say I still don't understand why it works. I am amazed that unification is allowed at all in this setting

[Riccardo Brasca]

It's like

theorem foo (a : Nat) (ha : a + 0 = a) : a = 37 := by sorry

example : False := by
  have := foo _ (Nat.add_zero 55)
  sorry

[Riccardo Brasca]

Since Nat.add_zero 55 proves 55+0=55 Lean understands that the have is 55 = 37.

[Kevin Buzzard]

But where is the underscore in the sSup example? For me it's the underscore which means "use unification". All I could find was "use typeclass inference". If you leave out the definition of a field of a structure lean doesn't use unification to fill it in AFAIK, it gives an error (is this where I'm wrong?)

[Riccardo Brasca]

Ah yes, that is some magic in the where syntax. My proposal is indeed to at least force people to write sSup := _ to make it clear that it is found by unification

[Kevin Buzzard]

I'm not sure what you're proposing to change here: Just to be clear, master now has the field filled in.

The experiment I want to do: make a structure with two fields: a nat and a proof it's 37. Then instantiate the structure by giving the proof as rfl but not giving the nat at all. Does this work?

[Riccardo Brasca]

Yes, this specific example is fixed. I would like the previous syntax to give an error

[Riccardo Brasca]

Going to teach now

[Yaël Dillies]

Kevin Buzzard said:

The experiment I want to do: make a structure with two fields: a nat and a proof it's 37. Then instantiate the structure by giving the proof as rfl but not giving the nat at all. Does this work?

Yes it does. I use this trick all the time to fill in the default arguments to docs#BooleanAlgebra and similar

[Kevin Buzzard]

import Mathlib

structure foo where
  a : ℕ
  ha : a = 37

example : foo where
  ha := rfl

[Edward van de Meent]

Riccardo Brasca said:

Ah yes, that is some magic in the where syntax. My proposal is indeed to at least force people to write sSup := _ to make it clear that it is found by unification

it's not just where, it evidently also works with the {foo := _} notation

[Kyle Miller]

(where is a macro for {...} notation)

[Kyle Miller]

I'm working on some improvements to {...} notation, so some changes here could be possible. (Yes, this so-called 'structure instance notation' is sort of sugar for the structure's constructor @Junyan Xu, though it's a bit more complicated because it knows about default values and overriding default values, and, soon, filling in default values using all parent instances. Also, it doesn't expand as a macro to the structure constructor. It processes the fields and constructs the constructor application expression itself.)

While it's surprising that sup was filled in using the type of a proof, I'm not sure exactly what could be done here to get {...} to detect that this happened... I could imagine perhaps detecting which fields are Prop-valued and elaborating those last. Or perhaps we disallow filling in fields by pure unification — i.e., we throw a warning when a field isn't given and there is no default value for it. You'd have to write sup := _ if you wanted to opt-in to the current behavior.

[Junyan Xu]

Riccardo Brasca said:

What I find confusing in this example is that Lean infers data from a proof. I understand why this works, but it goes against the slogan "proofs don't matter", and it looks to me code smell.

I think it infers the data from the type of the proof. It's dependent type at work :)

[Edward van de Meent]

Kyle Miller said:

(where is a macro for {...} notation)

yes, so it's the where semantics that is magic, not the where syntax.
clearly {...} is different syntax.

[Kyle Miller]

I'm not sure what you're pointing out. Earlier you mentioned that it works with {...} notation too, but that's what I'd expect since where is a macro for it.

[Edward van de Meent]

i'm pointing out that you Riccardo Brasca said it's the where syntax that is magic (emphasis mine). if that were the case, it wouldn't work with {...} since it's different syntax with the same semantics.

[Kyle Miller]

I'm confused, I haven't said anything was magic. Are you confusing me with Riccardo?

[Edward van de Meent]

Oops :grimacing: my mistake :upside_down:

[Riccardo Brasca]

Kyle Miller said:

You'd have to write sup := _ if you wanted to opt-in to the current behavior.

This is what I proposed.

[Riccardo Brasca]

I understand it's not magic, and that it works because Lean sees the type of the proof so it guesses the Prop. But the fact the this was not immediately clear to expert users suggests it is a confusing behavior. (but maybe it's just our fault :sweat_smile: )

[Kyle Miller]

This is what I proposed.

Thanks for the confirmation, I wasn't completely sure what the proposal was, but I see it now in #new members > Where is sSup defined on submodules? @ 💬.

I think this will happen within the next couple releases.

[Kyle Miller]

Concretely, explicit fields will be required (unless they have a default value), implicit fields will be optional.

[Kyle Miller]

Kevin Buzzard said:

structure foo where
  a : ℕ
  ha : a = 37

example : foo where
  ha := rfl

This is what this example now reports post lean4#7717:

fields missing: 'a'

field 'a' must be explicitly provided, its synthesized value is
  37

If you instead define

 structure foo where
  {a : Nat}
  ha : a = 37

then it does not complain about the missing field.

[Mario Carneiro]

can you do

example : foo where
  a := _
  ha := rfl

?

[Kyle Miller]

Yeah, that's allowed

[Edward van de Meent]

i'm curious, were there other definitions in mathlib which had to be changed because of this?

[Edward van de Meent]

(find out at this diff)

[Eric Wieser]

I think that diff is everything so in 4.19.0, not just the effects of the relevant PR

[Edward van de Meent]

:sad:

[Eric Wieser]

I think this diff is the one you want

[Kevin Buzzard]

Oh this looks like a really happy ending to this story!