Zulip Chat Archive

Stream: new members

Topic: Cases on fin 2


view this post on Zulip Thomas Read (Nov 28 2019 at 17:42):

Is there an easy way to do cases on a fin 2? Specifically I'd like to show that if we have
swap : fin 2 → fin 2 := λ x, if x = 0 then 1 else 0 then swap(swap(x)) = x.

I can repeatedly do cases on the fin to eventually get the answer, but it seems very tedious.

view this post on Zulip Johan Commelin (Nov 28 2019 at 17:44):

You could see if the library know about an equivalence between fin 2 and bool

view this post on Zulip Johan Commelin (Nov 28 2019 at 17:44):

Your problem might also be a good job for the case_bash tactic

view this post on Zulip Johan Commelin (Nov 28 2019 at 17:45):

Which is hiding somewhere in mathlib, if I'm not mistaken

view this post on Zulip Bryan Gin-ge Chen (Nov 28 2019 at 17:46):

Is this something fin_cases can do?

view this post on Zulip Thomas Read (Nov 28 2019 at 17:47):

Awesome, that works perfectly!

view this post on Zulip Johan Commelin (Nov 28 2019 at 17:48):

Aah, that's the one I meant


Last updated: May 14 2021 at 04:22 UTC