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:

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.

meta def zify.lift_to_z (e : 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.

theorem int.coe_nat_ne_coe_nat_iff (a b : ) :
a b a b
meta def tactic.zify (extra_lems : list tactic.simp_arg_type) :

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

meta def tactic.zify_proof (extra_lems : list tactic.simp_arg_type) (h : 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.

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.