heterogenous operators and coercions

Stream: lean4

[Deniz Aydin]

While porting files on ints, I ran into confusing behaviour that led me to finding out about the new heterogenous operators.

The issue stemmed from the fact that there are multiple ways lean can express a+n. One lemma in the original file has the hypothesis {a b : ℤ} {n : ℕ} (h : b - a = n), and the next has the seemingly equivalent {a b : ℤ} {n : ℕ} (h : a + n = b). In lean4, the first gets translated into h : b - a = ofNat nand the second becomes h : a + n = b, where + here is the sneaky heterogenous kind causing the rewrite of add_comm to fail. Looking at how they're defined anyone would expect rearranging one to give you an identical hypothesis to the other.

What made this especially confusing to me was that neither of these behaviours is what would happen in lean3, which IIRC would insert a coercion arrow in front of n in both cases. Since coercion arrows are hidden by default in lean4 I assumed that this is what was happening and what I saw as h : a + n = b was actually h : a + ↑n = b. After all, how else can you add an int and a nat? This thinking led me to infuriating errors before I realised what was wrong:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  -a + (a + n)
a b : ℤ
n : ℕ
h : a + n = b
⊢ -a + (a + n) = ofNat n

To work around this I now make sure to use explicit coercion arrows wherever possible and enable showing coercions in the pretty printer (which I also struggled with as set_option pp.coercions true does the opposite of what the name suggests and should probably be renamed).

While having heterogenous operators (especially hMul) seem very useful, I suggest removing these instances for generating them from coercions. Users shouldn't have to worry about whether it's the operators that are being silently coerced or their inputs.

[Gabriel Ebner]

I've warned of this problem before: https://github.com/leanprover/lean4/issues/433#issuecomment-831928888
I completely agree with you that these instances should be removed.

[Gabriel Ebner]

Deniz Aydin said:

Since coercion arrows are hidden by default in lean4

Coercions are actually not hidden at all (except for these few problematic instances), they are even unfolded into the concrete coercion functions (instead of the generic arrow) which I like very much.

[Deniz Aydin]

Interesting, so does this mean that I should be expressing statements about coercions from Nat to Int using Int.ofNat instead of ↑ since that's now the default way lean translates statements like (a : Int) = (n : Nat)?
That does make it clear what's being coerced to what but I'm not sure I prefer it since it's a lot of boilerplate on what would otherwise be statements that read very naturally.

[Gabriel Ebner]

If you want to hide the Int.ofNat function, that's a 5 line delaboration function. We can even put it scoped in a namespace, so that you can enable it only when you want.

[Sebastien Gouezel]

Is there a way that, when one declares a coercion, the corresponding function automatically gets a special treatment in pretty-printing, and is represented by ↑ there?

[Gabriel Ebner]

You can write a macro that does both at once, declare the coercion and hide the function.