# Documentation

Mathlib.Tactic.Zify

# zify tactic #

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 := by
zify
zify at h
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
¬ x*y*z < 0) : c < a + 3*b := by
zify
zify at h
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
⊢ ↑c < ↑a + 3 * ↑b
-/
↑c < ↑a + 3 * ↑b
-/
↑a + 3 * ↑b
-/
↑b
-/


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 := by
zify
zify at h
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
¬ x*y*z < 0) : c < a + 3*b := by
zify
zify at h
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/
⊢ ↑c < ↑a + 3 * ↑b
-/
↑c < ↑a + 3 * ↑b
-/
↑a + 3 * ↑b
-/
↑b
-/


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 := by
zify [hab] at h
/- h : ↑a - ↑b < ↑c -/
≤ a) : false := by
zify [hab] at h
/- h : ↑a - ↑b < ↑c -/
↑a - ↑b < ↑c -/
↑b < ↑c -/
↑c -/


zify makes use of the @[zify_simps] 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≥ 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.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Tactic.Zify.mkZifyContext (simpArgs : Option (Lean.Syntax.TSepArray Lean.Parser.Tactic.simpStar ",")) :

The Simp.Context generated by zify.

Equations
• One or more equations did not get rendered due to their size.

A variant of applySimpResultToProp that cannot close the goal, but does not need a meta variable and returns a tuple of a proof and the corresponding simplified proposition.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Tactic.Zify.zifyProof (simpArgs : Option (Lean.Syntax.TSepArray Lean.Parser.Tactic.simpStar ",")) (proof : Lean.Expr) (prop : Lean.Expr) :

Translate a proof and the proposition into a zified form.

Equations
• One or more equations did not get rendered due to their size.
theorem Mathlib.Tactic.Zify.nat_cast_eq (a : ) (b : ) :
a = b a = b
theorem Mathlib.Tactic.Zify.nat_cast_le (a : ) (b : ) :
a b a b
theorem Mathlib.Tactic.Zify.nat_cast_lt (a : ) (b : ) :
a < b a < b
theorem Mathlib.Tactic.Zify.nat_cast_ne (a : ) (b : ) :
a b a b