Field notation and `CoeFun`

Stream: mathlib4

[Wojciech Nawrocki]

I came across this while looking into porting Algebra.Group.TypeTags. In Lean 3 we can write

import logic.equiv.defs

def foo := nat
def foo.to_foo : foo ≃ foo := ⟨λx, x, λx, x, λx, rfl, λx, rfl⟩

example (f : foo) : f.to_foo = f.to_foo := sorry

but in Lean 4 we get

import Mathlib.Logic.Equiv.Defs

def Foo := Nat
def Foo.to_Foo : Foo ≃ Foo := ⟨λx => x, λx => x, λx => rfl, λx => rfl⟩

/- invalid field notation, function 'Foo.to_Foo' does not have argument with type (Foo ...) that can be used, it must be explicit or implicit with an unique name -/
example (f : Foo) : f.to_Foo = f.to_Foo := sorry

I am assuming this is because the elaborator for field notation has changed and no longer is happy to apply the CoeFun. Three possible options would be to

• a) adjust the elaborator (difficult); or
• b) port it as Foo.to_Foo f (easy, just churn); or
• c) port it as

def Foo.equiv_Foo : Foo ≃ Foo := ⟨λx => x, λx => x, λx => rfl, λx => rfl⟩
def Foo.to_Foo : Foo → Foo := fun f => equiv_Foo f

(different kind of churn)

What does everyone think?

[Eric Wieser]

Having dot notation work on bundled morphisms like this was often convenient in Lean 3; it would be a shame to lose it

[Eric Wieser]

c) sounds like either something that should be done as a post-port refactor after first porting b), or as a pre-port refactor in mathlib3 if we're really sure a) is ruled out

[Eric Wieser]

The big problem with c) is that now you have two ways to spell the same thing and you either need lemmas about both, or need to declare one of them canonical and essentially never use the other.

[Scott Morrison]

@Wojciech Nawrocki, could you give a more realistic example? I would argue that we never should have been writing f.to_foo! It took me a long moment to work out that this was meant to mean (foo.to_foo : foo \to foo) f in the first place.

[Scott Morrison]

i.e. looking at an example like this, I would describe it as "gross misuse of dot notation" rather than "convenient". :-)

[Yury G. Kudryashov]

See, e.g., docs#enat.to_nat

[Yury G. Kudryashov]

It is natural to write (n : ℕ∞).to_nat; it is bundled as a monoid_with_zero_hom.

[Yury G. Kudryashov]

Note that it worked in Lean 3 only if the function had exactly 1 argument, so, e.g., we were unable to bundle polynomial.map without loosing dot notation.

[Scott Morrison]

If someone is interested in writing this up as an issue (i.e. with a #mwe that doesn't need mathlib4, and that explains a valuable use case), we could see what the Lean 4 devs think.

[Wojciech Nawrocki]

Scott Morrison said:

If someone is interested in writing this up as an issue (i.e. with a #mwe that doesn't need mathlib4, and that explains a valuable use case), we could see what the Lean 4 devs think.

I will do it.

[Yury G. Kudryashov]

It's quite possible that the answer will be "you should unfold old coercions!"

[Yury G. Kudryashov]

But this way we'll loose generic map_mul etc lemmas.

[Yury G. Kudryashov]

(unless someone rewrites simp so that it unifies @[coe] functions with coe in simp lemmas)

[Kyle Miller]

Just to point toward was was going on in the Lean 3 side, this is what the last paragraph for this Lean 3 commit message was about: https://github.com/leanprover-community/lean/commit/f2b2beefe2e9ab200d23e1c99dc20879eb32e9fa

Reproduced here:

To preserve reverse compatibility, we (temporarily?) add a feature that if the elaborator fails to find an explicit argument corresponding to the structure, it will insert the structure as the first explicit argument. This matches the previous behavior for non-application dot notation (x.f). The reason for including this feature is that mathlib has been misusing this type of dot notation for terms with has_coe_to_fun instances. It is not currently compatible with Lean 4.

[Kyle Miller]

What was going on in Lean 3 is that there were two ways that dot notation was resolved, depending on whether it's a term of the form x.f a b c (with arguments) or x.f (no arguments). In the second case, if x : Foo, it would always turn it into Foo.f x no matter what. If Foo.f was an equiv, then since this isn't a function the elaborator would insert a has_coe_to_fun coercion for you.

When there were arguments, then it would use a different resolution scheme and would always fail for this sort of equiv example.

[Kyle Miller]

(That commit fixed the fact that there were two separate ways of resolving dot notation, but the cost was explicitly programming in the old behavior to support this kind of equiv example.)

[Kyle Miller]

One way Lean 4 could be modified would be to have the elaborator try a pass at using a CoeFun instance if the normal dot notation resolution fails. Given my understanding of this part of the Lean 4 elaborator, this might not be very straightforward (at least it seems like it would involve reorganizing how it works, more than just a patch).

[Mario Carneiro]

We could add this as a rule to lean 4: If we can't find an argument of type Foo in a Foo.f dot-notation application, but the target type has a CoeFun instance, then apply it and look in the new arguments, and so on recursively. However, that algorithm loops if you have CoeFun A (B -> A) and you are looking for a Foo in Foo.f : A

[Eric Rodriguez]

will we ever have instances of that form?

[Mario Carneiro]

Probably not, but I wrote one just a few minutes ago

[Mario Carneiro]

Lambda calculus types like to have a CoeFun instance for .app

[Mario Carneiro]

In fact even Expr has one of these (in lean 3, not sure about lean 4)

[Mario Carneiro]

We could detect that the instance has this form explicitly as an optimization though

[Mario Carneiro]

or do cycle detection to avoid loops

[Kyle Miller]

or use a complexity measure on the syntactic term being coerced as as upper bound on the number of iterations :smile: (observation: in realistic use cases, this feature is for arrow-like types, so the target of the dot notation ought to correspond to one of the subterms that is already present)

[Mario Carneiro]

until I make a CoeFun A (B -> T A) and CoeFun (T (T (T (T A)))) (Foo -> Unit) because I really wanted to have four arguments and then a Foo :smile:

[Wojciech Nawrocki]

Filed as lean4#1910.