wlog

Stream: mathlib4

[Johan Commelin]

I'm not sure whether my simplification is worth it: https://github.com/leanprover-community/mathlib/compare/refactor-wlog?expand=1

[Johan Commelin]

I'm happy to push on. But I would like to hear from others first.

[Johan Commelin]

After my refactor, the wlog tactic would be really easy to port, but every wlog call turns from a 1-liner into a 3-or-4-line proof.

[Johan Commelin]

Those proofs are still very easy. So it's very likely that they can be killed by automation.

[Johan Commelin]

One reason (independent of mathport) why I wanted to simplify wlog is that the current version is pretty slowish.

[Kevin Buzzard]

Yes! The last time I tried it I found it had become unusable. I wanted to embark on a medium length proof; the first line was "WLOG a<=b" and this was taking several seconds to compile, meaning that I just couldn't face using it because it would have made writing the proof really painful.

[Johan Commelin]

I have another 8 hr train ride coming up tomorrow. Should I press on with this? Or is it not worth it?

[Jireh Loreaux]

I'll second that I have found wlog almost completely unusable, so a refactor would be greatly appreciated by me.

[Johan Commelin]

I just pushed more commits. All files in src/ containing wlog now compile locally.

[Johan Commelin]

TODO:

• update the docs
• make the tests work again