Cast weirdness

Stream: new members

[Neil Strickland]

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]

The coercion nat -> int is not a specialization of the generic coercion nat -> A, so it has its own theorems

[Mario Carneiro]

I think this one is int.coe_nat_lt

[Kevin Buzzard]

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]

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

[Neil Strickland]

Thanks. I now see that it also works to rewrite with int.nat_cast_eq_coe_nat at an appropriate point.

[Kevin Buzzard]

Just in case you didn't know:

import tactic.linarith

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

[Gun Pinyo]

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]

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]

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]

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