zify mathlib4#517

Stream: mathlib4

[Scott Morrison]

I'm keen to get @Moritz Doll's port of zify in, but I'm having trouble with a casting issue.

By adding some norm_cast attributes, I got the mathlib3 tests to work.

However, if you add imports to the test file so that the CommRing ℤ instance becomes available, things fail again! Here's my summary from github:

---

Okay, so we need to import Mathlib.Init.Data.Int.Basic, in order to get the Preorder ℤ instance. However as soon as the CommRing ℤ instance is available, which is currently defined in Mathlib.Algebra.Ring.Basic, the tests start failing again.

In

example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) (h2 : (c : ℤ) < a + 3 * b) : a + 3*b > c := by
  zify at h ⊢
  push_cast at h
  guard_hyp h : ¬↑x * ↑y * ↑z < (0 : ℤ)
  guard_target =ₐ ↑c < (↑a : ℤ) + 3 * ↑b
  exact h2

which right now succeeds in this branch, after adding the import (and hence the CommRing ℤ instance), we get

hypothesis h has type ¬↑x * ↑y * ↑z < 0, not ¬↑x * ↑y * ↑z < 0

Here the first ↑x is Int.ofNat x : ℤ, while the other ↑x is @Nat.cast ℤ NonUnitalNonAssocSemiring.toAddMonoidWithOne x : ℤ.

---

I'm not sure what the appropriate resolution of this is, so if someone who understands how casts are meant to work in Lean 4 wants to help out here, that would be great. :-)

[Mario Carneiro]

I believe the intention is for Nat.cast to take precedence over Int.ofNat in mathlib once the former is available. It should have a precedence such that this happens consistently, and there is a simp lemma rewriting ofNat to Nat.cast IIRC

[Moritz Doll]

Thanks Scott for looking into this.
When I wrote the tests, I thought that the Int.ofNat cast lemmas were not tagged as norm_cast in mathlib3 and this was the reason why I did not add them, but now I see that I was wrong.