# zify tactic #

The zify tactic is used to shift propositions from Nat to Int. This is often useful since Int has well-behaved subtraction.

example (a b c x y z : Nat) (h : ¬ x*y*z < 0) : c < a + 3*b := by
zify
zify at h
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑b
-/


The zify tactic is used to shift propositions from Nat to Int. This is often useful since Int has well-behaved subtraction.

example (a b c x y z : Nat) (h : ¬ x*y*z < 0) : c < a + 3*b := by
zify
zify at h
/-
h : ¬↑x * ↑y * ↑z < 0
⊢ ↑c < ↑a + 3 * ↑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 : Nat) (h : a - b < c) (hab : b ≤ a) : false := by
zify [hab] at h
/- h : ↑a - ↑b < ↑c -/


zify makes use of the @[zify_simps] attribute to move propositions, and the push_cast tactic to simplify the Int-valued expressions. zify is in some sense dual to the lift tactic. lift (z : Int) to Nat will change the type of an integer z (in the supertype) to Nat (the subtype), given a proof that z ≥ 0; propositions concerning z will still be over Int. zify changes propositions about Nat (the subtype) to propositions about Int (the supertype), without changing the type of any variable.

Equations
• One or more equations did not get rendered due to their size.
Instances For
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.
Instances For

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.
Instances For
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.
Instances For
theorem Mathlib.Tactic.Zify.natCast_eq (a : ) (b : ) :
a = b a = b
theorem Mathlib.Tactic.Zify.natCast_le (a : ) (b : ) :
a b a b
theorem Mathlib.Tactic.Zify.natCast_lt (a : ) (b : ) :
a < b a < b
theorem Mathlib.Tactic.Zify.natCast_ne (a : ) (b : ) :
a b a b
theorem Mathlib.Tactic.Zify.natCast_dvd (a : ) (b : ) :
a b a b
@[deprecated Mathlib.Tactic.Zify.natCast_dvd]
theorem Mathlib.Tactic.Zify.nat_cast_dvd (a : ) (b : ) :
a b a b

Alias of Mathlib.Tactic.Zify.natCast_dvd.

theorem Mathlib.Tactic.Zify.Nat.cast_sub_of_add_le {R : Type u_1} [] {m : } {n : } {k : } (h : m + k n) :
(n - m) = n - m
theorem Mathlib.Tactic.Zify.Nat.cast_sub_of_lt {R : Type u_1} [] {m : } {n : } (h : m < n) :
(n - m) = n - m