Duplicates in rw?

Stream: mathlib4

[Bhavik Mehta]

Here's an example:

import Mathlib.Data.Nat.Basic

lemma test (n m : ℕ) : n + m + 1 = m + n + 1 := by
  rw?

The suggestions here are:
image.png

There are three notable things about this list of suggestions:

• It has duplicates of the same lemma, eg add_assoc appears twice
• It has "rough" duplicates of the same lemma, eg AddSemigroup.add_assoc, Nat.add_assoc, add_assoc
• It doesn't contain the rewrite add_comm n m which would close the goal

Is it possible for any of these to be improved? Namely, the first problem might be resolvable by refusing to report a lemma twice; the second by checking syntactic equality of the lemmas or (more likely) deduplicating the result of the rewrite by syntactic equality.

(I'm aware exact? or any other method can be used to clear this particular goal, but my actual example showed up where I did genuinely need a rewrite and rw? instead cluttered the list with a bunch of useless repeats)

[Scott Morrison]

Yes, these should definitely be addressed. I completely forgot to do anything about deduplication, but the way we look up lemmas is extremely prone to it! (rw? actually traverses the entire expression, and looks up each subexpression in a discrimation tree for candidate lemmas.)

A much better implementation of rw? would actually keep track of where it is in the expression, and only apply the lemmas at that subexpression! (As if in conv.) This would be a substantial reimplementation (and would mean that potentially it suggests conv ... rw ... results instead).

But deduplication is easy in the meantime.

[Scott Morrison]

Point 1. is resolved in #6746

[Scott Morrison]

Point 2. is resolved in #6749

[Scott Morrison]

Point 3, that add_comm n m is missing, despite closing the goal, is harder to achieve. The problem is that even nth_rewrite (as implemented in Mathlib 4 --- the implementation in mathlib3 solved this problem but was never ported!) will not find rewrites by different instantiations of the same lemma --- just different locations at which the first possible instantiation works.

[Scott Morrison]

This could be fixed by providing a proper nth_rewrite. Now that rw itself is written in Lean it's easier to do well.

[Scott Morrison]

But better would be to only rewrite subexpressions as we visit them to find rewrite lemmas.

[Bhavik Mehta]

Thanks so much for this, Scott! My hope was that resolving (at least one of) 1, 2 would fix 3, but it seems from what you describe that a more principled implementation of rw? would be necessary?

[Scott Morrison]

There are multiple ways to fix 3.

The good-but-not-perfect approach requires a Lean core patch to how the "occurrences" argument is handled that I would like to get merged. I have it working, but need to write up the motivation/docs/tests. Perhaps next week!

The perfect approach requires some more work.

[Mario Carneiro]

what's the patch?

[Scott Morrison]

@Mario Carneiro https://github.com/semorrison/lean4/pull/5/files#diff-519bcbd0d6c069957197a9c0f0d7768a4bcd1ea02720905668aa08ae205cbfebR47

[Scott Morrison]

That diff does two things: exposes the occs parameter via rw (config := {occs := ...}), but also changes the behaviour of kabstract, so that "rejected" rewrites don't fix the values of mvars.

[Scott Morrison]

I would want to separate out these two changes before making PRs.

[Scott Morrison]

We had an implementation of this in Lean 3, but it jumped through many hoops rather than touching kabstract.

[Scott Morrison]

Here's something that I'd love to see, and perhaps is easy to put together out of pieces:

def traverseSubexpressionsWithConvGoals (e : Expr) (f : Expr → Option (MVarId → MetaM Unit)) : MetaM (Expr × Expr) := ...

which:

• traverses the expression e, visiting every subexpression
• each subexpression is passed to f, which returns an Option
• f returns none if it doesn't want to touch that subexpression
• otherwise, it returns some t, where t : MVarId → MetaM Unit is a tactic that expects a goal of the form x = ?_ (i.e. as in conv mode), where x is the current subexpression.
• if t closes that goal with ?_ unified with some x', then we replace x with x' using that proof, and continue
• at the end, return the modified expression e' along with the proof e' = e.

[Scott Morrison]

(Obviously there are some restrictions about which subexpressions we can actually descend into here, based on available congruence lemmas.)

[Scott Morrison]

I think a tool like this would be generally useful, and would make my preferred implementation of rw? easy to do.

[Scott Morrison]

Currently rw? traverses all subexpressions, using them to look up from the discrimination tree relevant lemmas for rewriting. After doing that, it tries to rewrite the entire expression by any of these lemmas.

Perhaps it should only be rewriting the subexpression that the lemmas are relevant for!

[Damiano Testa]

Scott, I would also like the traverse... definition! I was doing something similar with move_add and felt that besides kabstract and replace there was little support for this.

[Scott Morrison]

Something very close to this was exposed by the simplifier in Lean 3 (which you could use separately from actually firing the simplifier at each visited location).

[Scott Morrison]

Lean.Meta.Simp.simp is rather close to this, actually.

It has signature

def simp (e : Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result := ...

and the monad Lean.Meta.Simp.M is something with read-only Lean.Meta.Simp.Methods and Lean.Meta.Simp.Context, update-able Lean.Meta.State, and otherwise just MetaM.

Methods is:

structure Methods where
  pre        : Expr → SimpM Step          := fun e => return Step.visit { expr := e }
  post       : Expr → SimpM Step          := fun e => return Step.done { expr := e }
  discharge? : Expr → SimpM (Option Expr) := fun _ => return none

where the pre and post functions are essentially of the form for f above. (Here pre and post are distinguish whether we will try to transform the subexpression before or after visiting its subexpressions.) (Here Step contains a flag about whether we should revisit after modifying, and otherwise is just a new expr : Expr along with a proof? : Option Expr (none for defeq modifications).

[Scott Morrison]

So it should be possible to write what I asked for in terms of this.

[Scott Morrison]

This is essentially the same design as ext_simplify_core (I think?) from Lean 3, just a bit more monadic.

[Scott Morrison]

Zero testing, but

import Lean

open Lean Meta Simp

def convSubexpressions (pre post : Expr → MVarId → MetaM Bool := fun _ _ => fail) (e : Expr) :
    MetaM Simp.Result :=
  let go (fn : Expr → MVarId → MetaM Bool) e : SimpM Step := do
    let rhs ← mkFreshExprMVar (← inferType e)
    let eq ← mkFreshExprMVar (← mkEq e rhs)
    return (if ← fn e eq.mvarId! then Step.visit else Step.done) { expr := rhs, proof? := eq }
  (simp e : M Result) |>.run { pre := go pre, post := go post } |>.run {} |>.run' {}

could conceivably be it?

[Scott Morrison]

(Now with both pre and post, and both able to return a bool indicating whether the modified subexpression should be revisited.)

[Scott Morrison]

Having written that, it occurs to me this isn't really what I wanted for rw? in the first place. :-)

[Scott Morrison]

This is getting a bit specific, but I want something like:

def zooms (f : Expr → MVarId → MetaM Unit) (e : Expr) : MLList MetaM (Expr × Expr) := ...

that returns the lazy list generated by looking at each subexpression (accessible via congr lemmas) x of e, applying f to x and a goal x = ?_, and each time it succeeds replacing that subexpression x, giving me the pair e' and pf : e = e'.

[Damiano Testa]

ext_simplify had been suggested by Eric for move_add in Lean 3. All of this looks very similar to what I wanted/did in move_add: I'll see whether I can reuse and recycle!