wlog #16495

Stream: mathlib4

[Johan Commelin]

Since wlog is now a much simpler tactic, I have also significantly shortened the test file.

[Johan Commelin]

#16495

[Johan Commelin]

I merged master and fixed conflicts.

[Johan Commelin]

However, I must say that there is something going on with the generalizing clause that I don't understand completely.

• Sometimes the tactic fails in mysterious ways if the generalizing clause is not present (the error suggests that the final exact in the source of the tactic is failing), and adding a generalizes x y solves the problem.
• In other cases, I've seen a generalizing x y clause, and the tactic state would look all happy, but the kernel would reject the proof. Removing the generalizing clause solved the problem.

I've not been able to minimize.

[Moritz Doll]

I am in need of the wlog tactic for !4#2131. Is anyone working on porting it or is there a simple shortcut?

[Moritz Doll]

Also mathport goes a bit crazy on wlog:

trace
--"./././Mathport/Syntax/Translate/Tactic/Builtin.lean:75:38: in wlog #[[ident hle], [\":\", expr «expr ≤ »(u, v)], [\"generalizing\", ident u, ident v], []]: ./././Mathport/Syntax/Translate/Basic.lean:349:22: unsupported: too many args"

[Ruben Van de Velde]

Moritz Doll said:

Also mathport goes a bit crazy on wlog:

trace
--"./././Mathport/Syntax/Translate/Tactic/Builtin.lean:75:38: in wlog #[[ident hle], [\":\", expr «expr ≤ »(u, v)], [\"generalizing\", ident u, ident v], []]: ./././Mathport/Syntax/Translate/Basic.lean:349:22: unsupported: too many args"

@Mario Carneiro is that a mathport bug?

[Johan Commelin]

@Moritz Doll Very recently the wlog tactic in mathlib 3 was simplified. By now it should be "easy" to port.

[Lukas Miaskiwskyi]

I've also gotten fairly far by replacing wlog with swap_var, though it's a bit annoying since wlog was smart enough to find out all the dependent terms that needed to be swapped, and with swap_var you need to pick everything out manually. So first use e.g. casesto deconstruct the situation into different cases, on_goal x => swap_var for all the variable replacements, and then all_goals for the rest of the proof. But it's finicky. Here is my example: https://github.com/leanprover-community/mathlib4/blob/9749733b8f63c15ef3c310cbe6133f1f20cfa73d/Mathlib/Data/Set/Intervals/OrdConnectedComponent.lean#L213

[Lukas Miaskiwskyi]

But if wlog is easy to port, that is certainly the more useful way to go :)

[Thomas Murrills]

I can start porting it tomorrow if no one is working on it already :)

[Mario Carneiro]

I just changed the syntax to match lean 3:

/- B -/ syntax (name := wlog) "wlog " ident " : " term
  (" generalizing" (ppSpace colGt ident)*)? (" with " ident)? : tactic

make sure you use this if you are working on it

[Mario Carneiro]

on this note, what should the syntax of lean 4 wlog be? It seems to have been quite significantly changed in the last update, I'm not really sure how the new bells and whistles map onto the old ones:

/- B -/ syntax (name := wlog) "wlog" (" (" &"discharger" " := " term ")")?
  (ppSpace (colGt ident))? (" : " term)? (" := " term)? (" using " (ident*),+)? : tactic

[Mario Carneiro]

I guess the generalizing argument corresponds to the old using arg, although there is no longer a list of lists?

[Mario Carneiro]

and the with H argument is new, or is it the := arg?

[Johan Commelin]

generalizing just means a revert before the actual wlog call.

[Mario Carneiro]

I noticed that generalizing * is supported and means the same as nothing?

[Johan Commelin]

/-- `wlog h : P` will add an assumption `h : P` to the main goal,
and add a side goal that requires showing that the case `h : ¬ P` can be reduced to the case
where `P` holds (typically by symmetry).

The side goal will be at the top of the stack. In this side goal, there will be two assumptions:
- `h : ¬ P`: the assumption that `P` does not hold
- `this`: which is the statement that in the old context `P` suffices to prove the goal.
  By default, the name `this` is used, but the idiom `with H` can be added to specify the name:
  `wlog h : P with H`.

Typically, it is useful to use the variant `wlog h : P generalizing x y`,
to revert certain parts of the context before creating the new goal.
In this way, the wlog-claim `this` can be applied to `x` and `y` in different orders
(exploiting symmetry, which is the typical use case).

By default, the entire context is reverted. -/

[Johan Commelin]

I think this should answer your questions

[Mario Carneiro]

I see this but it doesn't cover migration questions

[Johan Commelin]

I don't have a good name for the h and H in wlog h L P with H.

[Mario Carneiro]

you are presuming that I know what the old version did :)

[Mario Carneiro]

does the with arg map onto anything in the old version?

[Johan Commelin]

Not sure. Why is that relevant?

[Johan Commelin]

My understanding is that with H is a new feature. In the old version, H was always called this. But maybe I'm missing something.

[Thomas Murrills]

I made a PR with blank files; I'll start actually looking at it tomorrow. In the meantime, if anyone wants to write a test or two beforehand in test/wlog.lean, that would be very much appreciated—I'm new to the tactic and seeing a couple lean 4 examples (and having the tests at the ready) will probably help speed things along! :) !4#2144

[Thomas Murrills]

Ok, wlog should be usable now! !4#2144

[Thomas Murrills]

I'm not putting it out for review just yet because the code itself could use an organizational once-over, and I want to sleep. But the functionality should be there, so @Moritz Doll if you're eager to start porting with it, feel free merge the wlog branch—and of course let me know if you run into any bugs 🙃

[Kevin Buzzard]

Thank you Thomas!

[Moritz Doll]

that is great news, thanks Thomas. I will put that into my branch tomorrow and report any errors.

[Arien Malec]

I'm using this with !4#2080 and blocked on using

[Arien Malec]

Unless using in mathli3 is the same as generalizing?

[Thomas Murrills]

The syntax has just now changed to use generalizing and with both in mathlib4 and mathlib3, and the mathlib3 and 4 versions match up in functionality! I’m not sure which corresponds to which (since I’m not familiar with the old version) but it should be one of the two. 🙃

[Moritz Doll]

Error message time:
Code is at https://github.com/leanprover-community/mathlib4/blob/362a3511b6cfe1940ff86171f2c772b7533ed481/Mathlib/Topology/Algebra/Order/LeftRightLim.lean#L266
and the error is that wlog does not find variables that have been introduced in the rintro in the line before (unknown identifier 'u'), so I suspect that it is a WithMainContext issue.

[Moritz Doll]

in fact it is, I commit the fix to your PR

[Moritz Doll]

with that my PR is error free

[Thomas Murrills]

ah nice, good catch! I was so worried about inner withMainContexts causing problems I forgot about the main one... :upside_down:

[Moritz Doll]

I've added a test as well. It is a bit stupid, but that keeps the bugs out

[Thomas Murrills]

Nice! All tests are welcome, the stupider (= more minimal!) the better :) I still haven't given the code that once-over since I didn't have much time today, but I hope to do so tomorrow—I wouldn't be surprised if there's another surprise in there. (...Well, you know what I mean.) I plan to add a couple more tests as well.

[Arien Malec]

Is this the same issue that cases swap to lose this in !4#2043?

[Thomas Murrills]

the fix is live now if you want to merge wlog and see if it works; but if not lmk and I’ll take a look (is this an issue with wlog or swap?)

[Arien Malec]

I've re-merged to make sure I picked up the latest.

I don't understand well what wlog does, but after wlog at line 400, I get the tactic state:

n: ℕ
c: Composition n
i₁i₂: Fin (length c)
h: i₁ ≠ i₂
this: ∀ {i₁ i₂ : Fin (length c)},
  i₁ ≠ i₂ →
    i₁ ≤ i₂ → _root_.Disjoint (Set.range ↑(embedding c i₁).toEmbedding) (Set.range ↑(embedding c i₂).toEmbedding)
h': ¬i₁ ≤ i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁).toEmbedding) (Set.range ↑(embedding c i₂).toEmbedding)
n: ℕ
c: Composition n
i₁i₂: Fin (length c)
h: i₁ ≠ i₂
h': i₁ ≤ i₂
⊢ _root_.Disjoint (Set.range ↑(embedding c i₁).toEmbedding) (Set.range ↑(embedding c i₂).toEmbedding)

where the second goal is missing this (and I've tried to name via with to no avail).

[Thomas Murrills]

Weird, I'll take a look rn

[Thomas Murrills]

Oops, I didn't read the message closely. the second goal should not have this; only the first goal gets a this, because this is only used in the first goal to prove that we can reduce to the second goal.

[Thomas Murrills]

It seems this has to with this file coming from an outdated mathlib3 source (from before the recent mathlib3 change to wlog). The mathlib3 proof looks a little different now; I'll fix it.

[Thomas Murrills]

Oops, realizing I never implemented the other half of binderIdent (_).

What should this look like? mathlib3 doesn't allow _ in this position, so I'm guessing it's a new feature? Is it just that we should generate some name (presumably h here) and introduce it with .implicit binder info?

[Mario Carneiro]

_ should be allowed wherever an identifier is allowed (when declaring new bindings), and it does nothing except name the variable automatically with an inaccessible name

[Thomas Murrills]

and inaccessible = has BinderInfo.implicit?

[Thomas Murrills]

wait a minute...maybe that's a red herring. case detects if names are inaccessible by whether they have macro scopes

[Mario Carneiro]

why are you detecting if the name is inaccessible?

[Mario Carneiro]

intro1 will introduce an anonymous variable

[Thomas Murrills]

I'm not actually trying to detect inaccessible names, I'm just trying to figure out what it means for a name to be inaccessible

[Mario Carneiro]

the short version is "it is printed with a tombstone"

[Thomas Murrills]

but behind the scenes, literally all that's different is that the name contains a tombstone? surely there's more?

[Mario Carneiro]

it could mean that the name is shadowed, it has macro scopes, or it uses internal name components

[Thomas Murrills]

hmmmm okay

[Mario Carneiro]

the name doesn't literally have a tombstone in it

[Thomas Murrills]

I did see one function which appeared to check for just that, so it sounded plausible

[Mario Carneiro]

but the idea is that writing the literal name you see for the variable won't resolve to that variable

[Thomas Murrills]

right, that part (how they should work/affect things) makes sense

[Thomas Murrills]

hmm intro1 works for one part

[Thomas Murrills]

but the other is an introduction of a hypothesis from byCases

[Mario Carneiro]

the point being that it's sort of an emergent property, it's not a flag on the name

[Thomas Murrills]

oh interesting. so when it's greyed out in the tactic state, how does lean "tell" that it should do that? and is being greyed out actually connected to being inaccessible, or is that a coincidence? (is it perhaps just a reflection of the binderinfo?)

[Mario Carneiro]

I believe it just does a name lookup with the name of the ldecl and if you don't get the same ldecl back then it's inaccessible

[Mario Carneiro]

the binderinfo is mostly unrelated

[Thomas Murrills]

how could the result of the name lookup differ if we're using the name to look it up, so to speak?

[Mario Carneiro]

there is a binderinfo for variables that are even more hidden than inaccessible names, isImplementationDetail. These will not be shown at all in the tactic state and are not accessible to tactics like assumption

[Thomas Murrills]

is there any relation between implementation details and aux decls?

[Mario Carneiro]

if you have two variables named x in the state, let's say with FVarIds 1 and 2 respectively, then getFVarByUserName? `x will give you FVarId 2 and so FVarId 1 is inaccessible

[Thomas Murrills]

ah okay

[Mario Carneiro]

IIRC implementation detail replaced aux decl

[Mario Carneiro]

that's not true, they are both there and serve similar functions

[Mario Carneiro]

I think they can probably be merged

[Mario Carneiro]

aux decls act more like global declarations than local variables for name resolution purposes

[Thomas Murrills]

I see, I just looked up the code and saw that there are default decls, aux decls, and implementation detail decls, though apparently isImplementationDetail means "not a .default decl"

[Thomas Murrills]

so anyway hmm. I need to make this fvar introduced by byCases into an inaccessible name

[Thomas Murrills]

or wait. do I

[Mario Carneiro]

you don't need to do anything special for that

[Mario Carneiro]

it already is unless you gave it a name explicitly

[Thomas Murrills]

because byCases doesn't, so maybe I shouldn't either

[Thomas Murrills]

byCases actually seems to use an explicit name h when a name is not given

[Thomas Murrills]

instead of an inaccessible one

[Mario Carneiro]

pass `_ for the name and an inaccessible name will be generated

[Thomas Murrills]

from a design point of view is that the right thing to do? if this is essentially the result of a by_cases tactic, should it be named accordingly?

[Mario Carneiro]

if you pass _ then it should not be named h (it can be named hygienic h if you like)

[Mario Carneiro]

if you pass nothing then it can maybe be named h (although that kind of design is being deprecated in lean 4)

[Thomas Murrills]

ah i see. irrelevant here anyway since the binderIdent is not optional for wlog

[Thomas Murrills]

so that decides that

[Thomas Murrills]

ok, fixed! :)

[Thomas Murrills]

(ok, now: fixed. long line snuck in.)

[Thomas Murrills]

I'm guessing that, in general, implementation details have no business being reverted, right?

[Thomas Murrills]

Or is that just an aux decls thing?

[Thomas Murrills]

wait, when you said "not visible in the tactic state"—do implDecls even appear when I retrieve a goal's local context?

[Mario Carneiro]

they do

[Mario Carneiro]

you should use isImplementationDetail when looping over the local context to skip those variables

[Mario Carneiro]

you should pretend that implementation detail variables don't exist at all for the purpose of tactic logic

[Thomas Murrills]

Makes sense, I was already filtering out aux decls

[Mario Carneiro]

that's why isImplementationDetail returns true for both implDetail and auxDecl

[Thomas Murrills]

Actually there is one thing here: revert has an option to clear aux decls instead of reverting them, but currently I just avoid feeding them to revert in the first place. Do you think that's alright? That's basically my last (known) issue with wlog.

[Thomas Murrills]

Oh wait. Clearing won't affect anything at the point I do it

[Mario Carneiro]

you should not use that optional parameter in revert

[Thomas Murrills]

I do it within withoutModifyingState, so whether I do or don't it won't matter—but cool, I will not :)

[Mario Carneiro]

if you let it do the default thing, it will fail if you pass it an aux decl

[Thomas Murrills]

right, that's what I found

[Thomas Murrills]

which is why I filter them out (well, now I filter all implementation details out)

[Mario Carneiro]

but you shouldn't do that anyway

[Mario Carneiro]

why are you going over the lctx in the first place?

[Mario Carneiro]

withoutModifyingState doesn't prevent failures from leaking out BTW

[Thomas Murrills]

yes, but presumably running .clear on an mvarid inside withModifyingState won't affect the outside world?

[Mario Carneiro]

only if it succeeds

[Mario Carneiro]

why would you use clear and then revert the state?

[Thomas Murrills]

Mario Carneiro said:

why are you going over the lctx in the first place?

same reason it's done in mathlib3: get the fvarids to revert, and revert them to construct the type of this (one of the reduction hypotheses)

[Mario Carneiro]

revert does that already

[Thomas Murrills]

Mario Carneiro said:

why would you use clear and then revert the state?

I wouldn't, but that's what revert does

[Thomas Murrills]

like here's what happened here: clearAuxDeclsInsteadOfReverting not only skips aux decls, it clears them. I currently just skip them (and filter them out before they get to revert.

I wondered "hmm, do I need to worry about some weird edge case where I would want them cleared? why is revert trying to clear them anyway? something I don't know about?"

then realized "wait, obviously: a successful clear operation doesn't matter, I'm doing it in withoutModifyingState" (a failed clear operation does matter, as you pointed out)

[Mario Carneiro]

it sounds like you don't need most of what revert does, actually, since you aren't making use of the mvar

[Mario Carneiro]

the main important logic is collectForwardDeps fvars preserveOrder

[Thomas Murrills]

that's true, is there an expression version that still lets me use the FVarIds?

[Thomas Murrills]

ah ok

[Mario Carneiro]

you also want to filter out the isImplementationDetail hyps from that

[Mario Carneiro]

Thomas Murrills said:

like here's what happened here: clearAuxDeclsInsteadOfReverting not only skips aux decls, it clears them. I currently just skip them (and filter them out before they get to revert.

It doesn't clear all aux decls, only the ones that would otherwise have been reverted

[Mario Carneiro]

the reason is that we want to pretend they don't exist, so they can't cause a failure of the tactic, nor can they show up in the implication of the new goal

[Thomas Murrills]

Mario Carneiro said:

you also want to filter out the isImplementationDetail hyps from that

you mean from the result...?

[Mario Carneiro]

yes

[Mario Carneiro]

forward deps means all hyps whose types depend on the variables that are about to be reverted

[Mario Carneiro]

those hyps all have to go, one way or another

[Mario Carneiro]

either they go into the implication or they are cleared

[Mario Carneiro]

(at least, in revert)

[Mario Carneiro]

in your case you are just constructing the implication without clearing stuff so you can just skip them

[Thomas Murrills]

ah, I see what you mean

[Thomas Murrills]

seems like the thing that actually makes the type after that is mkAuxMVarType, which handles a bunch of different cases, so I suppose I'll use that as well

[Thomas Murrills]

@Mario Carneiro, do you want to take a look at how this wound up (lines 77 - 82 WLOG.lean !4#2144), or shall I just go ahead and merge it? (It works fine in the tests and the mathlib4 file it's currently used in)

[Thomas Murrills]

(I was delegated merge privileges (exciting!), but it's changed since I was delegated those, so I thought I'd be prudent)

[Thomas Murrills]

(Or if anyone else wants to take a look at the refactor and give me the go ahead again, just in the interest of having everything be reviewed by someone who didn’t write it.)

[Thomas Murrills]

Actually there is something I don't understand about the code I used.

So, revert calls collectForwardDeps to get toRevertNew, then feeds the result to MetavarContext.revert. This uses a fresh cache (what does that do?) and calls elimMVar.

That actually calls collectForwardDeps again (the MkBinding version, which is what's lifted to the version used explicitly in revert), and has this note:

-- Note that `toRevert` only contains free variables at this point since it is the result of `getInScope`;
-- after `collectForwardDeps`, this may no longer be the case because it may include metavariables
-- whose local contexts depend on `toRevert` (i.e. "may dependencies")
let toRevert ← collectForwardDeps mvarLCtx toRevert

mkAuxMVarType is then called on the resulting toRevert. But here's the thing I don't understand:

This toRevert (the one that "may include metavariables") is returned all the way up through to revert, where we then return toRevert.map Expr.fvarId!.

[Thomas Murrills]

So, I mean, the fact that revert uses Expr.fvarId! is a pretty good indication that we don't actually have to worry about those possible metavariables in this circumstance. But why don't we?

[Thomas Murrills]

Hmm, in the interest of not holding up the port, I’m just going to merge it—if there is a problem introduced by this refactor, it must only occur in some edge cases, and I’ll fix it at that point :)

[Mario Carneiro]

I'm in paper crunch time, so I don't have much time for reviewing. It looks plausible, we can pick up the pieces later

[Thomas Murrills]

Sounds good, good luck with the paper(s)! :)

[Jon Eugster]

I came across a bit of an unfortunate behaviour of wlog (sorry for the bit daft mwe):

import Mathlib.Tactic.WLOG
import Mathlib.Tactic.Tauto

-- some random global variables
variable {A B C : Prop}

example (h : A ) : A := by
    wlog a : A with h_wlog
    · have w := h_wlog h    -- fails
      -- don't know how to synthesize implicit argument
      -- @h_wlog A ?m.68 ?m.69
      -- It wants some values for `B` and `C`, even though they are not used at all in
      -- the theorem.
      -- have w := @h_wlog _ A A h    -- This works (or any other values for arg 2 and 3)
      apply w
      assumption
    · assumption

If there are too many variables in context that are not needed, then the first step of wlog still creates implicit holes for all of them (in h_wlog) and you have to explicitely plug in values for them. (see also !4#3153 )

Is there an easy fix for this? Or would I just have to delete all unnecessary variables?

[Kevin Buzzard]

aargh.

For some reason I still don't quite understand, Lean 4 finds it much harder to throw away variables which aren't being used in a proof. This is not the first time it's caused problems.

[Floris van Doorn]

A workaround is to use the clear tactic on all variables that you don't want, e.g. clear B C.

[Thomas Murrills]

Thanks for letting me know, I’ll take a look! :)

[Thomas Murrills]

Hmmm...this might be intended behavior for wlog, which is meant to revert the entire context by default. You can choose to only revert the parts of the context that depend on x y <etc> by using generalizing x y <etc>, e.g.

variable {A B C : Prop}

example (h : A) : A := by
    wlog a : A generalizing h with h_wlog
    · have w := h_wlog h -- ok
      apply w
      assumption
    · assumption

But maybe it shouldn't revert the entire context by default...open to any ideas!

[Thomas Murrills]

Though, maybe this is more a "how should variables work" problem than a wlog problem. If B and C weren't introduced into the context in the first place, we wouldn't need generalizing (note that generalizing A also works here).

[Thomas Murrills]

But, if we assume that's not going to change: is there any way a tactic can identify global variables not used in the theorem statement like B and C? If so I could simply remove those "probably irrelevant" ones from the default reverted context, if that would be a good idea. (Not sure.)

[Thomas Murrills]

@Jon Eugster what was the wlog issue in !4#3150 ?

[Jon Eugster]

Thanks for having a look @Thomas Murrills. I wouldn't know either what's the best default behaviour. And after all we're probably talking about wlog working in a bad context in the first place. I assume after the port some people will go and delete a lot of these variable (α β γ δ … : Type _) lines anyways.

#3150 does not have any issues with wlog, I mistook the apply @Nat.gcd.induction _ m n (which I had to write out) as an example of the case above, but that has nothing to do with wlog, my bad.

[Scott Morrison]

This has also arisen in !4#3152.