coercions for implicit arguments

Stream: general

[Cotton Seed]

Is it possible for coercions to apply to implicit arguments? I can't get an example like this to work:

structure probability_space
  (α: Type*) :=
  (α_is_measurable: measurable_space α)
  (μ: probability_measure α)

instance prob_space_coe_to_measure_space
  {α: Type*}
  : has_coe (probability_space α) (measure_space α)
  := {coe := λ P: probability_space α,
    @measure_space.mk α P.α_is_measurable P.μ}

instance prob_space_coe_to_measurable_space
  {α: Type*}
  : has_coe (probability_space α) (measurable_space α)
  := {coe := λ P: probability_space α, P.α_is_measurable}

structure random_variable
  {α β:Type*}
  [α_is_prob_space: probability_space α]
  [β_is_measurable: measurable_space β]
  (f: α → β) :=
  [f_measurable: measurable f]

I can get it to work by making the arguments explicit but it is much less readable: @measurable α _ α_is_prob_space _ f

Lean fails to infer α in @measurable _ _ α_is_prob_space _ f which was surprising since the constraint always comes from f.

[Heather Macbeth]

Hi @Cotton Seed, nice to see you here :)

Without addressing your question directly, the idiomatic way to express this situation is

variables (α : Type*) [measurable_space α]

Do you want to say a bit about your use case to see whether your setup with structures is needed?

[Cotton Seed]

Hey Heather, you too! Let me update the example with more meaningful names.

[Heather Macbeth]

I see your motivation. It would still be conventional not to bundle the space with the variable. See eg
docs#probability_theory.indep_fun

[Heather Macbeth]

or docs#measure_theory.condexp

[Cotton Seed]

OK, I understand your suggestion. This works:

structure probability_space
  (α: Type*)
  [α_is_measurable: measurable_space α] :=
  (μ: probability_measure α)

instance prob_space_coe_to_measure_space
  {α: Type*}
  [α_is_measurable: measurable_space α]
  : has_coe (probability_space α) (measure_space α)
  := {coe := λ P: probability_space α, measure_space.mk P.μ}

structure random_variable
  {α β:Type*}
  [α_is_measurable: measurable_space α]
  [α_is_prob_space: probability_space α]
  [β_is_measurable: measurable_space β]
  (f: α → β) :=
  [f_measurable: measurable f]

However, for complicated structures with many implicit dependencies, I was hoping to avoid listing all of them in every use of the structure.

[Cotton Seed]

I still seem to be having trouble with implicit arguments [...] inferred by type class resolution. Here is another simple example:

structure S (α:Type*) := (dummy: nat)

def S_fun {α:Type*} [S α] (f: α → α): Prop := tt

def S_id_bad1 (α:Type*) [s: S α]: S_fun (λ x:α, x) := sorry
/-
  15:5: failed to synthesize type class instance for
  α : Type ?,
  s : S α
  ⊢ S α
-/

def S_id_bad2 (α:Type*) [s: S α]: @S_fun _ _ (λ x:α, x) := sorry

def S_id_ok3 (α:Type*) [s: S α]: @S_fun _ s (λ x:α, x) := sorry

Why is s not inferred inside the call to S_fun in the return type of S_id_bad1? The error shows I have literally the correct term s available.

I've read the relevant parts of the reference manual but I couldn't find an explanation. I couldn't find a description of the "type class resolution" procedure used to infer [...] arguments.

[Kevin Buzzard]

The S in your code is a structure not a class, so [S \alpha] won't make sense to the type class system

class S (α:Type*) := (dummy: nat)

def S_fun {α:Type*} [S α] (f: α → α): Prop := tt

def S_id_bad1 (α:Type*) [S α]: S_fun (λ x:α, x) := sorry -- works fine

[Kevin Buzzard]

It is normally not necessary to name your class instances by the way; it's quite rare to see [s : S alpha] in mathlib and much more common to see [S alpha].

[Kevin Buzzard]

A class is just a structure tagged with the @[class] attribute, but this is the attribute that the typeclass system (the square brackets system) is looking out for when it does its hole-filling-in.

[Heather Macbeth]

@Cotton Seed This still feels a bit awkward to me, and more context would probably help. You're perhaps trying to make the type of "bundled measurable functions"? I think we'd usually have the f as a field rather than a parameter. So something like

variables {α : Type*} [measurable_space α] {β : Type*} [measurable_space β]

structure random_variable :=
(f : α → β)
(f_measurable : measurable f)

[Heather Macbeth]

You'll see I dropped every hypothesis, like (μ: probability_measure α) and [probability_space α], which wasn't actually needed for the definition; this is conventional.

[Heather Macbeth]

Also: you don't need to make this bundled definition in order to prove theorems about random variables. We would usually only make the bundled definition in this way to put further structure on it (like, say β was a group and you wanted to consider the group of measurable functions to β).

[Cotton Seed]

Thanks, @Kevin Buzzard! I get it now. And thanks for the suggestions both of you, I have a lot to experiment with now.