qify and division

Stream: mathlib4

[Kevin Buzzard]

What should qify do to statements of the form a = b / c with a,b,c naturals? Here is a proposal, which loses information but is sometimes more helpful than the status quo. The point is that if ↑a = ↑b / ↑c then a = b / c but not conversely.

import Mathlib

-- current state
example (a b c : ℕ) : a = b / c := by
  qify -- ⊢ (a : ℚ) = (((b : ℤ) / (c : ℤ) : ℤ) : ℚ)
  sorry

-- do we not have this?
lemma Nat.eq_div_of_cast_eq_div (a b c : ℕ) (h : (a : ℚ) = b / c) : a = b / c := by
  obtain rfl | hc := Nat.eq_zero_or_pos c
  · simp_all
  rw [eq_div_iff (by simp_all [hc.ne'])] at h
  norm_cast at h
  rw [← h, Nat.mul_div_cancel a hc]

-- should qify do this?
example (a b c : ℕ) : a = b / c := by
  apply Nat.eq_div_of_cast_eq_div
  -- ⊢ (a : ℚ) = (b : ℚ) / (c : ℚ)
  sorry

[Kevin Buzzard]

(the application was this where it makes it easier to prove $\sum_{i=1}^ni=n(n+1)/2$ where everything is formulated in terms of naturals; you can use tactics instead of having to rearrange a sum and then remembering what the lemma (a + 2 * b) / 2 = a / 2 + b is called)

[Ruben Van de Velde]

Hmm, I think qify and similar tactics currently never turn a provable goal into one that isn't provable. That seems like a good invariant to keep. But maybe yours could work as qify!?

[Kevin Buzzard]

Yes, I think qify is basically a simp set right now I think; I like the idea of the qify! variant.