Zulip Chat Archive

Stream: new members

Topic: WLOG trick

Suryansh Shrivastava (May 24 2023 at 17:54):

Is there a lean4 counterpart to the statement that if aba \neq b, we can assume a<b a < b. Here a,b:Na,b: \N

Chris Bailey (May 24 2023 at 18:46):

What if a > b? If you meant a < b ∨ a > b, it appears to be in mathlib as lt_or_gt_of_ne

Anatole Dedecker (May 24 2023 at 19:11):

I think Suryansh meant that if the hypotheses and the goal are symmetrical in a and b, then you can treat only the a < b case. We have tactic#wlog to do that, but to be fair I’ve never used it. The manual solution is to start by proving your result for all a' and b' which satisfy ˋa' < b'ˋ, and then apply this to either ˋ(a, b) or ˋ(b, a) depending on the case

Jireh Loreaux (May 24 2023 at 19:19):

Anatole meant tactic#wlog

Yakov Pechersky (May 24 2023 at 19:39):

There is also the much less powerful, but conceptually simpler tactic#swap_var

Kevin Buzzard (May 24 2023 at 19:45):

Before WLOG I used to do this manually. You write down the appropriate statement of the from a<=b + symmetric hypotheses -> symmetric result and then apply it twice

Last updated: Dec 20 2023 at 11:08 UTC