Zulip Chat Archive

Stream: general

Topic: nat again


view this post on Zulip 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
  admit,
end

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 12 2020 at 17:00):

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

view this post on Zulip 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