# Zulip Chat Archive

## Stream: new members

### Topic: Cast weirdness

#### Neil Strickland (Mar 20 2019 at 11:27):

Can anyone help me to understand what is going on here?

lemma L (n : ℤ) (p : n ≥ 0) (q : n < 1) : true := begin have h0 : n = n.nat_abs := int.eq_nat_abs_of_zero_le p, have h1 : (1 : ℤ) = ((1 : ℕ) : ℤ) := dec_trivial, rw[h0,h1] at q, -- Now q : ↑(int.nat_abs n) < ↑1 have h2 : n.nat_abs < 1 := (@nat.cast_lt ℤ _ n.nat_abs 1).mp q, end

Lean rejects `h2`

with a type mismatch error. It says that `q`

has the following type:

@has_lt.lt int int.has_lt (@coe nat int (@coe_to_lift nat int (@coe_base nat int int.has_coe)) (int.nat_abs n)) (@coe nat int (@coe_to_lift nat int (@coe_base nat int int.has_coe)) 1)

This seems sensible. However, it says that `q`

is expected to have a different type, the description of which takes 70 lines or so. The difference seems to involve some kind of issue with typeclass inference and possibly different coercion functions, but I have not been able to understand this properly. I have tried a number of other syntax variants without any more success.

#### Mario Carneiro (Mar 20 2019 at 11:35):

The coercion `nat -> int`

is not a specialization of the generic coercion `nat -> A`

, so it has its own theorems

#### Mario Carneiro (Mar 20 2019 at 11:36):

I think this one is `int.coe_nat_lt`

#### Kevin Buzzard (Mar 20 2019 at 11:41):

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/casts.md

Witness the asymmetry with nat -> int e.g.

import data.complex.basic example (q : ℕ) : (q : ℤ) = (3 : ℕ) → q = 3 := int.of_nat_inj example (q : ℕ) : (q : ℚ) = (3 : ℕ) → q = 3 := nat.cast_inj.1 example (q : ℕ) : (q : ℝ) = (3 : ℕ) → q = 3 := nat.cast_inj.1 example (q : ℕ) : (q : ℂ) = (3 : ℕ) → q = 3 := nat.cast_inj.1 example (q : ℤ) : (q : ℚ) = (3 : ℤ) → q = 3 := int.cast_inj.1 example (q : ℤ) : (q : ℝ) = (3 : ℤ) → q = 3 := int.cast_inj.1 example (q : ℤ) : (q : ℂ) = (3 : ℤ) → q = 3 := int.cast_inj.1 example (q : ℚ) : (q : ℝ) = (3 : ℚ) → q = 3 := rat.cast_inj.1 example (q : ℚ) : (q : ℂ) = (3 : ℚ) → q = 3 := rat.cast_inj.1 example (q : ℝ) : (q : ℂ) = (3 : ℝ) → q = 3 := complex.of_real_inj.1

The problem is that one of the constructors of int is `int.of_nat`

and so for reasons apparently to do with efficiency they use it as the coercion. Given that "efficiency" and "definition of nat" together imply an immediate contradiction, I've never seen the logic -- but then again IANACS...

#### Mario Carneiro (Mar 20 2019 at 11:42):

note that `nat`

is actually the most efficient VM natural numbers type, because of native support

#### Neil Strickland (Mar 20 2019 at 11:42):

Thanks. I now see that it also works to rewrite with `int.nat_cast_eq_coe_nat`

at an appropriate point.

#### Kevin Buzzard (Mar 20 2019 at 11:52):

Just in case you didn't know:

import tactic.linarith example (n : ℤ) (p : n ≥ 0) (q : n < 1) : n = 0 := by linarith

#### Gun Pinyo (Aug 11 2019 at 23:29):

Hi there, I have a question regarding coercion. Consider the following code:

section variables (n : ℕ) (i : fin n) #check (i : fin (n +1)) -- ↑i : fin (n +1) #reduce (infer_instance : has_coe (fin n) (fin (n +1))) -- error #reduce (i : fin (n +1)) -- nat.cast (i.val) end

I want to cast `i`

from `fin n`

to `fin (n +1)`

. This is fine using `(i : fin (n +1))`

.

The `#check`

mention `↑`

in which I believe it is something to `has_coe`

class so I dig deeper to understand the function behind it, however, it fails to find such an instance. At this point, I am really confused so I change `#check`

to `#reduce`

and get `nat.cast (i.val)`

.

My question is that why `#reduce`

successfully find the instance but `infer_instance`

doesn't. Is there another way to cast things without using `has_coe/has_lift`

?

#### Kevin Buzzard (Aug 11 2019 at 23:52):

What's the definition of nat.cast? Just right click on it in vs code and go to the definition, and it might give some insight into what's going on

#### Kevin Buzzard (Aug 11 2019 at 23:54):

Oh! Isn't this the function which defines a map from nat to any structure with zero and one and add or something? So maybe the cast is going via nat and isn'ta direct coercion

#### Mario Carneiro (Aug 12 2019 at 02:02):

There is no direct map from `fin n`

to `fin (n+1)`

, so `has_coe`

fails. However `has_coe_t`

probably succeeds and that's what the up arrow actually uses. As kevin says, the actual map goes via `nat`

Last updated: May 09 2021 at 20:11 UTC