# Zulip Chat Archive

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