It is often easier to work in ℤ, where subtraction is well behaved, than in ℕ where it isn't.
zify is a tactic that casts goals and hypotheses about natural numbers to ones about integers.
It makes use of push_cast, part of the norm_cast family, to simplify these goals.
zify is extensible, using the attribute @[zify] to label lemmas used for moving propositions
from ℕ to ℤ.
zify lemmas should have the form ∀ a₁ ... aₙ : ℕ, Pz (a₁ : ℤ) ... (aₙ : ℤ) ↔ Pn a₁ ... aₙ.
For example, int.coe_nat_le_coe_nat_iff : ∀ (m n : ℕ), ↑m ≤ ↑n ↔ m ≤ n is a zify lemma.
zify is very nearly just simp only with zify push_cast. There are a few minor differences:
zify lemmas are used in the opposite order of the standard simp form.
E.g. we will rewrite with int.coe_nat_le_coe_nat_iff from right to left.
zify should fail if no zify lemma applies (i.e. it was unable to shift any proposition to ℤ).
However, once this succeeds, it does not necessarily need to rewrite with any push_cast rules.
zify can be given extra lemmas to use in simplification. This is especially useful in the
presence of nat subtraction: passing ≤ arguments will allow push_cast to do more work.
example(abc:ℕ)(h:a-b<c)(hab:b≤a):false:=beginzify[hab]ath,/- h : ↑a - ↑b < ↑c -/end
zify makes use of the @[zify] attribute to move propositions,
and the push_cast tactic to simplify the ℤ-valued expressions.
zify is in some sense dual to the lift tactic. lift (z : ℤ) to ℕ will change the type of an
integer z (in the supertype) to ℕ (the subtype), given a proof that z ≥ 0;
propositions concerning z will still be over ℤ. zify changes propositions about ℕ (the
subtype) to propositions about ℤ (the supertype), without changing the type of any variable.