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:

• qify lemmas are used in the opposite order of the standard simp form. E.g. we will rewrite with rat.coe_nat_le_coe_nat_iff from right to left.
• qify should fail if no qify lemma applies (i.e. it was unable to shift any proposition to ℚ). However, once this succeeds, it does not necessarily need to rewrite with any push_cast rules.
meta def qify.qify_attr  :

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.

meta def qify.lift_to_q (e : 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.

theorem qify.rat.coe_nat_lt_coe_nat_iff (a b : ) :
a < b a < b
theorem qify.rat.coe_nat_eq_coe_nat_iff (a b : ) :
a = b a = b
theorem qify.rat.coe_int_lt_coe_int_iff (a b : ) :
a < b a < b
theorem qify.rat.coe_int_eq_coe_int_iff (a b : ) :
a = b a = b
meta def tactic.qify (extra_lems : list tactic.simp_arg_type) :

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'.

meta def tactic.qify_proof (extra_lems : list tactic.simp_arg_type) (h : 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.

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.

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.

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.