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
qify rewrites the main goal by shifting propositions from ℕ or ℤ to ℚ.
This is often useful since ℚ has well-behaved subtraction and division.
qify makes use of the @[zify_simps] and @[qify_simps] attributes to insert casts into
propositions, and the push_cast tactic to simplify the ℚ-valued expressions.
qify is in some sense dual to the lift tactic. lift (q : ℚ) to ℤ will change the type of a
rational number q (in the supertype) to ℤ (the subtype), given a proof that q.den = 1;
propositions concerning q will still be over ℚ. qify changes propositions about ℕ or ℤ
(the subtype) to propositions about ℚ (the supertype), without changing the type of any variable.
qify at l1 l2 ...rewrites at the given locations.qify [h₁, ..., hₙ]uses the expressionsh₁, ...,hₙas extra lemmas for simplification. This is especially useful in the presence of nat subtraction or of division: passing arguments of type· ≤ ·or· ∣ ·will allowpush_castto do more work.
Examples:
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
example (a b c : ℤ) (h : a / b = c) (hab : b ∣ a) (hb : b ≠ 0) : a = c * b := by
-- Divisibility hypothesis allows pushing `· / ·`.
qify [hab] at h hb ⊢
exact (div_eq_iff hb).1 h
Equations
- One or more equations did not get rendered due to their size.