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
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:
zifylemmas are used in the opposite order of the standard simp form. E.g. we will rewrite withint.coe_nat_le_coe_nat_ifffrom right to left.zifyshould fail if nozifylemma applies (i.e. it was unable to shift any proposition to ℤ). However, once this succeeds, it does not necessarily need to rewrite with anypush_castrules.
The zify attribute is used by the zify tactic. It applies to lemmas that shift propositions
between nat and int.
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.
Given an expression e, lift_to_z e looks for subterms of e that are propositions "about"
natural numbers and change them to propositions about integers.
Returns an expression e' and a proof that e = e'.
Includes ge_iff_le and gt_iff_lt in the simp set. These can't be tagged with zify as we
want to use them in the "forward", not "backward", direction.
zify extra_lems e is used to shift propositions in e from ℕ to ℤ.
This is often useful since ℤ has well-behaved subtraction.
The list of extra lemmas is used in the push_cast step.
Returns an expression e' and a proof that e = e'.
A variant of tactic.zify that takes h, a proof of a proposition about natural numbers,
and returns a proof of the zified version of that propositon.
The zify tactic is used to shift propositions from ℕ to ℤ.
This is often useful since ℤ has well-behaved subtraction.
example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b :=
begin
zify,
zify at h,
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
end
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 (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : false :=
begin
zify [hab] at h,
/- 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.