Issue using nat.cast_max

Stream: maths

[David A]

I was looking for a library proof of

example (a b : ℕ) : ↑(max a b) = max (↑a : ℤ) (↑b : ℤ)

I (manually) found nat.cast_max which looks like it should do the trick. But both bare nat.cast_max and

example (a b : ℕ) : ↑(max a b) = max (↑a : ℤ) (↑b : ℤ)
  := @nat.cast_max int _ a b

give

type mismatch, term
  nat.cast_max
has type
  ↑(@max ℕ nat.decidable_linear_order a b) =
    @max ℤ
      (@decidable_linear_ordered_semiring.to_decidable_linear_order ℤ
         (@decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring ℤ
            int.decidable_linear_ordered_comm_ring))
      ↑a
      ↑b
but is expected to have type
  ↑(@max ℕ nat.decidable_linear_order a b) = @max ℤ int.decidable_linear_order ↑a ↑b

This seems like a bug because the mentioned types unify AFAICT. I see that it's supposed to be used by the tactic norm_cast but that tactic just fails here.

Is there any way around this and/or am I missing something here?

[Alex J. Best]

If you use convert you can see what lean thinks is the difference between the terms

example (a b : ℕ) :(↑ (max a b): ℤ)  = max (a : ℤ) (b : ℤ)
  := begin
    convert @nat.cast_max int _ a b,

  end

[Alex J. Best]

You can set

local attribute [instance, priority 850] coe_base

before this and it works fine, not sure why this is needed really though

[David A]

So... there are two non-defeq versions of nat -> int coercion? That seems... bad.
Anyways, this workaround does seem to help so thanks!

[David A]

Well... it kind of works. It leads to a bunch of other errors in previously-working code, so I think it has to be really scoped down.

[Alex J. Best]

Looks like @Gabriel Ebner was the last person to change this in #2573, perhaps he can shed some light on the matter.

[Gabriel Ebner]

Yes, there are two different coercions. IIRC the idea was that we standardize on int.has_coe for coercions from ℕ → ℤ. But then you can't use lemmas that are stated for the general coercion. :shrug:

example (a b : ℕ) : ↑(max a b) = max (↑a : ℤ) (↑b : ℤ) :=
begin
  rw [← int.nat_cast_eq_coe_nat, nat.cast_max,
    int.nat_cast_eq_coe_nat, int.nat_cast_eq_coe_nat]
end

[Kevin Buzzard]

Mario was always adamant that the coercion from nat to int had to be the constructor, for computational reasons.

[Gabriel Ebner]

Mmmh, nowadays we might be able to do this:

@[priority 9000, vm_override int.has_coe]
instance nat.better_int_coe : has_coe ℕ ℤ :=
⟨nat.cast⟩

[Johan Commelin]

Ooh that would be really sweet.

[Johan Commelin]

This coe problem was not as bad as nat.pow, but it comes close.

[Johan Commelin]

And now that nat.pow is gone, it's a serious contestant for claiming the free spot of "most annoying incompatibility in mathlib/lean"
Runner up is the fact that int.gcd doesn't match euclidean_domain.gcd

[Mario Carneiro]

I can't use pattern matching on | (n : nat) := ... | -[1+n] := ... though if we do this

[Mario Carneiro]

it would also silently break a lot of tactics by switching out a constant time implementation for an exponential time algorithm

[Reid Barton]

| (mk n) := ... :golf:

[Mario Carneiro]

that would only work if you have the right namespace open

[Reid Barton]

which you almost certainly do if you are writing | -[1+n]

[Reid Barton]

however, the second issue seems more serious

[Mario Carneiro]

I almost never open nat or int, there are too many conflicts

[Mario Carneiro]

It's already somewhat challenging to avoid accidentally hitting the exponential time nat -> rat coe

[Eric Wieser]

What do the [] mean in -[1+n]? I assume that's not a list constructor?

[Yury G. Kudryashov]

It's a notation for docs#int.neg_succ_of_nat, one of the constructors of docs#int

[Reid Barton]

doesn't @Gabriel Ebner's vm_override suggestion address the evaluation issue? If not then what does it do?

[Reid Barton]

Ideally, int would be implemented in the VM as mpz anyways (and maybe defined in Lean as a quotient)

[Gabriel Ebner]

int is implemented using mpz (or signed integers if they fit). The proposed instance has the right runtime complexity (unless I mixed up the order of the vm_override arguments).

[Gabriel Ebner]

Pattern matching still works on -[1+n] (the coercion doesn't even apply here??). Instead of (n : nat) you can just write int.of_nat n, as Reid pointed out.