mathlib documentation

tactic.zify

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:

source
meta def zify.zify_attr  :
(user_attribute simp_lemmas)

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.

source
meta def zify.lift_to_z (e : expr) :
tactic (expr × expr)

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.

source
theorem int.coe_nat_ne_coe_nat_iff (a b : ℕ) :
↑a ≠ ↑b ↔ a ≠ b
source
meta def tactic.zify (extra_lems : list tactic.simp_arg_type) :
expr → tactic (expr × expr)

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'.

source
meta def tactic.zify_proof (extra_lems : list tactic.simp_arg_type) (h : expr) :
tactic expr

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.

source
meta def tactic.interactive.zify (sl : interactive.parse tactic.simp_arg_list) (l : interactive.parse interactive.types.location) :
tactic unit

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.