## 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