equivalent to zify for rationals

Stream: Is there code for X?

[Miguel Marco]

I am trying to prove some equalities like the formulas for the sum of the first terms of some sequence. They all involve natural numbers, but in the expressions some divisions appear. So proving them becomes kind of a pain.

I have seen that the zify tactic deals with that kind of problem but specifically for substractions, transforming the goal that involves naturals, to a goal that involves integers (asking for proves that whatever needs to be positive, is indeed positive).

Is there an equivalent for that tactic for transforming a goal to the rationals (asking for proofs that denominators divide numerators in the fractions that appear)?

[Damiano Testa]

I don't think that there is a ratify tactic. It also seems a little harder that you would be in the situation where you know that all divisions are "exact". For zify, all you need is some inequalities. Divisibility seems like a much more stringent condition. It certainly can be satisfied, but seems much less applicable.

Could you expand on what divisions appear in your expressions?

[Kevin Buzzard]

Have you tried just coercing everything directly into the rationals and proving it there? In my mind a mathematician should never be using nat.div because it is not the "correct" division, so for example if you want to prove $\sum_{i=0}^{n-1}i=n(n-1)/2$ then this should be formalised as a statement about an equality of two rational numbers.

[Kevin Buzzard]

Example:

import tactic

open_locale big_operators

open finset

example (n : ℕ) : ∑ i in range n, (i : ℚ) = n * (n - 1) / 2 :=
begin
  induction n with d hd,
  { simp, },
  { rw [sum_range_succ, hd],
    push_cast,
    ring, }
end

[Kevin Buzzard]

and conversely I would claim that ∑ i in range n, i = n * (n - 1) / 2 is not a correct formalisation of $\sum_{i=0}^{n-2}i=n(n-1)/2$ because it's an a priori weaker statement due to the non-mathematical division.

[Yakov Pechersky]

There's also tactic#lift

[Miguel Marco]

Kevin Buzzard said:

Have you tried just coercing everything directly into the rationals and proving it there? In my mind a mathematician should never be using nat.div because it is not the "correct" division, so for example if you want to prove $\sum_{i=0}^{n-1}i=n(n-1)/2$ then this should be formalised as a statement about an equality of two rational numbers.

I thought about it, and I agree that that is usually what a mathematician thinks when we see such an equality. Bit then I thought that there might be also a case for the idea that what we really want to prove is that the equality holds even assuming that we mean integer division (with remainder).

That is why i though of having a tactic that could do that.

[Miguel Marco]

Damiano Testa said:

Could you expand on what divisions appear in your expressions?

The example I am working on in particular has expressions with sub-expressions like n * (n + 1) / 2

[Damiano Testa]

If you know what the denominators are beforehand, and you really want to work with nat.division, you can also multiply through by the LCM of the denominators.

However, I would recommend going with Kevin's suggestion, unless you have a compelling reason not to do it.