mathlib3 documentation

tactic.qify

A tactic to shift ℕ or ℤ goals to ℚ #

Note that this file is following from zify.

Division in ℕ and ℤ is not always working fine (e.g. (5 : ℕ) / 2 = 2), so it's easier to work in ℚ, where division and subtraction are well behaved. qify can be used to cast goals and hypotheses about natural numbers or integers to rational numbers. It makes use of push_cast, part of the norm_cast family, to simplify these goals.

Implementation notes #

qify is extensible, using the attribute @[qify] to label lemmas used for moving propositions from ℕ or ℤ to ℚ. qify lemmas should have the form ∀ a₁ ... aₙ : ℕ, Pq (a₁ : ℚ) ... (aₙ : ℚ) ↔ Pn a₁ ... aₙ. For example, rat.coe_nat_le_coe_nat_iff : ∀ (m n : ℕ), ↑m ≤ ↑n ↔ m ≤ n is a qify lemma.

qify is very nearly just simp only with qify push_cast. There are a few minor differences:

source
meta def qify.qify_attr  :
(user_attribute simp_lemmas)

The qify attribute is used by the qify tactic. It applies to lemmas that shift propositions from nat or int to rat.

qify lemmas should have the form ∀ a₁ ... aₙ : ℕ, Pq (a₁ : ℚ) ... (aₙ : ℚ) ↔ Pn a₁ ... aₙ or ∀ a₁ ... aₙ : ℤ, Pq (a₁ : ℚ) ... (aₙ : ℚ) ↔ Pz a₁ ... aₙ. For example, rat.coe_nat_le_coe_nat_iff : ∀ (m n : ℕ), ↑m ≤ ↑n ↔ m ≤ n is a qify lemma.

source
meta def qify.lift_to_q (e : expr) :
tactic (expr × expr)

Given an expression e, lift_to_q e looks for subterms of e that are propositions "about" natural numbers or integers and change them to propositions about rational numbers.

Returns an expression e' and a proof that e = e'.

Includes ge_iff_le and gt_iff_lt in the simp set. These can't be tagged with qify as we want to use them in the "forward", not "backward", direction.

source
theorem qify.rat.coe_nat_le_coe_nat_iff (a b : ℕ) :
↑a ≤ ↑b ↔ a ≤ b
source
theorem qify.rat.coe_nat_lt_coe_nat_iff (a b : ℕ) :
↑a < ↑b ↔ a < b
source
theorem qify.rat.coe_nat_eq_coe_nat_iff (a b : ℕ) :
↑a = ↑b ↔ a = b
source
theorem qify.rat.coe_nat_ne_coe_nat_iff (a b : ℕ) :
↑a ≠ ↑b ↔ a ≠ b
source
theorem qify.rat.coe_int_le_coe_int_iff (a b : ℤ) :
↑a ≤ ↑b ↔ a ≤ b
source
theorem qify.rat.coe_int_lt_coe_int_iff (a b : ℤ) :
↑a < ↑b ↔ a < b
source
theorem qify.rat.coe_int_eq_coe_int_iff (a b : ℤ) :
↑a = ↑b ↔ a = b
source
theorem qify.rat.coe_int_ne_coe_int_iff (a b : ℤ) :
↑a ≠ ↑b ↔ a ≠ b
source
meta def tactic.qify (extra_lems : list tactic.simp_arg_type) :
expr → tactic (expr × expr)

qify extra_lems e is used to shift propositions in e from ℕ or ℤ to ℚ. This is often useful since ℚ has well-behaved division and subtraction.

The list of extra lemmas is used in the push_cast step.

Returns an expression e' and a proof that e = e'.

source
meta def tactic.qify_proof (extra_lems : list tactic.simp_arg_type) (h : expr) :
tactic expr

A variant of tactic.qify that takes h, a proof of a proposition about natural numbers or integers, and returns a proof of the qified version of that propositon.

source
meta def tactic.interactive.qify (sl : interactive.parse tactic.simp_arg_list) (l : interactive.parse interactive.types.location) :
tactic unit

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

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

qify can be given extra lemmas to use in simplification. This is especially useful in the presence of subtraction and division: passing ≤ or ∣ arguments will allow push_cast to do more work.

example (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : false :=
begin
  qify [hab] at h,
  /- h : ↑a - ↑b < ↑c -/
end

example (a b c : ℕ) (h : a / b = c) (hab : b ∣ a) : false :=
begin
  qify [hab] at h,
  /- h : ↑a / ↑b = ↑c -/
end

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

source
def tactic_doc.attribute.qify  :
tactic_doc_entry

The qify attribute is used by the qify tactic. It applies to lemmas that shift propositions from nat or int to rat.

qify lemmas should have the form ∀ a₁ ... aₙ : ℕ, Pq (a₁ : ℚ) ... (aₙ : ℚ) ↔ Pn a₁ ... aₙ or ∀ a₁ ... aₙ : ℤ, Pq (a₁ : ℚ) ... (aₙ : ℚ) ↔ Pz a₁ ... aₙ. For example, rat.coe_nat_le_coe_nat_iff : ∀ (m n : ℕ), ↑m ≤ ↑n ↔ m ≤ n is a qify lemma.

source
def tactic_doc.tactic.qify  :
tactic_doc_entry

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

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

qify can be given extra lemmas to use in simplification. This is especially useful in the presence of subtraction and division: passing ≤ or ∣ arguments will allow push_cast to do more work.

example (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : false :=
begin
  qify [hab] at h,
  /- h : ↑a - ↑b < ↑c -/
end

example (a b c : ℕ) (h : a / b = c) (hab : b ∣ a) : false :=
begin
  qify [hab] at h,
  /- h : ↑a / ↑b = ↑c -/
end

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