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
  • One or more equations did not get rendered due to their size.
Instances For

    The Simp.Context generated by zify.

    Equations
    • One or more equations did not get rendered due to their size.
    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
      • One or more equations did not get rendered due to their size.
      Instances For
        def Mathlib.Tactic.Zify.zifyProof (simpArgs : Option (Lean.Syntax.TSepArray `Lean.Parser.Tactic.simpStar ",")) (proof : Lean.Expr) (prop : 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
          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
          @[deprecated Mathlib.Tactic.Zify.natCast_dvd]
          theorem Mathlib.Tactic.Zify.nat_cast_dvd (a : ) (b : ) :
          a b a b

          Alias of Mathlib.Tactic.Zify.natCast_dvd.

          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