Coercions from Nat to Int

Stream: new members

[Philippe Duchon]

Generally speaking I was thinking I understood coercions, specifically from ℕ to ℤ; Theorem Proving in Lean 4 has a section on Coercions with examples, but only involving additions. I tried similar things with subtractions, and was a bis surprised at the result.

import Mathlib

variable (m n : ℕ) (i j: ℤ)
#check (m-n)+i
#eval ((3:ℕ) - (4:ℕ)) + (2:ℤ) -- 1

I was not surprised that (m-n)+i was typed as ℤ: this is similar to the case with additions in TPIL. But I was somehow expecting Lean to insert the coercion to ℤ after the subtraction, where it becomes clear that what is expected is a term of type ℤ and not ℕ; so 3-4 would be evaluated as 0:ℕ, then coerced to 0:ℤ, for a final value of 2.

So what I understand is that, somehow, Lean decides that natural numbers should be converted to integers as early as possible. I can see how this will be less confusing to a person not used to thinking in terms of having different types, but I don't understand why and how this works.

Is this somehow linked to the - notation? Does Lean somehow decide it wants to apply Int.sub and not Nat.sub, triggering coercions at this level? If I explicitly use Nat.sub in the expression instead, I do get the expected (by me) result 2:ℤ

[Chris Bailey]

Coercions are pushed out toward the leaves of the expression tree; the expected type of the expression is the sort of "goal" that gets propagated out during elaboration. Without having to understand how all of the parts of the elaborator are working together, I think the heuristic you can use is just "which possible coercion is further toward the leaves", which in this case is (↑3) - (↑4) rather than ↑(3 - 4).

[Philippe Duchon]

OK, thanks. So "expect coercions to be applied as early as possible" seems like a good mantra.

[Yaël Dillies]

No, that's not exactly right, Chris

[Chris Bailey]

Enlighten me then, I'm going off what I got here

[Yaël Dillies]

Arithmetic operators like +, -, * (but currently not ∑ nor ∏) have special elaborator support to push the coercion inside as you describe. However, other operators follow the usual rule which is to have the coercion outside

[Philippe Duchon]

OK, so my new mantra looks like it will be "it's not that simple". Which, in turn, is a good overall mantra with proof assistants.

[Chris Bailey]

@Yaël Dillies What's the actual definition of "arithmetic" in this context/can you give an example that doesn't follow the "coerce at the leaves" pattern? The first one I thought of that doesn't seem arithmetic is the List.cons notation, but that seems to want to coerce at the leaves even when an alternative is possible:

instance : Coe (List Nat) (List Int) where
  coe xs := xs.map Int.ofNat

def xs : List Int := (Nat.zero :: [])

/-
def xs : List.{0} Int :=
@List.cons.{0} Int (@Nat.cast.{0} Int instNatCastInt Nat.zero) (@List.nil.{0} Int)
-/
set_option pp.all true in #print xs


/-
def ys : List.{0} Int :=
@List.cons.{0} Int (@Nat.cast.{0} Int instNatCastInt Nat.zero) (@List.map.{0, 0} Nat Int Int.ofNat (@List.nil.{0} Nat))
-/
def ys : List Int := (Nat.zero :: ([]: List Nat))
set_option pp.all true in #print ys

[Chris Bailey]

I can get the other one to fire if I annotate it at the top:

def zs : List Int := ((Nat.zero :: []) : List Nat)

/-
def zs : List.{0} Int :=
@List.map.{0, 0} Nat Int Int.ofNat (@List.cons.{0} Nat Nat.zero (@List.nil.{0} Nat))
-/
set_option pp.all true in #print zs

[Yaël Dillies]

"arithmetic" means "is one of the few elaborators to use docs#Lean.Parser.Term.binop"

[Chris Bailey]

I don't think List.cons uses that, and using List.cons without the notation also seems to coerce at the leaves. I found this; I'll take a closer look into this when I get some time.

[Kyle Miller]

The expression tree elaborator has a module docstring here: https://github.com/leanprover/lean4/blob/39eaa214d464bac67696e7ee1279232f5e199164/src/Lean/Elab/Extra.lean#L83

There are a handful of other elaborators that participate, including unop%, etc. Any syntax that is a macro that expands to one of these elaborators is part of the expression tree. Parentheses count as being part of the expression tree too.

I found a couple messages where I tried to explain a bit about it (below). The core issue is that the basic arithmetic operations are completely heterogenous, so they can't propagate types from the expected type to the arguments (the output type is an outParam after all). For normally defined homogenous operators, like List.cons, then a natural consequence of the basic elaboration algorithm is that the expected type propagates inwards, causing coercions to be inserted as far inward as possible. The expression tree elaborator attempts to simulate this, but it will only ever be able to put coercions at its own synthetic notion of a leaf (sub-expressions that aren't one of these binop%/unop%/... elaborators).

Kyle Miller said:

Yeah, to first approximation it's outside-in, and it's wrong to say that "the rule is reversed".

Basic operation: it locates the entire tree of arithmetic expressions (the ones that participate in the binop%/unop%/rightact%/etc protocol), elaborates each leaf without an expected type, computes a type that everything can coerce to (the "maximal type"), then drops coercions at the leaves wherever they're needed. Just like for the Lean 3 "outside-in" description, coercions are at the leaves, but unlike pure "outside-in", (1) leaves can influence the type of the entire expression and (2) coercions can't be dropped inside the leaves, since elaboration is already completed.

If it weren't expensive, the way it could work instead is, rather than inserting coercions at leaves, is to re-elaborate each leaf with the computed maximal type. That would let the types propagate coercions deeper into subexpressions, like Finset.sum.

Kyle Miller said:

Outside-in vs inside-out isn't completely accurate. It elaborates each leaf in a full arithmetic expression without an expected type, then it computes a type that everything can be coerced to, and then it inserts coercions where needed.

A difference one can observe is that coercions don't get sunk into the leaves in expression trees -- they're stuck right at a leaf -- where if there were no such elaborator then coercions can get sunk arbitrarily deep based on expected types.