Casting

Stream: general

[Bolton Bailey]

When I write an expression with a certain type, enclose it in parentheses, put a colon after it, and then put a different type after the colon, I expect the value I put in parentheses to be cast to the new type. But that's not what happens here! Lean sees the real type and starts converting individual arguments to reals, casting n and missing the intended meaning. Is this a bug? Is there a way to achieve the bottom awkward ℕ) : ℝ more cleanly? (it seems perverse if this is the minimal-character way of doing this)

import data.real.basic

lemma mwe {n : ℕ} (n_one : n = 1) : ((2 * n / 3) : ℝ) = 0 :=
begin
  rw n_one,
  norm_num, -- false
end

lemma casting_twice {n : ℕ} (n_one : n = 1) : (((2 * n / 3) : ℕ) : ℝ) = 0 :=
begin
  rw n_one,
  norm_num, -- works
end

[Kyle Miller]

Yeah, this is how it works -- casting (coercion) goes "outside in". The cast is first and foremost a type ascription, so it ends up directing typeclass search to choose the has_div for a real-valued output, which causes the division's operands to be reals, and so on recursively.

[Kyle Miller]

One way is to explicitly put in the coercion arrow yourself:

lemma casting_twice {n : ℕ} (n_one : n = 1) : (↑(2 * n / 3) : ℝ) = 0 :=
begin
  rw n_one,
  norm_num, -- works
end

[Kyle Miller]

You can try searching for "elaboration outside in" in zulip for scattered details

[Kyle Miller]

Another example that might help make it clear Lean doesn't really do casting like other languages:

lemma casting_twice {n : ℕ} (n_one : n = 1) : ↑(2 * n / 3) = (0 : ℝ) :=
begin
  rw n_one,
  norm_num, -- works
end

[Eric Wieser]

I think the missing intuition is that (x : T) does not mean "cast x to T", it means "parse a T here, insert ↑s (the actual casts) if and where you need them"

[Yaël Dillies]

This is definitely very confusing to beginners and I remember having a hard time with it.

[Bolton Bailey]

Kyle Miller said:

One way is to explicitly put in the coercion arrow yourself:

lemma casting_twice {n : ℕ} (n_one : n = 1) : (↑(2 * n / 3) : ℝ) = 0 :=
begin
  rw n_one,
  norm_num, -- works
end

This solves the issue, but now that I understand the given-type coercion process better it leads to another question: If the casting is going outside-in figuring out the type of everything from the top of the syntax tree, when it reaches the ↑, how does it figure out the type of the / inside? Does it wait until it spots an ambiguity and then start working bottom-up?

[Kyle Miller]

The answer is what Eric was alluding to: "casting" is actually about automatically inserting ↑s in certain places when Lean detects a type mismatch. It's the elaboration (i.e., solving for things like implicit arguments, like types) that's going outside-in. The coercion arrow has type a -> b, so when Lean solves for a and b they don't contribute any constraints. Later it'll do typeclass inference to find a has_coe instance for those particular a and b.

[Kyle Miller]

What's going on with this example (going outside in) is that with ↑(2 * n / 3), lean knows the coercion has to go to ℝ, but it doesn't know yet what it's coercing from.

Then it looks at 2 * n /3, and it still doesn't know what the value should be, but since / requires everything to be the same type, now 2 * n and 3 are constrained to have the same type. It then looks at 2 * n, and since n has type ℕ, then we know 2 and 3 have that type. Then those literals are interpreted as terms of ℕ (they're actually expressions in terms of bit0 and bit1).