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.

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.

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.