Documentation

Mathlib.Tactic.Qify

qify tactic #

The qify tactic is used to shift propositions from or to . This is often useful since has well-behaved division.

example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
  qify
  qify at h
  /-
  h : ¬↑x * ↑y * ↑z < 0
  ⊢ ↑c < ↑a + 3 * ↑b
  -/
  sorry

The qify tactic is used to shift propositions from or to . This is often useful since has well-behaved division.

example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
  qify
  qify at h
  /-
  h : ¬↑x * ↑y * ↑z < 0
  ⊢ ↑c < ↑a + 3 * ↑b
  -/
  sorry

qify 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) (hb : b ≠ 0) : a = c * b := by
  qify [hab] at h hb ⊢
  exact (div_eq_iff hb).1 h

qify makes use of the @[zify_simps] and @[qify_simps] attributes to move propositions, and the push_cast tactic to simplify the -valued expressions.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Mathlib.Tactic.Qify.intCast_eq (a : ) (b : ) :
    a = b a = b
    theorem Mathlib.Tactic.Qify.intCast_le (a : ) (b : ) :
    a b a b
    theorem Mathlib.Tactic.Qify.intCast_lt (a : ) (b : ) :
    a < b a < b
    theorem Mathlib.Tactic.Qify.intCast_ne (a : ) (b : ) :
    a b a b
    @[deprecated Mathlib.Tactic.Qify.intCast_ne]
    theorem Mathlib.Tactic.Qify.int_cast_ne (a : ) (b : ) :
    a b a b

    Alias of Mathlib.Tactic.Qify.intCast_ne.