A tactic to shift
ℕ goals to
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.
Implementation notes #
zify is extensible, using the attribute
@[zify] to label lemmas used for moving propositions
zify lemmas should have the form
∀ a₁ ... aₙ : ℕ, Pz (a₁ : ℤ) ... (aₙ : ℤ) ↔ Pn a₁ ... aₙ.
int.coe_nat_le_coe_nat_iff : ∀ (m n : ℕ), ↑m ≤ ↑n ↔ m ≤ n is a
zify is very nearly just
simp only with zify push_cast. There are a few minor differences:
zifylemmas are used in the opposite order of the standard simp form. E.g. we will rewrite with
int.coe_nat_le_coe_nat_ifffrom right to left.
zifyshould fail if no
zifylemma applies (i.e. it was unable to shift any proposition to ℤ). However, once this succeeds, it does not necessarily need to rewrite with any