Zulip Chat Archive

Stream: new members

Topic: best tactic for simple subtraction in nat


Moritz Firsching (Sep 23 2022 at 07:40):

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 (Sep 23 2022 at 07:48):

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 (Sep 23 2022 at 07:50):

E.g

import tactic

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

Alex J. Best (Sep 23 2022 at 07:51):

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

Moritz Firsching (Sep 23 2022 at 09:08):

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 (Sep 23 2022 at 09:10):

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

Moritz Firsching (Sep 23 2022 at 09:19):

perfect!

Kevin Buzzard (Sep 23 2022 at 11:44):

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

Martin Dvořák (Sep 23 2022 at 11:45):

I use omega very often!

Damiano Testa (Sep 23 2022 at 16:13):

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 (Sep 23 2022 at 16:13):

Would this be useful?

Alex J. Best (Sep 23 2022 at 20:23):

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 (Sep 24 2022 at 07:48):

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 (Sep 24 2022 at 08:08):

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.


Last updated: Dec 20 2023 at 11:08 UTC