# `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
      -/

source
def Mathlib.Tactic.Zify.zify :
Lean.ParserDescr

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

source
def Mathlib.Tactic.Zify.mkZifyContext (simpArgs : Option (Lean.Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",")) :
Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.MkSimpContextResult

The `Simp.Context` generated by `zify`.

Equations

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

Instances For

source
def Mathlib.Tactic.Zify.applySimpResultToProp' (proof prop : Lean.Expr) (r : Lean.Meta.Simp.Result) :
Lean.MetaM (Lean.Expr × Lean.Expr)

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

source
def Mathlib.Tactic.Zify.zifyProof (simpArgs : Option (Lean.Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",")) (proof prop : Lean.Expr) :
Lean.Elab.Tactic.TacticM (Lean.Expr × 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

source
theorem Mathlib.Tactic.Zify.natCast_eq (a b : ℕ) :
a = b ↔ ↑a = ↑b
source
theorem Mathlib.Tactic.Zify.natCast_le (a b : ℕ) :
a ≤ b ↔ ↑a ≤ ↑b
source
theorem Mathlib.Tactic.Zify.natCast_lt (a b : ℕ) :
a < b ↔ ↑a < ↑b
source
theorem Mathlib.Tactic.Zify.natCast_ne (a b : ℕ) :
a ≠ b ↔ ↑a ≠ ↑b
source
theorem Mathlib.Tactic.Zify.natCast_dvd (a b : ℕ) :
a ∣ b ↔ ↑a ∣ ↑b
source
theorem Mathlib.Tactic.Zify.Nat.cast_sub_of_add_le {R : Type u_1} [AddGroupWithOne R] {m n k : ℕ} (h : m + k ≤ n) :
↑(n - m) = ↑n - ↑m
source
theorem Mathlib.Tactic.Zify.Nat.cast_sub_of_lt {R : Type u_1} [AddGroupWithOne R] {m n : ℕ} (h : m < n) :
↑(n - m) = ↑n - ↑m