mathlib

mathlib copied to clipboard

Benefits:

• The tactic is faster
• The tactic is easier to port to Lean 4

Downside:

• The tactic doesn't do any heavy-lifting for the user

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/wlog/near/296996966

---

i'd be a lot more confortable if it could run some basic things, maybe some sort of push_neg (with a wlog! switch if you're worried about performance). or at least have dot notation for stuff like le_of_not_le

I would prefer to leave those improvements to the Lean 4 version.

I didn't look through the implementation yet, but I love the semantics! Finally a wlog that I understand and that works like a w.l.o.g. on paper!

What is the reason for a separate doneif though? Is there an advantage over wlog ..., swap, or even just reordering the proof? I also find it a bit confusing that wlog and doneif revert different assumptions by default.

@gebner Providing doneif is just a little bonus for the user. Just like you have suffices and have.

I agree that it might make sense to have both of them have the same "reverting" behaviour. I'll fix that now.

I'm also in the camp that doneif is superfluous here, for a relatively infrequently used tactic. Too many variants makes it harder for newbies. I'm guessing the total number of swaps this will require in the future history of mathlib may still add up to fewer bytes than the boilerplate to introduce doneif separately from wlog!

But it's obviously not critical either way.

The current build failure suggests that wlog is broken. But I have no idea how to debug what's wrong.

The problem seems to be with wlog ... generalizing generating a buggy proof. But I don't see what's wrong when I stare at the code.

I just observed wlog generating a buggy proof that the kernel rejects: it's the proof of pow_eq_one_of_norm_eq_one here. This is with the wlog currently in mathlib, so this bug may be already present and unrelated to changes made in this PR. The error message says

type mismatch at application
...
term
  habne
has type
  a < b
but is expected to have type
  b < a

Beware that the last commit would conflict with #16804 where I used a trick to replace the buggy wlog. (I suspect the trick is pretty widely applicable and actually may provide one way of implementing wlog, but I'm not sure if it's good practice.)

I'm able to minimize the example above:

import tactic.wlog
example (a b : ℕ) (hn : a < b ∨ b < a) : 0 = 0 :=
by { wlog : b < a := hn using [a b], refl }

shows "goals accomplished" but produces the error

type mismatch at application
  (λ (a b : ℕ) (hn : b < a), eq.refl 0) a b hn
term
  hn
has type
  a < b
but is expected to have type
  b < a

Maybe this is intended to fail because b < a isn't the first in the disjunction; if you replace it with wlog : a < b ... then it works (and [a b] vs. [b a] doesn't matter). However it's really confusing that it shows "goals accomplished". Not sure if this remains relevant after simplification made in this PR.

I don't think I can meaningfully push this PR further. I don't know how to debug the mysterious behaviour. So I'm tagging this please-adopt (cc @semorrison).

@urkud Thanks for pushing some fixes.

@jcommelin Do you have concrete examples for the mysterious behavior? You said something about generalize on zulip. Everything seems to build here though.

I'm perfectly happy if we merge as is and deal with any mysterious fallout later. :-)

Here's an example that works around a problem: https://github.com/leanprover-community/mathlib/pull/16495/commits/39df28619ded2767bcc8c60c9e87a793b2739c80 If you revert those two lines, you can see how generalizing is misbehaving.

But I agree with Scott. We can probably just merge this. The port of wlog to Lean 4 might have the bug disappear altogether because of hygiene and whatnot.

bors merge

Build failed (retrying...):

• Lint mathlib

bors r- Can you merge master and fix the build? bors d+

:v: jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Canceled.

I will not be able to do this before Tuesday. If someone else wants to do it before then, please go ahead!

bors merge

This PR was included in a batch that was canceled, it will be automatically retried

Build failed (retrying...):

• Lint mathlib

One more use of wlog was merged in the meantime :(

bors failure

bors r-

Canceled.

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests