Zulip Chat Archive

Stream: new members

Topic: contracting `by_cases`


view this post on Zulip Heather Macbeth (Jul 22 2020 at 01:16):

Suppose I have a proof beginning with by_cases, and one of the cases is answered by a single lemma. Is there a syntactic trick to combine these two lines (the by_cases and the exact [lemma]) into one line?

view this post on Zulip Adam Topaz (Jul 22 2020 at 01:30):

You can probably do something with refine and LEM.

view this post on Zulip Heather Macbeth (Jul 22 2020 at 01:34):

Yes, I was hoping so -- do you know the syntax?

view this post on Zulip Adam Topaz (Jul 22 2020 at 01:45):

My first guess would be to try something approximately like this: refine or.elim (classical.em h) _ _ and fill in the blanks as necessary.

view this post on Zulip Heather Macbeth (Jul 22 2020 at 01:54):

Thanks! The or.elim is what I needed.

view this post on Zulip Adam Topaz (Jul 22 2020 at 01:56):

Maybe a better way would be to refine decidable.by_cases, since (I assume) that's what by_cases actually does

view this post on Zulip Mario Carneiro (Jul 22 2020 at 09:38):

You could also write something like refine if h : p then term else _


Last updated: May 06 2021 at 22:13 UTC