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:

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.