out_param

Stream: new members

[Nicolò Cavalleri]

Up to some moths ago, this:

import tactic.basic

@[nolint has_inhabited_instance]
structure right_inv {α: Type*} {β: Type*} (f : α → β) :=
(to_fun : β → α)
(right_inv' : function.right_inverse to_fun f)

variables {α: Type*} {β: Type*} {f : α → β} {g h : right_inv f}

instance : has_coe_to_fun (right_inv f) := ⟨_, right_inv.to_fun⟩

worked, but now has_coe_to_fun wants term of type out_param something. I have never heard about out_param before, is this new? If not, how does it have to do with has_coe_to_fun? docs#out_param is not really terribly helpful to me...

[Yaël Dillies]

There has been a change to has_coe_to_fun. It now expects the type of the function.

[Anne Baanen]

out_param is a synonym for id, so you can mostly ignore it unless you're defining a new class.

[Yaël Dillies]

instance : has_coe_to_fun (right_inv f) (λ _, β → α} := ⟨right_inv.to_fun⟩

[Nicolò Cavalleri]

Yaël Dillies said:

instance : has_coe_to_fun (right_inv f) (λ _, β → α} := ⟨right_inv.to_fun⟩

I see thanks, so now the type of the function needs to be given before := instead of after. Does this mean that now one can define multiple instances of has_coe_to_fun for the same type?

[Eric Rodriguez]

no, this is actually what the out_param means; it tells Lean that given the other arguments, the rest are uniquely determined

[Nicolò Cavalleri]

I am not sure if I understand maybe it would help me to know why is this an improvement with respect to before

[Nicolò Cavalleri]

Eric Rodriguez said:

no, this is actually what the out_param means; it tells Lean that given the other arguments, the rest are uniquely determined

by the rest you mean the argument following out_param? Why is this different than using curly brackets?

[Riccardo Brasca]

I think it's a matter of performance. It tells Lean where to look for it.

[Anne Baanen]

Nicolò Cavalleri said:

I am not sure if I understand maybe it would help me to know why is this an improvement with respect to before

Reason 1 is for compatibility with Lean 4. Reason 2 is that this makes it possible to talk about the function's type in subclasses, for example to specify M and N are monoids in docs#monoid_hom_class

[Nicolò Cavalleri]

Anne Baanen said:

Nicolò Cavalleri said:

I am not sure if I understand maybe it would help me to know why is this an improvement with respect to before

Reason 1 is for compatibility with Lean 4. Reason 2 is that this makes it possible to talk about the function's type in subclasses, for example to specify M and N are monoids in docs#monoid_hom_class

Ok thanks

[Nicolò Cavalleri]

Moreover now

lemma coe_injective (H : ⇑g = h) : g = h := sorry

goes wrong because

has_coe_to_fun (right_inv f) (λ {g : right_inv f}, right_inv f)

I can fix it by writing

lemma coe_injective (H : (g : β → α) = h) : g = h := sorry

but is this normal? Will I not be able to use ⇑ anymore from now on?

[Anne Baanen]

Nicolò Cavalleri said:

Eric Rodriguez said:

no, this is actually what the out_param means; it tells Lean that given the other arguments, the rest are uniquely determined

by the rest you mean the argument following out_param? Why is this different than using curly brackets?

It means the set of parameters that contain out_param are (assumed to be) uniquely determined by the ones without out_param. Let's take has_coe_to_fun as an example:

class has_coe_to_fun (a : Sort u) (F : out_param (a → Sort v)) :=
(coe : Π x : a, F x)

Here, F : out_param _ indicates that the parameter F is uniquely determined by the value passed for a. In particular, if Lean is looking for a has_coe_to_fun instance, once it finds one with the correct a, it won't look for an alternative with a different F.

This is starting to get a bit technical, but the reason you'd want to make something an out_param instead of leaving it implicit is that Lean waits untill all non-out_params are filled before searching for an instance.

[Anne Baanen]

(It's a bit more complicated for stuff like docs#monoid_hom_class where you have instance parameters depending on out_params, but that's the basic idea.)

[Anne Baanen]

Nicolò Cavalleri said:

Moreover now

lemma coe_injective (H : ⇑g = h) : g = h := sorry

goes wrong because

has_coe_to_fun (right_inv f) (λ {g : right_inv f}, right_inv f)

I can fix it by writing

lemma coe_injective (H : (g : β → α) = h) : g = h := sorry

but is this normal? Will I not be able to use ⇑ anymore from now on?

That is not supposed to happen, but out_params are less tested than the rest so it doesn't really surprise me that it's broken.

[Anne Baanen]

For what it's worth, you can now make a docs#fun_like instance for right_inv, and then you get rules like coe_injective and congr_arg for free!

[Nicolò Cavalleri]

Anne Baanen said:

Here, F : out_param _ indicates that the parameter F is uniquely determined by the value passed for a. In particular, if Lean is looking for a has_coe_to_fun instance, once it finds one with the correct a, it won't look for an alternative with a different F.

Isn't this similar to putting curly brackets around F though?

[Nicolò Cavalleri]

Anne Baanen said:

For what it's worth, you can now make a docs#fun_like instance for right_inv, and then you get rules like coe_injective and congr_arg for free!

Wow this is cool I've been waiting for something like this for ages!

[Anne Baanen]

Nicolò Cavalleri said:

Anne Baanen said:

Here, F : out_param _ indicates that the parameter F is uniquely determined by the value passed for a. In particular, if Lean is looking for a has_coe_to_fun instance, once it finds one with the correct a, it won't look for an alternative with a different F.

Isn't this similar to putting curly brackets around F though?

Not exactly: curly brackets are used for function application, out_param is used for instance synthesis. (Although the unifier tries explicit parameters before implicit parameters, and the unifier is called to check instances...)

[Nicolò Cavalleri]

Anne Baanen said:

Nicolò Cavalleri said:

Anne Baanen said:

Here, F : out_param _ indicates that the parameter F is uniquely determined by the value passed for a. In particular, if Lean is looking for a has_coe_to_fun instance, once it finds one with the correct a, it won't look for an alternative with a different F.

Isn't this similar to putting curly brackets around F though?

Not exactly: curly brackets are used for function application, out_param is used for instance synthesis. (Although the unifier tries explicit parameters before implicit parameters, and the unifier is called to check instances...)

I see I think I understand now