Zulip Chat Archive

Stream: maths

Topic: Issue using nat.cast_max


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 16 2020 at 11:58):

Ooh that would be really sweet.

view this post on Zulip Johan Commelin (Oct 16 2020 at 11:58):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 16 2020 at 15:41):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 16 2020 at 15:42):

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

view this post on Zulip Mario Carneiro (Oct 16 2020 at 15:43):

that would only work if you have the right namespace open

view this post on Zulip Reid Barton (Oct 16 2020 at 15:43):

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

view this post on Zulip Reid Barton (Oct 16 2020 at 15:43):

however, the second issue seems more serious

view this post on Zulip Mario Carneiro (Oct 16 2020 at 15:43):

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

view this post on Zulip Mario Carneiro (Oct 16 2020 at 15:45):

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

view this post on Zulip Eric Wieser (Oct 16 2020 at 15:49):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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