confused about coercions

Stream: mathlib4

[Kevin Buzzard]

I'm trying to explain coercions in mathlib4 to my class but I realise I don't understand them myself.

import Mathlib

example (x : ℕ) : (x : ℂ) = x := by
  -- `⊢ ↑x = ↑x`
  rfl

example (f : ℕ →+ ℕ) (x : ℕ) : f x = f x := by
  -- `⊢ f x = f x`
  rfl

example (S : Set ℕ) : (S : Type) = S := by
  -- `⊢ ↑S = ↑S`
  rfl

So is the rule that lean 3 coercions from types to types have an up-arrow in lean 4, lean 3 coercions to functions don't have any arrows any more, and lean 3 coercions to sort used to have an exotic arrow but now just have a simple up-arrow? Or is something more complicated going on? Or do I have some settings on some values which can be changed?

[Eric Wieser]

So is the rule that lean 3 coercions from types to types have an up-arrow in lean 4

Yes, if tagged with @[coe]

lean 3 coercions to functions don't have any arrows any more,

Only Funlike.coe has special printing rules. Yes, but the arrow is printed if there is no argument to make it obvious

[Yury G. Kudryashov]

BTW, you can use set_option pp.coercions false to see what functions are actually used for coercions.

[Eric Wieser]

Just to make things more confusing

-- `set_option pp.coercions false ` has no effect!
example (S : Submonoid ℕ) : (S : Type) = S := by
  -- `⊢ ↥S = ↥S`
  rfl

[Eric Wieser]

↥ is used for {x // x \in _}, but not Set.Elem

[Yury G. Kudryashov]

In Lean 3, we had generic coe/coe_fn/coe_sort, now Lean unfolds to Nat.cast, FunLike.coe, and Set.Elem in your examples.

[Yury G. Kudryashov]

The arrows are added by delaborators and we can cahnge the rules without touching Lean core source code.

[Kevin Buzzard]

So, to summarise, the rule now is that it's chaos?

[Kevin Buzzard]

in the sense that I cannot give some succinct list of rules to undergraduates, like I could in Lean 3? (other than "erm...it depends on which delaborators have been written")

[Eric Wieser]

Make the list of rules you want to have, then ask someone to fix them in Std/mathlib

[Kevin Buzzard]

It's too late for my course now -- I will not be upgrading mathlib because the course has started and experience shows me that not upgrading mathlib solves more problems than it causes. I'm writing documentation.