Stream: general

Topic: nat again

Reid Barton (Aug 12 2020 at 16:51):

What's the state of the art for proving goals like

example {n : ℕ} (i j : fin n) (h : i < j) :
n = ↑i + (↑j - ↑i + 1 + (n - 1 - ↑j)) :=
begin
end


Alex J. Best (Aug 12 2020 at 16:57):

I don't know about state of the art, but moving everything to nat then omega seems a general strategy.

example {n : ℕ} (i j : fin n) (h : i < j) :
n = ↑i + (↑j - ↑i + 1 + (n - 1 - ↑j)) :=
begin
cases i,
cases j,
dsimp,
change i_val < j_val at h,
omega,
end


Alex J. Best (Aug 12 2020 at 16:59):

I guess you want a tactic like zify to take goals about fin to goals about nat with various bounds so omega can do its thing?

Kevin Buzzard (Aug 12 2020 at 16:59):

import tactic

example {n : ℕ} (i j : fin n) (h : i < j) :
n = ↑i + (↑j - ↑i + 1 + (n - 1 - ↑j)) :=
begin
cases i; cases j, dsimp at *,
have h2 : i_val < j_val := h,
-- omega fails here
clear h,
omega, -- works here
end


omega is sort of like an old car, if you use it a fair amount then you learn some of the tricks and you can get things out of it, but there's an issue where there's a list of problems it has.

Reid Barton (Aug 12 2020 at 17:00):

Thanks, I definitely don't have the habit of using omega yet.

Kevin Buzzard (Aug 12 2020 at 17:03):

It works best if you have cleared all other hypotheses and made sure every natural is in a sensible form.

Last updated: May 12 2021 at 22:15 UTC