zify broken?

Stream: mathlib4

[Scott Morrison]

@Moritz Doll, it seems we're missing some of the zify_simps lemmas. The example from the zify doc-string isn't working:

example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
  zify
  zify at h

[Scott Morrison]

The state should be

  h : ¬↑x * ↑y * ↑z < 0
  ⊢ ↑c < ↑a + 3 * ↑b

[Scott Morrison]

but it is

h: ¬↑(x * y * z) < 0
⊢ ↑c < ↑a + ↑(3 * b)

[Scott Morrison]

I guess this is push_cast lemmas missing, not zify_simps.

[Moritz Doll]

I would suspect that this is a push_cast problem, not specific to zify

[Scott Morrison]

Indeed, found missing @[norm_cast] attributes in an ad-hoc ported file.

[Scott Morrison]

Interesting, this is broken again/still:

import Mathlib.Tactic.Zify
import Mathlib.Data.Int.Basic
import Std.Tactic.GuardExpr

example (a b : ℕ) : a < 2 * b := by
  zify
  -- goal is: `↑a < ↑(2 * b)`
  push_cast
  -- goal is: `↑a < ↑(2 * b)`
  guard_target = (a : Int) < 2 * (b : Int)
  -- fails with: `target of main goal is ↑a < ↑(2 * b), not ↑a < 2 * ↑b`

Does anyone know what's going on here?

[Scott Morrison]

Has it been broken all the time since I noticed this last December?

[Scott Morrison]

Oh, I'm an idiot. Apparently I fixed this problem last night when upstreaming norm_cast to Std.

[Scott Morrison]

Who knows if Mathlib is compatible with the version I upstreamed, however. I guess I better check that.

[Scott Morrison]

std#351

[Scott Morrison]

Seems fine: #8222