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.

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