Zulip Chat Archive

Stream: new members

Topic: How to prove a target with `ite` by cases


view this post on Zulip Rui Liu (Dec 25 2020 at 16:23):

I have a goal of form (ite p a b) = c, how do I prove by cases on p and generate two goals?

view this post on Zulip Yakov Pechersky (Dec 25 2020 at 16:27):

split_ifs should generate the two goals, casing on p

view this post on Zulip Yakov Pechersky (Dec 25 2020 at 16:28):

If you want more control, you can do

by_cases hp : p,
{ rw if_pos hp,
  sorry },
{ rw if_neg hp,
  sorry }

view this post on Zulip Rui Liu (Dec 25 2020 at 16:29):

@Yakov Pechersky Thank you, that's fast and exactly what I want :)


Last updated: May 14 2021 at 12:18 UTC