Zulip Chat Archive

Stream: mathlib4

Topic: mathlib4#557


Moritz Doll (Nov 08 2022 at 10:22):

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 (Nov 08 2022 at 10:38):

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

Moritz Doll (Nov 08 2022 at 10:42):

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

Yaël Dillies (Nov 08 2022 at 10:42):

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 (Nov 08 2022 at 10:48):

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

Gabriel Ebner (Nov 08 2022 at 22:57):

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 (Nov 08 2022 at 22:58):

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 (Nov 08 2022 at 23:00):

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

Gabriel Ebner (Nov 08 2022 at 23:00):

So I think this instance is no longer necessary.

Gabriel Ebner (Nov 08 2022 at 23:01):

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 (Nov 09 2022 at 00:14):

Thanks Gabriel for the explanation.

Moritz Doll (Nov 09 2022 at 00:23):

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 (Nov 09 2022 at 00:25):

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

Gabriel Ebner (Nov 09 2022 at 00:27):

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 (Nov 09 2022 at 07:02):

@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.


Last updated: Dec 20 2023 at 11:08 UTC