mathlib4#557

Stream: mathlib4

[Moritz Doll]

It seems that the way that coercions work seems to have changed significantly and I have no idea how to do transitive coercions.
This is the #mwe version of what mathlib3port gave me:

variable {R S M : Type _} [Coe R S] [CoeTC S M] (r : R)

#check (r : M)

but it fails in Lean4.

[Moritz Doll]

with [Coe S M] it does work, but I don't know whether this is correct solution for Algebra.NeZero

[Moritz Doll]

it is funny, [CoeTC R S] [Coe S M] works as well. Is there a transitive instance missing somewhere?

[Yaël Dillies]

Transitivity coercions are only added at the end of the chain, not at the beginning. I don't think that changed between Lean 3 and Lean 4.

[Eric Wieser]

See docs4#CoeHTCT; Lean4 has a mechanism for chaining coercions at both ends

[Gabriel Ebner]

Oh yeah, this instance won't work at all:

instance coe_trans [Zero M] [Coe R S] [CoeTail S M] [h : NeZero (r : M)] : NeZero ((r : S) : M) :=
  ⟨h.out⟩

[Gabriel Ebner]

In Lean 4, coercions are expanded eagerly by the elaborator. So there's never a coe function appearing in the elaborated term, and there's nothing for TC synthesis to match on here.

[Gabriel Ebner]

Maybe another angle: in Lean 4, NeZero (r : M) and NeZero ((r : S) : M) will usually elaborate to syntactically the same term.

[Gabriel Ebner]

So I think this instance is no longer necessary.

[Gabriel Ebner]

Also: [Coe A B] assumptions are evil (because they don't work well with the eager coe expansion). Avoid them outside of instance [Coe A B] : Coe (List A) (List B)

[Moritz Doll]

Thanks Gabriel for the explanation.

[Moritz Doll]

A funny thing happens on mathlib4#557: In the file I've added I am using the variable n but it is never declared and Lean magically knows thatn : Nat. Is this just a very smart type inference system or are variables bleeding into other files?

[Gabriel Ebner]

It's called auto-implicits. It's the same mechanism that makes def foo (xs : List α) : Nat := xs.length work.

[Gabriel Ebner]

I was unsure of the name for a second. This one is auto-implicits (with the autoImplicit option to turn it off). Don't confuse it with implicit lambdas, which is also auto and implicit :smile: but lambda.

[Kevin Buzzard]

@Moritz Doll one of the first things I do when porting a file is to add a bunch of imports so I have tools like library_search, and to turn autoImplicit off (because it can be confusing with files written by a computer). I delete this stuff at the end when the port of the file is finished.