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
  -/
source
def Mathlib.Tactic.Zify.zify :
Lean.ParserDescr

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

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

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; 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.
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 : Lean.Expr) (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 : Lean.Expr) (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.nat_cast_eq (a : ℕ) (b : ℕ) :
          a = b ↔ ↑a = ↑b
          source
          theorem Mathlib.Tactic.Zify.nat_cast_le (a : ℕ) (b : ℕ) :
          a ≤ b ↔ ↑a ≤ ↑b
          source
          theorem Mathlib.Tactic.Zify.nat_cast_lt (a : ℕ) (b : ℕ) :
          a < b ↔ ↑a < ↑b
          source
          theorem Mathlib.Tactic.Zify.nat_cast_ne (a : ℕ) (b : ℕ) :
          a ≠ b ↔ ↑a ≠ ↑b