# `rify` tactic #

The `rify` tactic is used to shift propositions from `ℕ`, `ℤ` or `ℚ` to `ℝ`.

Although less useful than its cousins `zify` and `qify`, it can be useful when your goal or context already involves real numbers.

In the example below, assumption `hn` is about natural numbers, `hk` is about integers and involves casting a natural number to `ℤ`, and the conclusion is about real numbers. The proof uses `rify` to lift both assumptions to `ℝ` before calling `linarith`.

    import Mathlib.Tactic.Linarith
    import Mathlib.Tactic.Rify

    example {n : ℕ} {k : ℤ} (hn : 8 ≤ n) (hk : 2 * k ≤ n + 2) :
        (0 : ℝ) < n - k - 1 := by
      rify at hn hk
      linarith

TODO: Investigate whether we should generalize this to other fields.

source
def Mathlib.Tactic.Rify.rify :
Lean.ParserDescr

The `rify` tactic is used to shift propositions from `ℕ`, `ℤ` or `ℚ` to `ℝ`. Although less useful than its cousins `zify` and `qify`, it can be useful when your goal or context already involves real numbers.

In the example below, assumption `hn` is about natural numbers, `hk` is about integers and involves casting a natural number to `ℤ`, and the conclusion is about real numbers. The proof uses `rify` to lift both assumptions to `ℝ` before calling `linarith`.

    example {n : ℕ} {k : ℤ} (hn : 8 ≤ n) (hk : 2 * k ≤ n + 2) :
        (0 : ℝ) < n - k - 1 := by
      rify at hn hk /- Now have hn : 8 ≤ (n : ℝ)   hk : 2 * (k : ℝ) ≤ (n : ℝ) + 2 -/
      linarith

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

`rify` 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) : a < b + c := by
      rify [hab] at h ⊢
      linarith

Note that `zify` or `qify` would work just as well in the above example (and `zify` is the natural choice since it is enough to get rid of the pathological `ℕ` subtraction).

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Mathlib.Tactic.Rify.ratCast_eq (a b : ℚ) :
a = b ↔ ↑a = ↑b
source
theorem Mathlib.Tactic.Rify.ratCast_le (a b : ℚ) :
a ≤ b ↔ ↑a ≤ ↑b
source
theorem Mathlib.Tactic.Rify.ratCast_lt (a b : ℚ) :
a < b ↔ ↑a < ↑b
source
theorem Mathlib.Tactic.Rify.ratCast_ne (a b : ℚ) :
a ≠ b ↔ ↑a ≠ ↑b
source
theorem Mathlib.Tactic.Rify.ofNat_rat_real (a : ℕ) [a.AtLeastTwo] :
↑(OfNat.ofNat a) = OfNat.ofNat a