Zulip Chat Archive

Stream: general

Topic: by_cases and by_contradiction with inequalities


view this post on Zulip Scott Morrison (Jul 12 2020 at 04:31):

How would people feel about by_cases a ≤ b returning h : b < a in the second branch, rather than h : ¬(a ≤ b)?

I'm worried that there's not a really principled way to do this (do we just hack in something for inequalities?) (do we add a simp_set and apply that?) but it seems like to could make life smoother for most people.

view this post on Zulip Kenny Lau (Jul 12 2020 at 04:32):

by_cases! will perform by_cases and push_neg

view this post on Zulip Kenny Lau (Jul 12 2020 at 04:32):

(just like contrapose!)

view this post on Zulip Scott Morrison (Jul 12 2020 at 04:37):

Where is by_cases! implemented? Hitting F12 takes me to by_cases, with no sign of parsing for a !

view this post on Zulip Scott Morrison (Jul 12 2020 at 04:40):

I can't find any usage at all of by_cases!.

view this post on Zulip Kenny Lau (Jul 12 2020 at 04:40):

by "will" I mean "I propose that"

view this post on Zulip Scott Morrison (Jul 12 2020 at 04:40):

oh

view this post on Zulip Scott Morrison (Jul 12 2020 at 04:40):

Sounds good.

view this post on Zulip Kevin Buzzard (Jul 12 2020 at 08:36):

Sounds great. Would be nice to have = and \ne as well


Last updated: May 06 2021 at 21:09 UTC