feat(tactic): generalize wlog to support multiple variables and cases…

[johoelzl]

This generalizes wlog to allow more than two variables, and hence also more then two permutations.

The user can now provide a explicit rule which shows that all permutation are covered.

Another change is that wlog doesn't run the default discharger for the main goal or for the cases.

@cipher1024 @PatrickMassot there are only tests in mathlib. Do you want to test this version if it works with our applications?
I have at least one applications from Mason-Stother which might go into mathlib and require more than one variable. I will merge this if there are no problems.

[cipher1024]

It looks pretty cool! Do you have a proof that you're using it for? Would it be possible to see it?

My main use is in a package that is currently pretty broken. I'll still venture a thumbs up and come back and fix it if it ends up (re-) breaking my package.

[johoelzl]

I want simplify this proof:
https://github.com/johoelzl/mason-stother/blob/master/mason_stothers_v2.lean#L1854
The case would be about the polynomial degrees a, b, c: selecting the maximum, a la
(a >= b /\ a >= c) \/ (b >= a /\ b >= c) \/ (c >= a /\ c >= b)
here we have three cases, and three variables.

[PatrickMassot]

What happened? I wanted to try this but the commits disappeared.

[johoelzl]

Argh, I somehow rebased my mathlib repo to the wrong version. Should be fixed now.

[johoelzl]

@PatrickMassot the commits are here again.

[johoelzl]

Sorry I pushed only a old version, this doesn't yet include the discharger for the invariant goals. Sorry, the changes are on my laptop at home

[PatrickMassot]

I just saw your last message after testing it. Indeed the current version is a regression compared to Simon's version in my use case. The magic is gone, I need two more { finish } for each use of wlog. At least I'm all set up to test your version when it's ready.

[johoelzl]

With the discharger, you will still need one additional { finish }.

I see wlog similar to induction or case which produce very fixed and predictable outputs. I want to have similar behavior for wlog, with the exception of the invariant proofs, ideally they are AC and symmetry proofs only.

[PatrickMassot]

Why not trying finish, and backtrack completely if it fails?

[johoelzl]

finish is a quiet powerful tactic, it maybe slow or even non-terminating. Also the list of your goals might change arbitrarily when a new rule gets added.

We also don't call finish after induction or cases.

[PatrickMassot]

Ok, maybe finish is a bit extreme for execution speed, although I don't understand you other point if you backtrack completely unless it's a total success.
What about using what @cipher1024 's version did in
https://github.com/leanprover/mathlib/blob/master/tactic/interactive.lean#L333-L339
Was it slow?

[PatrickMassot]

I guess cc was doing the right thing in my use case. And I feel like wlog is already a much more sophisticated (in the sense of specialized and far away from the low level term mode) tactic than induction or cases.

[cipher1024]

@johoelzl I see your point about making the tactic more specific rather than aggressive and it makes sense. I have a feeling that there is a number of cases that are very common and I'd love to make those shorter. How do you feel about making an aggressive version. For instance, we could call wlog! when we're faced with those common cases.

[cipher1024]

Also, when you talk about proofs of invariance, do you mean that you now give an obligation to prove an equivalence between various rewriting forms? I was quite happy to avoid those because the proof obligations I give discharged completely automatically.

[johoelzl]

So what would wlog! a <= b do? Isn't it wlog h : a <= b; finish?

The proof of invariance have the form (h : p y z x) (h : g x y z) |- g y z x so you proof that from the first case you can derive all other cases. As an implication, no equivalence necessary.

[johoelzl]

And I feel like wlog is already a much more sophisticated (in the sense of specialized and far away from the low level term mode) tactic

While wlog is specialized, it isn't very sophisticated. For me wlog is quite like induction or cases, it operates on your goal in a very specific way. Its very predicable what the outcome of wlog will be. Compared to the finishing tactics like simp, finish, cc etc. which are very heuristics based.

[cipher1024]

The proof of invariance have the form (h : p y z x) (h : g x y z) |- g y z x so you proof that from the first case you can derive all other cases. As an implication, no equivalence necessary.

Ah! Excellent! What does it do when that implication fails?

As I recall, I used to try solve_by_elim and apply le_total to discharge the disjunction. I'm not used to finish but if it subsumes those tactics, you could define wlog! as wlog h : a <= b ; [ finish , skip ]. If I'm counting correctly, that should take in one goal and return one goal.

[PatrickMassot]

While wlog is specialized, it isn't very sophisticated. For me wlog is quite like induction or cases, it operates on your goal in a very specific way. Its very predicable what the outcome of wlog will be. Compared to the finishing tactics like simp, finish, cc etc. which are very heuristics based.

Well, Simon's version is sophisticated and heuristic based. Somehow it may mean we really need two versions, as Simon suggests.

[johoelzl]

Both wlog try to solve the invariant cases using solve_by_elim, tauto or cc. Then the user is left with the main goal p x y -> g x y and maybe with the cases goal p x y \/ p y x both of these goals are quiet unlikely to be so solved using automation.

In both cases if the invariant goal can not be solved, it is returned to the user (i.e. try discharger). So, the only difference is that the current tactic tries some automation on the main goal.

Simon's version is sophisticated and heuristic based.

It only tries solve_by_elim, tauto, and intros, cc additionally on the main goal. I guess if these succeed on the main goal, then you don't need to call wlog at all.

[johoelzl]

So now the discharger for the invariance proofs is included. As discharger I also use now the SMT tactic, I think this should be slightly more powerful than just cc. Still it doesn't work for some obvious cases, e.g. the proof for enumerate_inj doesn't work automatically.

Also, one can use the case command to select the different subgoals.