## Stream: maths

### Topic: Issue using nat.cast_max

#### David A (Oct 15 2020 at 22:08):

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 (Oct 15 2020 at 22:25):

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 (Oct 15 2020 at 22:32):

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 (Oct 15 2020 at 22:41):

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 (Oct 15 2020 at 22:43):

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 (Oct 15 2020 at 22:44):

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

#### Gabriel Ebner (Oct 16 2020 at 07:58):

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 (Oct 16 2020 at 10:52):

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

#### Gabriel Ebner (Oct 16 2020 at 11:00):

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 (Oct 16 2020 at 11:58):

Ooh that would be really sweet.

#### Johan Commelin (Oct 16 2020 at 11:58):

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

#### Johan Commelin (Oct 16 2020 at 11:59):

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 (Oct 16 2020 at 15:41):

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

#### Mario Carneiro (Oct 16 2020 at 15:42):

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

#### Reid Barton (Oct 16 2020 at 15:42):

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

#### Mario Carneiro (Oct 16 2020 at 15:43):

that would only work if you have the right namespace open

#### Reid Barton (Oct 16 2020 at 15:43):

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

#### Reid Barton (Oct 16 2020 at 15:43):

however, the second issue seems more serious

#### Mario Carneiro (Oct 16 2020 at 15:43):

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

#### Mario Carneiro (Oct 16 2020 at 15:45):

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

#### Eric Wieser (Oct 16 2020 at 15:49):

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

#### Yury G. Kudryashov (Oct 16 2020 at 15:50):

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

#### Reid Barton (Oct 16 2020 at 15:51):

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

#### Reid Barton (Oct 16 2020 at 15:52):

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

#### Gabriel Ebner (Oct 16 2020 at 16:03):

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 (Oct 16 2020 at 16:05):

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.

Last updated: May 10 2021 at 06:13 UTC