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

zify rewrites the main goal by shifting propositions from ℕ to ℤ. This is often useful since ℤ has well-behaved subtraction.

zify makes use of the @[zify_simps] attribute to insert casts into propositions, and the push_cast tactic to simplify the ℤ-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.

  • zify at l1 l2 ... rewrites at the given locations.
  • zify [h₁, ..., hₙ] uses the expressions h₁, ..., hₙ as extra lemmas for simplification. This is especially useful in the presence of nat subtraction or of division: passing arguments of type · ≤ · will allow push_cast to do more work.

Examples:

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
  -/
  sorry

example (a b c : Nat) (h : a - b < c) (hab : b ≤ a) : False := by
  -- Nonnegativity hypothesis allows pushing `· - ·`.
  zify [hab] at h
  /- h : ↑a - ↑b < ↑c -/
  sorry
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
          @[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