best tactic for simple subtraction in nat

Stream: new members

[Moritz Firsching]

I sometimes find myself manually proving things like the following:

import tactic

example (n : ℕ) (h: 0 < n): n - 1 + 2 = n + 1 :=
begin
  sorry,
end

and feel like there should be a tactic which make these types of calculations automatic. Is there?

[Alex J. Best]

Well there used to be omega but you cant use that in mathlib proofs and more as it is unmaintained and not likely to be ported before mathlib4.
@Damiano Testa was working on a simpler tactic for exactly this at #16443 but its not merged yet.
tactic#zify is sometimes also useful for this sort of thing, especially when combined with ring/linarith

[Alex J. Best]

E.g

import tactic

example (n : ℕ) (h: 0 < n): n - 1 + 2 = n + 1 :=
begin
  zify [h], ring,
end

[Alex J. Best]

Apparently in this case tactics are smart enough to find h, but in general giving zify extra arguments helps

[Moritz Firsching]

Cool, thanks zify looks exactly like something I was looking for!
Now I wonder if there is something similar for integer division, like "qify". E.g. some tactic that could stuff like

example (n : ℤ) (h : 2 ∣ n) : n / 2 * 4 = n * 2 :=
begin
  sorry,
end

[Alex J. Best]

qify is #16313, which is awaiting review also I think!

[Moritz Firsching]

perfect!

[Kevin Buzzard]

One will also need a / analogue of Damiano's tactic I guess, because division on int and rat aren't compatible.

[Martin Dvořák]

I use omega very often!

[Damiano Testa]

I'm thinking that there are a few instances where similar case splits can be useful. I could look into extending remove_subs to take care of nat-division and max/min. It could be a generic "split obvious cases" tactic.

[Damiano Testa]

Would this be useful?

[Alex J. Best]

I think Damiano's tactic would just shorten the proof more right, qify, cancel_denoms, norm_num (if not just qify, cancel_denoms should work for Moritz' example)

[Damiano Testa]

I'm back at my computer and I just confirmed that on branch#adomani_remove_subs_at

import tactic.remove_subs

example (n : ℕ) (h: 0 < n): n - 1 + 2 = n + 1 :=
by remove_subs!

works.

[Damiano Testa]

Although I also just noticed that by linarith already works in this example.

Note that the !-flag to remove_subs means "try to discharge the side-goals using linarith", so I would not consider this a good test for remove_subs.