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

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

      The Simp.Context generated by zify.

      Equations
        Instances For

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

              Translate a proof and the proposition into a zified form.

              Equations
                Instances For
                  theorem Mathlib.Tactic.Zify.natCast_eq (a b : ) :
                  a = b a = b
                  theorem Mathlib.Tactic.Zify.natCast_le (a b : ) :
                  a b a b
                  theorem Mathlib.Tactic.Zify.natCast_lt (a b : ) :
                  a < b a < b
                  theorem Mathlib.Tactic.Zify.natCast_ne (a b : ) :
                  a b a b
                  theorem Mathlib.Tactic.Zify.natCast_dvd (a b : ) :
                  a b a b
                  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
                  theorem Mathlib.Tactic.Zify.Nat.cast_sub_of_lt {R : Type u_1} [AddGroupWithOne R] {m n : } (h : m < n) :
                  ↑(n - m) = n - m