Rewrite with inequalities

Stream: mathlib4

[Sebastian Zimmer]

I saw Terence Tao complaining on mathstodon about the inability to use inequalities with rw, so I've tried to make a tactic rwi that takes an inequality rather than x = y.

You can see a draft PR here https://github.com/leanprover-community/mathlib4/pull/8167

There's a lot to clean up of course, but it is already functional enough to be useful in my opinion. I'd like some feedback on the general approach:

• Currently most of the work of doing the actual proof is done by gcongr. Is this the right approach? I'm concerned that it's not clear how I handle multiplications where one side can be proven to be negative, so maybe it's not flexible enough?
• I realized half way through the implementation that there isn't really much reason why this should just work for inequalities. It could work for any transitive relations. Should I try to do this or clean up what already works?

[Patrick Massot]

There is also a version of this tactic at https://github.com/teorth/symmetric_project/blob/master/SymmetricProject/Tactic/RwIneq.lean

[Patrick Massot]

It will be interesting to look at the union of test cases and see whether both versions do the same thing.

[Sebastian Zimmer]

It looks very similar, I think my tactic can do all of those examples and probably vice versa (except I can handle > inequalities, but that is a trivial change).

It's interesting that we ended up with such similar solutions. I guess if I go further and try to make it work with arbitrary transitive relations then this won't have been a waste. (Although I learned a lot doing this so not complaining)

[Patrick Massot]

It feels a bit stupid that we worked independently. It didn't occur to me that someone else could be doing it at the same time.

[Patrick Massot]

I was discussing this Terence Tao privately and he is already using my version in his repository because going through the Mathlib review process would clearly have been too slow.

[Patrick Massot]

My version clearly doesn't do rw_ineq [h] when h starts with a forall. I didn't think about handling this.

[Patrick Massot]

It also doesn't do the

lemma test (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≤ 100 - a := by
  rwi [h₁]
  guard_target =ₛ b * c ≤ 100 - b

example which is clearly not the behavior that Tao was expecting. He expected the goal after rewriting to be b * c ≤ 100 - a, but one can argue that you're doing the right thing.

[Sebastian Zimmer]

I was trying to be as similar to rw as possible

[Sebastian Zimmer]

My initial implementation didn't use gcongr. I was manually traversing the expression and only changing values if they were in the right 'direction'.

E.g. rw[ x: a < b] would rewrite a - a <= a - a to b - a <= a - b but this became complicated once I wanted to use mono/congr lemmas and I thought it was kind of confusing

[Yaël Dillies]

Patrick Massot said:

It feels a bit stupid that we worked independently. It didn't occur to me that someone else could be doing it at the same time.

I already mentioned in the past that @Jovan Gerbscheid has a working ordered rewrite tactic.

[Sebastian Zimmer]

Feels like we should get something into mathlib before someone else writes one

[Patrick Massot]

And what is an ordered rewrite tactic? Is it what we are discussing now?

[Patrick Massot]

It seems your version can essentially do all my test except the one testing for the missing instantiateMVar bug:

example {n : ℕ} (bound : n ≤ 5) : n ≤ 10 := by
  have h' := (show 5 ≤ 10 by norm_num)
  rwi [h'] at bound
  assumption

[Patrick Massot]

Your version complains that Provided hypothesis must be an inequality because you forgot to instantiate the meta-variable that have created because the type of h' was not given upfront.

[Patrick Massot]

There are also difference because I call linarith only [h] after rwi [h] to cleanup side-goals.

[Patrick Massot]

Note also that you can use withRWRulesSeq to avoid repeating code from rw.

[Sebastian Zimmer]

Patrick Massot said:

Note also that you can use withRWRulesSeq to avoid repeating code from rw.

that would have saved a lot of time

[Patrick Massot]

You can see how it's used in my code.

[Sebastian Zimmer]

so presumably the reasoning behind using linarith only [h] is that positivity isn't good enough? Or are you ending up with side goals which aren't of the form 0 < x?

[Patrick Massot]

About your "It could work for any transitive relations.", note that my version uses Trans.trans for all transitivity proof. But I think the gain is virtual since I think gcongr itself works only for inequalities and congruence modulo an integer.

[Patrick Massot]

To be honest the example I had was generating a side goal a \le b when I had assumption h : a < b.

[Patrick Massot]

I guess you are doing a better analysis in case of mixing < and \le.

[Patrick Massot]

Anyway, as a Mathlib maintainer I'm very happy to see a new contributor writing tactics, so I strongly suggest that we try to get your version in Mathlib.

[Patrick Massot]

So I suggest that you clean up your code, fix your instantiated metavar bug, refactor using withRWRulesSeq and write documentation. Feel free to steal anything you want from my version, including examples or documentation.

[Sebastian Zimmer]

What's the reasoning behind only wanting to do the rewrite on one side? What I'm doing makes more sense to me, but then I'm not Terence Tao

[Patrick Massot]

That would be the natural thing to do from a mathematical point of view. But I guess that doing more can' t hurt. I will point him towards this thread.

[Sebastian Zimmer]

I guess we could have rwi_lhs and rwi_rhs as well

[Yaël Dillies]

Patrick Massot said:

And what is an ordered rewrite tactic? Is it what we are discussing now?

It is a generalised rewrite tactic restricted to ≤/ <. So yes.

[Sebastian Zimmer]

I can imagine this tactic being useful for much more general targets than we have discussed here.

For example if the target is x ∈ (T ⋃ S) then you should be able to rewrite with R ⊆ S to make the target x ∈ (T ⋃ R). But as you suggest I'll clean up what I've already got first.

[Patrick Massot]

Yaël, I clearly missed the moment you announced that, maybe because I didn't recognize the name. Where is that third version?

[Terence Tao]

Hi, thanks for doing this. For my own project (which will likely end in a few days) Patrick's tool is working fine (although it is noticeably slow for complex inequalities, and particularly for failure cases where no match was possible), but it would be great to have a standard tool in the mathlib.

I was mostly thinking of applying the tool when the inequalities are already in a somewhat normal form in which they are \leq or < rather than \geq or >, and all terms are non-negative when this is relevant due to multiplication operators (or all bases are at least one when working with exponentiation). In such contexts, rw_ineq would naturally only operate on the RHS on hypotheses and on the LHS on goals, but one could indeed extend it to the other side as well after making some guesses as to what is intended to be "positive". I guess by default assuming all terms are positive and/or have base greater than equal to one would be simplest (if one wants to work with negative expressions one can first pull out an explicit minus sign to get rw_ineq to flip the sign of the inequality as needed). I was also guided a bit by the philosophy of making the behavior as predictable as possible, which I understood was a desirable trait of Lean tactics (particularly non-finishing ones).

It's a neat idea to extend to other relations than inequalities, though I don't know how often that use case would actually come up in practice.

[Patrick Massot]

Sebastian, the mention of speed remind me this is also something that needs to be improved. gcongr is faster when you give it a pattern. Maybe there is an efficient way to build a pattern in our case.

[Yaël Dillies]

Patrick Massot said:

Yaël, I clearly missed the moment you announced that, maybe because I didn't recognize the name. Where is that third version?

Here it is: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Mandelbrot.20-.20Lean.204.20version/near/396158326

[Jannis Limperg]

Just FYI, this looks like a much restricted version of Coq's generalised rewriting. There was a previous attempt to bring this to Lean, but it's a rather big project (that probably won't lead to a paper).

[Joachim Breitner]

Was about to say the same thing. Rewriting with arbitrary relations is great! Unless I am missing something it has big a big overlap with gconcr, and as a user who likes the principle of least surprise I’d hope that such a grw would work precisely when gcongr work, and that the same congruence lemma setup will work for both tactics.

[Patrick Massot]

Yaël, is there any visible code?

[Patrick Massot]

The coq documentation starts with "This chapter presents the extension of several equality related tactics to work over user-defined structures (called setoids) that are equipped with ad-hoc equivalence relations meant to behave as equalities." so either this documentation is very misleading or this isn't related. Inequalities are not "meant to behave as equalities".

[Patrick Massot]

Joachim Breitner said:

Was about to say the same thing. Rewriting with arbitrary relations is great! Unless I am missing something it has big a big overlap with gconcr, and as a user who likes the principle of least surprise I’d hope that such a grw would work precisely when gcongr work, and that the same congruence lemma setup will work for both tactics.

This is precisely the case. Both my version and Sebastian's version are built on top of gcongr.

[Jannis Limperg]

The documentation is misleading (or rather, the introduction does not capture the full generality): Coq's generalised rewriting also works with relations that are merely reflexive or symmetric or transitive or any combination of the three properties. See here.

[Terence Tao]

By the way, I'm already using rw_ineq several times in my project https://github.com/teorth/symmetric_project so one could possibly use those instances as more complicated unit tests for any future version of the tool (they are quite far from being a minimal working example, but could perhaps serve as an example of use cases "in the wild"). The tool is primarily used in main.lean and main_lemmas.lean.

EDIT: In particular, these complex use cases could perhaps be used to benchmark performance. For complex rewrites, `rw_ineq' can take several seconds on my laptop, and I ended up splitting my main computation somewhat artificially into several smaller lemmas in order to keep under the heartbeat limit.

[Yaël Dillies]

Patrick Massot said:

Yaël, is there any visible code?

It should be somewhere in https://github.com/Human-Oriented-ATP/lean-tactics but I can't find it right now.

[Yaël Dillies]

I just hope that by tagging @Jovan Gerbscheid enough times he will end up explaining himself what his tactic does and where to find it :grinning:

[Patrick Massot]

Is this the work of Gowers' team?

[Yaël Dillies]

Yes, exactly.

[Jovan Gerbscheid]

Hi there, I've indeed also made a tactic that allows for rewriting with a preorder. It does not work using gcongr, but it is made independently. It uses an interactive point&click system that allows for the user to click on expression for interacting with the move. Yael told me yesterday, that working with explicit subexpression positions (which are pasted into the editor by the interactive system) is not very robust because it is hard to maintain, so he said it would be better to encode position using patterns. This is something that still has to be figured out, but I think there is a lot of potential for point&click moves in Lean.

Anyways, my program works with a type class for monotone functions that I made. It works with any preorder and it doesn't need to be the default instance, so for example one can rewrite with the divisibility relation on natural numbers. Using this type class inference, I find out for every function that it is either monotone increasing or monotone decreasing, and with respect to which order this is. It also works under binders (in particular set builder notation, and quantifiers). In the alternative representation of the proof state that I'm working with, it can unfold foralls, exisist, conditions and conjunctions in the used hypothesis. However if this is going into mathlib, this will probably have to be limited to unfolding foralls and conditions (using forallMetaTelescopeReducing). It doesn't work with multiplication, because thay requires the side condition that the number you multiply by is either positive or negative and I wasn't sure how to choose which one it would be.

I've made some more tactics that work with the point and click system. The simplest on is unfold, which unfolds the definition of the selected expression, so this is the first one I'd like to get into Mathlib. There is als an apply and a rewrite tactic. Notably the rewrite tactic allows for rewriting bound variables which rw in Lean does not. For these moves, I've also made library search variants, which searches the Mathlib library forblemmas that can be aplied, or rewritten or order rewritten with in the selected position. I think this would be a very useful addition to Mathlib.

[Jovan Gerbscheid]

Yaël Dillies said:

I just hope that by tagging Jovan Gerbscheid enough times he will end up explaining himself what his tactic does and where to find it :grinning:

It worked

[Patrick Massot]

Nice! Are you using the framework I provided for conv?, congrm? and the calc widget or are you also duplicating that? I wanted to to the unfold and rw soon so it would be nice if you could start PRing to Mathlib before everything is duplicated.

[Patrick Massot]

More generally it looks like a big project so announcing here that you are working on it would have been very welcome. There is a lot to do and duplicating efforts because of secret projects is no the most efficient approach.

[Jovan Gerbscheid]

I haven't done the work on the interactive system, I've made the tactics. But our code doesn't depend on the conv? congrm? calc framework. The idea for the unfolding move was that you type unfold?, then in the editor you click on an expression and then click on the button for pasting the text into the editor.

[Jovan Gerbscheid]

What do you think about how to represent selected subexpression position? The way it works now is that a list of integers is pasted into the editor, using the Subexpr.Pos encoding of positions.

[Terence Tao]

Jovan Gerbscheid said:

However if this is going into mathlib, this will probably have to be limited to unfolding foralls and conditions (using forallMetaTelescopeReducing). It doesn't work with multiplication, because thay requires the side condition that the number you multiply by is either positive or negative and I wasn't sure how to choose which one it would be.

I'm not sure whether this is feasible, but one could imagine for every side condition to implement a "default" choice (probably the "positive" choice) which is pursued unless the opposite choice is explicitly available in the available hypotheses. So, for instance if one ends up wanting to upper bound a * b, one can assume by default that a is non-negative and look for upper bounds on b (or vice versa, or both), unless the assertion a \leq 0 or a < 0 (or something definitionally equivalent to this) is provided, in which case one looks for lower bounds on b instead. Similarly when seeking upper bounds on an expression like a^b one would assume by default that a \geq 1 and look for upper bounds on b unless it is explicitly provided that a \leq 1 in which case one would seek lower bounds on b. This could perhaps be overengineering though. As a workaround, one can use ordinary rw to replace negative quantities by the negation of positive quantities, and to replace bases less than one by their reciprocal, before invoking the rw_ineq tool, so that one can take advantage of the default option in all cases.

[Mario Carneiro]

This exact issue came up in gcongr, and our approach was just to observe that usage of mul_pos compared to mul_pos_of_neg_of_neg was about 100:1, aka this is only a problem in theory, in practice the choice is obvious

[Patrick Massot]

I added the unfold widget in #8218 since it is a trivial one. It currently support selecting only one location because I think this is by far the most common case, but adding more locations would be easy.

[Patrick Massot]

Let me clarify since the question was asked on GitHub. PR #8218 has nothing to do with Jovan's code. It is an illustration of the fact that the current framework already allows easily writing such widgets.

[Patrick Massot]

I think I found Jovan's version and it inserts a cryptic string into the Lean file while my version inserts an ordinary unfold code that is indistinguishable from code written without using the widget.

[Yaël Dillies]

Ah okay, makes sense.

[Jovan Gerbscheid]

I had a look at your unfold, and what I see is that unfolding 1+1 gives instHAdd.1 1 1. In my version of unfold, it automatically reduces projections, so that this would turn into Add.add 1 1, which I think is a better design.

[Patrick Massot]

It is really not meant to be used in that case so I didn't think about that.

[Jovan Gerbscheid]

My version of unfold also allows you to click on a projection, to unfold it, or on a let expression, to zeta-reduce it, or to click on a lambda that is applied to an argument, to beta-reduce it. These sorts of features really require a position to be selected by the user and the position to be pasted into the editor.

[Eric Wieser]

At that point it should just emit a change tactic

[Kevin Buzzard]

Letting me poke around in the goal (changing it in a defeq way) and then Lean figuring out the corresponding change call would be awesome (although prone to round-tripping errors presumably)

[Eric Wieser]

Is there a tracking issue for the promised lands of round-tripping that were never found?

[Jovan Gerbscheid]

What do you mean with round-tripping?

[Kevin Buzzard]

Cut and paste from the infoview reliably working as input to tactics

[Jovan Gerbscheid]

Why wouldn't it be possible to reliably print expressions as input to tactics?

[Jireh Loreaux]

Because the input to tactics aren't Expressions they're Syntax. The process of going from the former to the latter is called delaboration, and going from the latter to the former is elaboration. Right now our delaboration isn't a perfectly adequate "inverse".

[Jovan Gerbscheid]

Surely it would be possible to check whether the specific result of delaboration is valid, and if not, then run the delaborator again with pp.all set to true (or some other setting that makes the delaboration more specific)? Or is even that not reliable enough?

[Jovan Gerbscheid]

Are there fundamental problems with the conversion between Syntax and Expr, or is it simply that nobody has fixed delab?

[Sebastian Zimmer]

I found some more time to work on this, and I updated my PR with a different approach. https://github.com/leanprover-community/mathlib4/pull/8167

1) The tactic is called grw (consistent with how gcongr generalizes congr)
2) The tactic code does not know anything specific to inequalities. It looks for lemmas tagged @[grw] and some of these happen to describe how to rewrite inequalities. There are also lemmas for handling x ∈ X or X ⊂ Y.
3) The code is much cleaner than before, in my opinion.

I think it's ready for review.

The tactic is already useful, but this is my todo list:

• Test against the examples @Terence Tao mentioned
• Optimize performance. @Patrick Massot mentioned providing a pattern and I think there are other 'easy wins'. (e.g. maintain an index of @[grw] lemmas indexed by relation, sort of like gcongr does)
• Add grw_lhs and grw_rhs, for only operating on one side of a relation at once. I think I can use all the same infrastructure, just the initial kabstract call will need to change.
• Apply rewrite rules inside binders.

I think at least some of that could happen in a followup PR.

[Patrick Massot]

Why can't you reuse the gcongr attribute? What are examples of lemmas that you want to use but gcongr doesn't or the other way around?

[Sebastian Zimmer]

Most of the actual work is still done by gcongr, so those lemmas are still being used. The grw lemmas are just used for the first step. These lemmas look more like transitivity statements than congruence ones. Maybe I'm missing something obvious, but I don't see how you would use gcongr lemmas to achieve this.

[Patrick Massot]

Ok, then I misunderstood the above description and I will need to look at the PR to understand.

[Patrick Massot]

Although I guess the next natural question is: why not using the Trans instance database if you need to tag transitivity lemmas?

[Sebastian Zimmer]

I think you would lose some flexibility there. E.g. we could add a grw lemma showing how to convert Finite x to Finite y using x > y. Now I look at it though, there are a lot of trans lemmas out there. Maybe it could do both?

Right now I'm trying to fix the performance because it is really slow

[Sebastian Zimmer]

I've got grw working as a replacement to rw_ineq in the project @Terence Tao linked.

I put in a few withReducibles and it's fast now (>100x faster than rw_ineq in many cases) seemingly without breaking it. The biggest difference in use is that rw_ineq allows side goals whereas grw expects any side goal that comes up in grw to be solved with either assumption or positivity, otherwise it fails. In practice that looks like:

rw_ineq [h1]
. prove side goal

turns into

have := prove side goal
grw [h1]

This might be a bit annoying, but it makes it much more backwards compatible since adding new side goal dischargers to grw is safe with this api. Since I intend this to be used nonterminally, I think that's quite important.

Currently the worst thing about using grw is how useless the errors are.

[Joachim Breitner]

Great! About three “side goals” that almost every tactic has to deal with: it doesn't seem to compose and scale well if every tactic does their own little thing. I expect you'll soon run into cases where some lemma have side goals that need something stronger, but where just adding them to the environment is too tedious.

It would be better if there is a commonly used, commonly accepted extensible tactic for “side goals that must be solved in an otherwise unrelated tactics”. As the developer if grw you shouldn't have to make decisions here - and as user I want to be able to predict what happens without reading tactic code or docs.

Could aesop be that? I hope it subsumes assumption and positivity, and can easily be extended with more logic?

Or is there already an accepted tactic for this?

(This is getting off topic for grw because it is more a matter of consistency across tactics.)

[Sebastian Zimmer]

I think the closest thing to an accepted tactic for this is gcongr_discharger, which just calls positivity.

[Sebastian Zimmer]

aesop could probably work, the side goal discharger is much less performance sensitive than the main goal discharger, plus there is an expectation that the statement is actually provable

[Joachim Breitner]

Using the same as gcongr is already a good step towards the principle of least surprise :-)

[Sebastian Zimmer]

That would mean not having assumption, in which case I would have to add unfilled side goals to the context instead of failing. This is what other tactics do, but I don't like it because if people depend on this then improving the tactic would break proofs (like how adding simp lemmas breaks nonterminal simps)

[Joachim Breitner]

Yeah, that's strange. So gcongr will automatically discharge positivity assumptions, but not assumptions that are already in the context? Isn't that suboptimal? (Or does positivity happen to run assumption?)

[Damiano Testa]

I tend to expect tactic! to try harder than tactic to do whatever the tactic is expected to do. Thus, I would expect grw to not try anything, other than the "rw". The one with the discharger would then simply be "first do grw, then try assumption/positivity/Aesop/norm_num/..." as appropriate.

[Sebastian Zimmer]

We have to do something with side goals otherwise the tactic is useless for anything involving a multiplication.

[Heather Macbeth]

Can you use gcongr_forward (which subsumes assumption)? That's the discharger gcongr uses for "main" goals.

[Sebastian Zimmer]

Could do but we'd still want positivity

[Heather Macbeth]

I looked briefly at your code and I agree that since this is explicitly supposed to be a discharger of side goals, gcongr_forward is not appropriate.

[Heather Macbeth]

Sebastian Zimmer said:

That would mean not having assumption, in which case I would have to add unfilled side goals to the context instead of failing. This is what other tactics do, but I don't like it because if people depend on this then improving the tactic would break proofs (like how adding simp lemmas breaks nonterminal simps)

Personally I prefer this approach. It's true that there is a possibility of it breaking proofs in the future, but it is an easy thing to clean up after (much easier than cleaning up after a broken nonterminal simp would be). And it's very user-friendly to present unsolved goals to the user -- much more user-friendly than making the user anticipate beforehand what facts might be needed and write them out.

[Sebastian Zimmer]

I made the two requested changes

• Use gcongr_discharger to discharge the sidegoals (instead of try positivity; assumption
• Add unfilled side goals to the context

[Scott Morrison]

I've left some review comments. This is great!

[Sebastian Zimmer]

I've fixed the review comments, is there any obstacle to merging this?

There's still stuff I want to do

• Try using transitivity lemmas in addition to the @[grw] lemmas
• Add grw_lhs and grw_rhs
• Rewrite inside binders

But IMO this all can be done in future PRs