Visibility of coercions

Stream: lean4

[Jovan Gerbscheid]

I was doing some tests, and ended up with some code equivalent to this:

def n : Nat := 100
def m : Fin 100 := 50
#eval m ≤ n

I expected the result to be true, but it is false. This is because n is coerced to 0 : Fin 100. I was not aware of this coercion existing, and I thought it would coerce m to a Nat. I don't have an opinion on which coercion is the 'right' one, however I would like to be able to see which coercion is going on. No matter where I put the cursor or hover the mouse, it doesn't say anything about the coercion.

So I would like to see a change to the hover info so that coercions become visible. In Haskell, I remember that hovering over an expression shows you the type of that expression and not just the information about the constant. So in this example, one possible way to resolve my confusion would be by hovering over n, and the hover info telling me that it has type Fin 100 instead of the Nat that shows up now.

[Eric Wieser]

You can use check to see the coercion:

def n : Nat := 100
def m : Fin 100 := 50
#check m ≤ n  -- m.val ≤ n : Prop

[Jovan Gerbscheid]

I see, but what if I'm writing some more complicated function, which happens to have m ≤ n as a subexpression. e.g.

def f (n : Nat) (m : Fin 100) : Prop := n ≤ m

[Mauricio Collares]

And importing Mathlib:

import Mathlib

def n : Nat := 100
def m : Fin 100 := 50

set_option pp.coercions false
#check m ≤ n -- m ≤ Nat.cast n : Prop

[Kyle Miller]

@Eric Wieser You're seeing m.val ≤ n, but we're seeing m ≤ ↑n.

[Eric Wieser]

Yep, my version was without imports

[Kyle Miller]

This is really not good that there's a cycle in coercions.

This is fun:

import Mathlib.Tactic

def n : Nat := 100
def m : Fin 100 := 50
#eval m ≤ n -- false
#eval n ≤ m -- false

[Eric Wieser]

import Mathlib.Data.Fin.Basic seem to be enough to switch the behavior

[Kyle Miller]

The expression tree elaborator (which ≤ participates in) assumes that the coercion instances form some kind of directed system

[Eric Wieser]

Specifically, docs#Fin.instAddMonoidWithOne changes the tide (because it makes #synth NatCast (Fin 100) succeed)

[Eric Wieser]

Arguably Fin.val is the bad coercion because its not structure-preserving

[Kyle Miller]

The coercion from Fin to Nat makes sense to have, since it's a subtype coercion, but is there some solution where we can prevent the Nat to Fin coercion? I thought having an algebraic structure was what docs#ZMod was for.

[Eric Wieser]

ZMod 0 and Fin 0 are very different, so I don't think one can be dropped in as a replacement for the other

[Eric Wieser]

Also, Fin (2 ^ n) is used to implement bitvectors and fixed-width integers, which are available long before Zmod

[Kyle Miller]

Is there something we can do about NatCast not giving Fin a Nat -> Fin coercion?

[Kyle Miller]

Fin is used as a plain subtype of Nat too, for indexing. For that use, having the the coercion to Nat seems to make sense.

I find non-injective coercions to be suspicious in general though. I'd think it would be better if you only got a NatCast-derived automatic coercion in characteristic 0.

[Yaël Dillies]

Isn't the Nat to Fin used precisely to have wrapping indices too?

[Mario Carneiro]

who wants wrapping indices?

[Mario Carneiro]

Kyle Miller said:

Is there something we can do about NatCast not giving Fin a Nat -> Fin coercion?

This one isn't NatCast's fault, it is a "notation typeclass" for exactly this map. Rather, you should blame AddGroupWithOne for having a NatCast instance

[Eric Wieser]

Mario Carneiro said:

who wants wrapping indices?

Toeplitz matrices are one example

[Eric Wieser]

Kyle Miller said:

I find non-injective coercions to be suspicious in general though.

We use them quite a lot for quotient constructions, though we could perhaps allocate a different notation there

[Mario Carneiro]

we already do, the \[[ x \]] notation

[Kevin Buzzard]

Or we could remove the additive group structure from Fin completely and tell users to use ZMod if they want a group structure and fin if they want the finite set. In my brain there's a coercion from Fin n to Nat and a coercion from Nat to ZMod n and no coercions in either of the opposite directions, and this is what distinguishes the set Fin n from the group ZMod n.

[Eric Wieser]

Mario Carneiro said:

we already do, the \[[ x \]] notation

We don't use that though because it has the wrong type up to semireducibility

[Kyle Miller]

I've mentioned before that I'd like having [[x]] be a notation typeclass. Would this be another point in favor for that?

[Mario Carneiro]

yeah I'd love to fix [[x]] to just do the right thing in quotient wrapper types

[Mario Carneiro]

not sure that means making it a notation typeclass, additional magic may be needed

[Jovan Gerbscheid]

Maybe we can remove the additive structure of Fin, and keep the ability to have wrapping indices, by instead having a group action of Int on Fin n that shifts the indeces cyclicly?

[Eric Wieser]

We probably want that action anyway, regardless of the other conversation here:

import Mathlib

-- this instance might cause some diamonds, or it might be fine
instance AddMonoidWithOne.toAddAction {R} [AddMonoidWithOne R] : AddAction ℕ R :=
  AddAction.compHom _ (Nat.castAddMonoidHom R)

-- this instance might cause some diamonds, or it might be fine
instance AddGroupWithOne.toAddAction {R} [AddGroupWithOne R] : AddAction ℤ R :=
  AddAction.compHom _ (Int.castAddHom R)

variable (n : ℕ) [NeZero n] in
#synth AddAction ℤ (Fin n)

[Yaël Dillies]

Yeah I had a branch adding those fields to AddCommGroupWithOne in Lean 3.

[Eric Wieser]

Did you have a case in mind where they were needed to avoid a diamond?

[Eric Wieser]

The only case I can think of where you might want a different defeq is complex numbers, where you could pick either (n + re, im) or (n + re, 0 + im) (where my proposal above gives the latter)

[Jovan Gerbscheid]

Going back to the original question, I think that it would be very beneficial for lean as a programming language that when you hover your mouse over an expression it shows you the 'true' type of that expression. There is this thing in the infoview called expected type that sort of does this but not quite; For example it doesn't show the coerced type. I want to be able to hover over the coerced m : Fin 100, and the info telling me that it has type Nat.

In tactic mode this isn't an issue because you can hover over expressions in the tactic state view (and coercions are shown), so this is just about lean as a (meta) programming language.