Documentation

Mathlib.Tactic.Zify

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.

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.

    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.

      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.

        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
          @[deprecated "use Nat.cast_sub" (since := "2026-02-21")]
          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