Stream: new members
Topic: contracting `by_cases`
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?
Adam Topaz (Jul 22 2020 at 01:30):
You can probably do something with refine and LEM.
Heather Macbeth (Jul 22 2020 at 01:34):
Yes, I was hoping so -- do you know the syntax?
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.
Heather Macbeth (Jul 22 2020 at 01:54):
or.elim is what I needed.
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
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