nat again

Stream: general

[Reid Barton]

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
  admit,
end

[Alex J. Best]

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]

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]

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]

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

[Kevin Buzzard]

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