Problem when instances are inside a structure

Stream: lean4

[Terence Tao]

Hi, for the PFR project there is a large amount of data and instances that I am trying to place inside a single structure in order not to repeatedly state all that data every time I state a new lemma. I figured out how to invoke individual instances that are buried inside the structure when needed, but encountered a problem when invoking an instance that depended on another instance, due to a definitional equality problem.

Here is a MWE (with a much smaller package of data than what I actually want to use). The following code works,

import Mathlib

structure package :=
  G : Type*
  hGm : MeasurableSpace G
  hGsc : MeasurableSingletonClass G

example (p:package) (a: p.G) : have _ := p.hGm; MeasurableSet {a} :=
  @MeasurableSingletonClass.measurableSet_singleton p.G p.hGm p.hGsc a

but the code

example (p:package) (a: p.G) : have _ := p.hGm; MeasurableSet {a} := by
  have hGm := p.hGm
  have hGsc := p.hGsc
  apply MeasurableSingletonClass.measurableSet_singleton a

fails because hGsc has type MeasurableSingletonClass p.G p.hGm which is not definitionally equal to MeasurableSingletonClass p.G hGm and so one gets a "failed to synthesize MeasurableSingletonClass p.G" message. I attempted to force the correct type with

example (p:package) (a: p.G) : have _ := p.hGm; MeasurableSet {a} := by
  have hGm := p.hGm
  have hGsc : @MeasurableSingletonClass p.G hGm := p.hGsc
  apply MeasurableSingletonClass.measurableSet_singleton a

but this simply created a type mismatch error: p.hGsc has type @MeasurableSingletonClass p.G p.hGm : Prop but is expected to have type @MeasurableSingletonClass p.G hGm : Prop.

For this example, is there any way to extract both the MeasurableSpace instance and the MeasurableSingletonClass instance from p:package as compatible instances, without having to manually insert all the instances with the @ notation on every line?

UPDATE: replacing all the haves by lets works (I guess it creates the needed definitional equality). So never mind, I answered my own question...

[Yaël Dillies]

Is there a reason why package is a structure, not a class?

[Terence Tao]

Hmm, I was actually not explicitly aware of this distinction. I guess it makes sense that a class could help with automatic inferencing.

The full package currently looks like this:

/-- A structure that packages all the fixed information in the main argument.  -/
structure multiRefPackage :=
  G : Type uG
  hG : AddCommGroup G
  hGf : Fintype G
  hGm : MeasurableSpace G
  hGsc : MeasurableSingletonClass G
  m : ℕ
  htorsion : ∀ x : G, m • x = 0
  Ω₀ : Type*
  hΩ₀ : MeasureSpace Ω₀
  hprob : IsProbabilityMeasure (ℙ : Measure Ω₀)
  X₀ : Ω₀ → G
  hmeas : Measurable X₀
  η : ℝ
  hη : 0 < η

Suppose I was given p:multiRefPackage and wanted to extract out the object p.G complete with its instances AddCommGroup, FinType, MeasurableSpace, MeasurableSingletonClass. If I made multiRefPackage a class instead of a structure, is there a way to do this without having to explicitly introduce the instances like I have been doing above? That would certainly be convenient.

I guess I'm having a conceptual issue here in that the reference package I am working with is not simply a single object G with various instances attached to it, but a collection of loosely related objects, each with their own instances, so I don't know how to use the class formalism properly here. I guess one needs to define something like multiRefPackage.toGroup and attach various instances to it?

[Logan Murphy]

I'm not sure if this is helpful, usually when I think "i need to pull out objects" I think of structures, but here's a partially similar class:

class multiRefPackage (G : Type u)
  extends AddCommGroup G, Fintype G,
          MeasurableSpace G, MeasurableSingletonClass G

example {G : Type u} [multiRefPackage G] (a: G) : MeasurableSet {a} :=
  by apply MeasurableSingletonClass.measurableSet_singleton a

[Terence Tao]

That helps - it gives a way of collecting multiple instances into a single combined instance, and now one only needs to pull out one instance out of the structure whenever pulling out the associated object, rather than pulling out two instances as I did in the original MWE. Ideally I'd like to go one step further and just pull out the object and have the instances come automatically, but this certainly makes things a bit less annoying.

[Patrick Massot]

Having internal universe variable is very likely to cause issues. So G and Ω₀ should probably be parameters, as in Logan’s message, but also pulling out Ω₀.

[Yaël Dillies]

Alternatively, make G : Type. That's justified by the fact that any finite group in Type u is isomorphic to a finite group in Type

[Logan Murphy]

I suppose, if Terence did want to hide the carrier type as a structure projection, there's no way to avoid explicitly re-inferring the instances? E.g.,

class multiRefClass (G : Type)
  extends AddCommGroup G, Fintype G,
          MeasurableSpace G, MeasurableSingletonClass G

structure myPackage where
  G : Type
  (hG : multiRefClass G)

/-- Can't circumvent this? --/
instance {p : myPackage} : MeasurableSpace p.G :=
  match p with | ⟨_,_⟩ => inferInstance

example (p : myPackage) (a: p.G) : MeasurableSet {a} :=
  by apply MeasurableSingletonClass.measurableSet_singleton a

[Terence Tao]

Patrick Massot said:

Having internal universe variable is very likely to cause issues. So G and Ω₀ should probably be parameters, as in Logan’s message, but also pulling out Ω₀.

OK, I tried this, but I ran into a stupid problem, because both G and Ω₀ are competing for the .toMeasurableSpace method, and so

class multiRefPackage (G: Type*) (Ω₀: Type*)
  extends AddCommGroup G, Fintype G, MeasurableSpace G, MeasurableSingletonClass G,
                   MeasureSpace Ω₀ where
  m : ℕ
  htorsion : ∀ x : G, m • x = 0
  hprob : IsProbabilityMeasure (ℙ : Measure Ω₀)
  X₀ : Ω₀ → G
  hmeas : Measurable X₀
  η : ℝ
  hη : 0 < η

etc. does not work directly.

[Yaël Dillies]

Logan Murphy, what does

structure myPackage where
  G : Type
  [hG : multiRefClass G]

do? In particular, does it do what you want?

[Logan Murphy]

Doesn't seem like we can use typeclass binders in class/structure fields, it gives a syntax error

[Logan Murphy]

Terence Tao said:

OK, I tried this, but I ran into a stupid problem, because both G and Ω₀ are competing for the .toMeasurableSpace method

I guess a parameterized version could be something like:

class MeasureableFinGroup (G : Type*)
extends AddCommGroup G, Fintype G,
          MeasurableSpace G, MeasurableSingletonClass G

structure multiRefPackage (G : Type*) (Ωₒ : Type*) [MeasureableFinGroup G] [MeasureSpace Ωₒ] where
  (m : ℕ)
  (htorsion : ∀ x : G, m • x = 0)
  (hprob : IsProbabilityMeasure (ℙ : Measure Ωₒ))
  (X₀ : Ωₒ → G)
  (hmeas : Measurable X₀)
  (η : ℝ)
  (hη : 0 < η)

[Terence Tao]

OK, that seems to work reasonably well. Thanks!

[Terence Tao]

So I guess the broader recommendation here is to not place instances inside a structure, or to concatenate together instances attached to different objects, but it is perfectly fine to concatenate instances on a single object into a unified class.

[Logan Murphy]

Well, combining the instances on G into MeasureableFinGroup is really just to improve legibility, you could in principle move all the instances as parameters of multiRefPackage. I think the general recommendation would be something like "to make typeclass inferences easier, you probably want to use structures in which types and typeclass instances are parameters rather than structure fields"

[Johan Commelin]

@Logan Murphy @Terence Tao I think there is also a technical reason for the split:

Suppose that Lean wants to find some fact about G, for example that it has a measure, or an addition. That means there is a goal like Add G. Now typeclass synthesis starts chasing around the large hierarchy in mathlib to find an instance that would imply Add G. Turns out that superBigPackage G ?m1 would imply it. But at that point in time, Lean doesn't know Omega, so it disregards that path.

[Johan Commelin]

That is why so many lemmas in the linear algebra part of mathlib make the ring of scalars explicit. Because when Lean hunts for Module ?m1 M it doesn't know which ring to assign to ?m1 and the search fails. But when we make the ring explicit, Lean searches for Module R M and then we're on the happy path.