zify bugs?

Stream: mathlib4

[Rob Lewis]

@Heather Macbeth and I have come across a few issues with zify, sometimes in relation to other tactics. I'm not up to speed on Lean 4 numerals and not sure how to fix these.

import import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.Zify

example (a b : ℕ) (h1 : a + b = 4) : a = 4 + 1 := by
  zify -- turns the 4 into 1 + 1 + 1 + 1
  sorry

example (a : ℕ) :
 1 = (1 + 1) * a := by
   ring_nf -- if this is `norm_num` instead, replicates the above
   zify -- leaves a coercion ℤ → ℕ on the numeral 2


example (a b : ℕ) (h1 : a + b = 4) : (a:ℤ) + b + 1 = 4 + 1 := by
  zify at h1
  linear_combination h1
/-
synthetic hole has already been defined and assigned to value incompatible with the current context
  h1
-/

Any thoughts on these?

[Shreyas Srinivas]

This might be relevant here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/data.2Enat.2Efib.20mathlib4.231644/near/322189239

[Moritz Doll]

to me it sounds like there is a missing norm_cast attribute for the numeral coercion. Probably you can reduce the problem to a norm_cast bug

[Shreyas Srinivas]

I can't see where norm_cast lemmas have been called in the lean 4 version of zify. In lean3 there is a line doing something with norm_cast lemmas. Are they summoned indirectly in the lean4 version? I had an issue where lemmas labelled norm_cast weren't applied (see linked thread) in lean 4 while the equivalent in lean 3 seems to have done so

[Shreyas Srinivas]

(deleted)

[Moritz Doll]

it is the push_cast in the macro. It uses the pushCastExt simpAttr, so one reason why zify does not use a lemma that has been labelled as norm_cast is that there might be something worng in how the norm_cast attribute creates the push_cast simpAttr:
https://github.com/leanprover/std4/blob/5770b609aeae209cb80ac74655ee8c750c12aabd/Std/Tactic/NormCast/Ext.lean#L115