numerals in fin

Stream: new members

[Yakov Pechersky]

I've extracted out an expression from a goal I have that I believe should simplify, but does not. What's the right way to discharge this goal? I can't figure out the right way to generalize the statement over bit0 or bit1. And, of course, this is just an instance of a larger pattern, so dec_trivial isn't useful for the general case.

import data.fin

example : equiv.swap (0 : fin (2 : ℕ).succ) (1 : fin (1 + (1 : ℕ).succ)) (1 : fin (1 + 1)).succ = (1 : fin (1 + 1)).succ :=
begin
  rw equiv.swap_apply_of_ne_of_ne,
  { simp [fin.succ_ne_zero] },
  { sorry }
end

[Alex J. Best]

Do you just want to solve this goal or are you asking about something more general?

[Alex J. Best]

You can do rintro ⟨⟩ for this sorry.

[Yakov Pechersky]

I'm asking about how to show

1 < 1.succ

or

1 \ne 1.succ

where the 1s are appropriate fin _. Or the same statement for any numeral. In the general case, so that I can pass that to a simp set, instead of proving this very particular instantiation as a side goal.

[Eric Wieser]

Would the following simp rules help?
swap (bit0 x) (bit0 y) (bit1 z) = bit1 z
swap (bit1 x) (bit1 y) (bit0 z) = bit0 z
swap (f x) (f y) (f z) = f (swap x y z)