nat.cast diamond

Stream: general

[Yaël Dillies]

Yet another diamond involving nat.cast...

import data.nat.cast

example (n : ℕ) : (nat.cast n : ℤ) = n :=
begin
  refl, --fails
end

[Yury G. Kudryashov]

AFAIR, we have a simp lemma for this.

[Yaël Dillies]

The culprit is docs#int.has_coe. Should we nuke it?

[Yury G. Kudryashov]

See docs#nat_cast_eq_coe_nat

[Yaël Dillies]

For context, when @Johan Commelin stumbled on the problem with enat, we decided to delete the enat-specific coercion.

[Yury G. Kudryashov]

This won't solve

example (n : ℕ) : (↑n : ℕ) = n := rfl -- fails

[Yaël Dillies]

What about we delete ℕ?

[Yury G. Kudryashov]

One way to deal with this is to include of_nat into the signature of semiring and restrict nat.cast to semirings.

[Johan Commelin]

It's going to be a royal PITA to do that refactor, but it's the logical extension of what we've been doing already.

[Yakov Pechersky]

At that point, you might as well use nat.bin_cast since you have all the proofs that they're the same, given your semiring.

[Yury G. Kudryashov]

Then we'll loose defeq ↑(n + 1) = ↑n + 1.

[Yury G. Kudryashov]

And you can use int.has_coe for integers, id for naturals.

[Yaël Dillies]

So no nat.cast for monoids anymore?

[Yury G. Kudryashov]

Are there examples of add_monoid + has_one but no semiring where we care about nat.cast?

[Yakov Pechersky]

Games?

[Yakov Pechersky]

I don't remember if it's pregames or games

[Yakov Pechersky]

I just remember proving that nat.bin_cast does the right thing for them was brutal. I don't remember if I even finished that.

[Yury G. Kudryashov]

You can have a separate has_coe instance in this case.

[Yury G. Kudryashov]

Most properties of nat.cast follow from it being an add_monoid_hom.

[Johan Commelin]

Otoh, I don't really care about whether ↑n is defeq to n. What I do care about, is that all the coercions from ℕ to ℤ are defeq.

[Yakov Pechersky]

I understand the reason to put nsmul and gsmul into the typeclass, to make typeclass inference and unification work better, because we can't provide proofs to the TC resolver. But what TC issue is there here?

[Yakov Pechersky]

In general, it has seemed that we avoid making things rfl proofs, because that just hides complexity.

[Yaël Dillies]

We have a generic coercion from ℕ to any unital add_monoidand a specific one from ℕ to ℤ.

[Johan Commelin]

I'm inclined to nuke the specific coe from ℕ to ℤ. If people want a map ℕ → ℤ that computes well, they can call it by name, instead of using the coe.

[Sebastien Gouezel]

Why not just kill the specific one?

[Johan Commelin]

But I understand that this is a very mathsy opinion.

[Sebastien Gouezel]

You just beat me to it :-)

[Johan Commelin]

I think @Mario Carneiro was strongly in favour of keeping the specific coe around.

[Mario Carneiro]

The issue with exponential time coes is bad enough already. This would just make that get secretly used all over the place, causing pain and suffering for anyone with lean 3 code that we aren't actively monitoring

[Eric Wieser]

We could add of_nat : has_one α → ℕ → α to add_monoid?

[Yaël Dillies]

That sounds like a good tradeof.

[Yury G. Kudryashov]

@Eric Wieser I think that the better way is to add add_monoid_with_one.

[Yury G. Kudryashov]

If you add of_nat : has_one α → ℕ → α with appropriate axioms, then you won't be able to ignore the has_one argument in the case α = int.

[Eric Wieser]

Yury G. Kudryashov said:

Eric Wieser I think that the better way is to add add_monoid_with_one.

But then you also might need add_comm_monoid_with_one, add_cancel_comm_monoid_with_one, add_group_with_one, ...