Stream: general

Topic: by_cases and by_contradiction with inequalities

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.

Kenny Lau (Jul 12 2020 at 04:32):

by_cases! will perform by_cases and push_neg

Kenny Lau (Jul 12 2020 at 04:32):

(just like contrapose!)

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 !

Scott Morrison (Jul 12 2020 at 04:40):

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

Kenny Lau (Jul 12 2020 at 04:40):

by "will" I mean "I propose that"

oh

Sounds good.

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