feat: rify tactic (#7990)

Mathlib.lean

@@ -3319,6 +3319,7 @@ import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Replace
 import Mathlib.Tactic.RewriteSearch
 import Mathlib.Tactic.Rewrites
+import Mathlib.Tactic.Rify
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Ring.Basic
 import Mathlib.Tactic.Ring.PNat

Mathlib/Data/Rat/Cast/Defs.lean

@@ -47,6 +47,10 @@ theorem cast_coe_nat (n : ℕ) : ((n : ℚ) : α) = n := by
   rw [← Int.cast_ofNat, cast_coe_int, Int.cast_ofNat]
 #align rat.cast_coe_nat Rat.cast_coe_nat
 
+-- See note [no_index around OfNat.ofNat]
+@[simp, norm_cast] lemma cast_ofNat (n : ℕ) [n.AtLeastTwo] :
+    ((no_index (OfNat.ofNat n : ℚ)) : α) = (OfNat.ofNat n : α) := by
+  simp [cast_def]
 
 @[simp, norm_cast]
 theorem cast_zero : ((0 : ℚ) : α) = 0 :=

Mathlib/Data/Rat/Floor.lean

@@ -79,9 +79,7 @@ theorem ceil_cast (x : ℚ) : ⌈(x : α)⌉ = ⌈x⌉ := by
 
 @[simp, norm_cast]
 theorem round_cast (x : ℚ) : round (x : α) = round x := by
-  -- Porting note: `simp` worked rather than `simp [H]` in mathlib3
-  have H : ((2 : ℚ) : α) = (2 : α) := Rat.cast_coe_nat 2
-  have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp [H]
+  have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp
   rw [round_eq, round_eq, ← this, floor_cast]
 #align rat.round_cast Rat.round_cast
 

Mathlib/Tactic.lean

@@ -137,6 +137,7 @@ import Mathlib.Tactic.RenameBVar
 import Mathlib.Tactic.Replace
 import Mathlib.Tactic.RewriteSearch
 import Mathlib.Tactic.Rewrites
+import Mathlib.Tactic.Rify
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Ring.Basic
 import Mathlib.Tactic.Ring.PNat

Mathlib/Tactic/Attr/Register.lean

@@ -40,11 +40,15 @@ register_simp_attr parity_simps
 /-- "Simp attribute for lemmas about `IsROrC`" -/
 register_simp_attr isROrC_simps
 
-/-- The simpset `qify_simps` is used by the tactic `qify` to moved expression from `ℕ` or `ℤ` to `ℚ`
+/-- The simpset `rify_simps` is used by the tactic `rify` to move expressions from `ℕ`, `ℤ`, or
+`ℚ` to `ℝ`. -/
+register_simp_attr rify_simps
+
+/-- The simpset `qify_simps` is used by the tactic `qify` to move expressions from `ℕ` or `ℤ` to `ℚ`
 which gives a well-behaved division. -/
 register_simp_attr qify_simps
 
-/-- The simpset `zify_simps` is used by the tactic `zify` to moved expression from `ℕ` to `ℤ`
+/-- The simpset `zify_simps` is used by the tactic `zify` to move expressions from `ℕ` to `ℤ`
 which gives a well-behaved subtraction. -/
 register_simp_attr zify_simps
 

Mathlib/Tactic/Rify.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2023 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll, Mario Carneiro, Robert Y. Lewis, Patrick Massot
+-/
+import Mathlib.Tactic.Qify
+import Mathlib.Data.Real.Basic
+
+/-!
+# `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.
+-/
+
+namespace Mathlib.Tactic.Rify
+
+open Lean
+open Lean.Meta
+open Lean.Parser.Tactic
+open Lean.Elab.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`.
+```
+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). -/
+syntax (name := rify) "rify" (simpArgs)? (location)? : tactic
+
+macro_rules
+| `(tactic| rify $[[$simpArgs,*]]? $[at $location]?) =>
+  let args := simpArgs.map (·.getElems) |>.getD #[]
+  `(tactic|
+    simp (config := {decide := false}) only [zify_simps, qify_simps, rify_simps, push_cast, $args,*]
+      $[at $location]?)
+
+@[rify_simps] lemma rat_cast_eq (a b : ℚ) : a = b ↔ (a : ℝ) = (b : ℝ) := by simp
+@[rify_simps] lemma rat_cast_le (a b : ℚ) : a ≤ b ↔ (a : ℝ) ≤ (b : ℝ) := by simp
+@[rify_simps] lemma rat_cast_lt (a b : ℚ) : a < b ↔ (a : ℝ) < (b : ℝ) := by simp
+@[rify_simps] lemma rat_cast_ne (a b : ℚ) : a ≠ b ↔ (a : ℝ) ≠ (b : ℝ) := by simp
+
+-- See note [no_index around OfNat.ofNat]
+@[rify_simps] lemma ofNat_rat_real (a : ℕ) [a.AtLeastTwo] :
+    ((no_index (OfNat.ofNat a : ℚ)) : ℝ) = (OfNat.ofNat a : ℝ) := rfl

Mathlib/Tactic/Zify.lean

@@ -5,6 +5,8 @@ Authors: Moritz Doll, Mario Carneiro, Robert Y. Lewis
 -/
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Attr.Register
+import Mathlib.Data.Int.Cast.Basic
+import Mathlib.Order.Basic
 
 /-!
 # `zify` tactic
@@ -99,3 +101,16 @@ def zifyProof (simpArgs : Option (Syntax.TSepArray `Lean.Parser.Tactic.simpStar
 @[zify_simps] lemma nat_cast_dvd (a b : Nat) : a ∣ b ↔ (a : Int) ∣ (b : Int) := Int.ofNat_dvd.symm
 -- TODO: is it worth adding lemmas for Prime and Coprime as well?
 -- Doing so in this file would require adding imports.
+
+
+-- `Nat.cast_sub` is already tagged as `norm_cast` but it does allow to use assumptions like
+-- `m < n` or more generally `m + k ≤ n`. We add two lemmas to increase the probability that
+-- `zify` will push through `ℕ` subtraction.
+
+variable {R : Type*} [AddGroupWithOne R]
+
+@[norm_cast] theorem Nat.cast_sub_of_add_le {m n k} (h : m + k ≤ n) :
+    ((n - m : ℕ) : R) = n - m := Nat.cast_sub (m.le_add_right k |>.trans h)
+
+@[norm_cast] theorem Nat.cast_sub_of_lt {m n} (h : m < n) :
+    ((n - m : ℕ) : R) = n - m := Nat.cast_sub h.le

test/Rify.lean

@@ -0,0 +1,36 @@
+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
+
+example {n : ℕ} {k : ℤ} (hn : 8 ≤ n) (hk : (2 : ℚ) * k ≤ n + 2) :
+    (0 : ℝ) < n - k - 1 := by
+  rify at hn hk
+  linarith
+
+example (a b c : ℕ) (h : a - b < c) (hab : b ≤ a) : a < b + c := by
+  rify [hab] at h ⊢
+  linarith
+
+example {n : ℕ} (h : 8 ≤ n) : (0 : ℝ) < n - 1 := by
+  rify at h
+  linarith
+
+example {n k : ℕ} (h : 2 * k ≤ n + 2) (h' : 8 ≤ n) : (0 : ℝ) ≤ 3 * n - 4 - 4 * k := by
+  rify at *
+  linarith
+
+example {n k : ℕ} (h₁ : 8 ≤ n) (h₂ : 2 * k > n) (h₃: k + 1 < n) :
+    n - (k + 1) + 3 ≤ n := by
+  rify [h₃] at *
+  linarith
+
+example {n k : ℕ} (h₁ : 8 ≤ n) (h₂ : 2 * k > n) (h₃: k + 1 < n) :
+    n - (n - (k + 1)) = k + 1 := by
+  have f₁ : k + 1 ≤ n := by linarith
+  have f₂ : n - (k + 1) ≤ n := by rify [f₁]; linarith
+  rify [f₁, f₂] at *
+  linarith