rewrite_search

Stream: mathlib4

[Scott Morrison]

I've had another go at rewrite_search! This time it is backed by the same DiscrTree that powersrw?, and seems to be reasonably fast (no tagging of lemmas, this is just trying the whole library):

rewrite_search.gif

There will be quite a few PRs before there's something to play with. In the meantime, the following PRs are all requirements:

• #5957
• #6061
• #6062
• #6088

[Scott Morrison]

The same ingredients should also allow a tactic to transform simp only [...] blocks into simp_rw [...].

[Johan Commelin]

I kicked the 2nd and 3rd PR on the queue

[Johan Commelin]

The last one contains meta stuff.

[Siddhartha Gadgil]

I noticed this really nice code-action which comes when there is a "try this" tactic. Can someone point me to the implementation?

[Scott Morrison]

It is spread across Mathlib and Std, it depends a bit exactly what part of the mechanism you are looking for. I would recommend starting with a tactic that uses this, e.g. exact?, and working your way back.

[Patrick Massot]

https://github.com/leanprover/std4/blob/main/Std/Tactic/TryThis.lean#L51

[Scott Morrison]

If you are writing tactics you will be using addExactSuggestion or its relatives, some of which are in Mathlib.Tactic.TryThis.

[Siddhartha Gadgil]

I am looking for the implementation of the code action to learn how to write such code actions.

[Scott Morrison]

Then Patrick's link is what you need!

[Siddhartha Gadgil]

Thanks @Patrick Massot

[Siddhartha Gadgil]

I will follow links from there.

[Siddhartha Gadgil]

I saw how to get the content of the "Try this" from the says implementation. Thanks @Scott Morrison

[Scott Morrison]

The rw_search PR is now up as #6120 and depends on #6090, #6096, #6097, #6115, #6117, #6118, #6119.

[Scott Morrison]

This PR is finally actually compiling, if anyone would like to give it a test drive. I think it is quite useful already, and can be made even better (allow rewriting using local hypotheses, allowing using occurrences in rw, add simp as a step, tweak the search heuristics, etc) over time. The dependency list is quite long, however!

• [ ] depends on: #5957
• [ ] depends on: #6088
• [ ] depends on: #6090
• [ ] depends on: #6092
• [ ] depends on: #6096
• [ ] depends on: #6097
• [x] depends on: #6115
• [ ] depends on: #6117
• [ ] depends on: #6118
• [ ] depends on: #6119

[Jason Rute]

It’s awesome you got this working! In the past I recall a feeling from others that one eventually needs ML (or something) to guide a rw search since there are just too many rw lemmas which say use _ + _, and you have to rank them. Do you feel this is still the case, or is it fast even in those situations because of the better data structures?

[Jason Rute]

The conversation I had in mind was #Machine Learning for Theorem Proving > rw_hint

[Scott Morrison]

I mean, I've always been a bit dubious about the "too slow" claim. Even back in Lean 3, my original implementation of rewrite_search in 2018 often successfully found ~10 step rewrite proofs. Yes, in some cases it will be too slow, of course.

[Scott Morrison]

Good premise selection that could order the lemmas before we even try rewriting by them would of course speed things up.

[Scott Morrison]

And good "how close are these goal" judgements (rather than just edit distances) would make the search more efficient.

[Scott Morrison]

This implementation is intended to be a starting point, not an end. It's a framework into which you can easily plug other heuristics for ordering lemmas, or distances between Expr.

[Scott Morrison]

A nice feature of the new implementation is that it "watches the clock", and if it gets too close to maxHeartbeats it just reports its best effort up to that point, rather than failing with a timeout.

[Scott Morrison]

The rw_search PR is waiting for review. @Anne Baanen gave it a review a few weeks ago, but it could do with another look / merging.

[Scott Morrison]

I know that it is far from optimal (in terms of both efficiency and heuristics for directing the search), but I think it is an interesting addition to our automation toolkit. Optimistically, we will wonder how we lived without it. :-) Pessimistically it will be too slow for practical use.

[Scott Morrison]

There are many additional improvements that can be made:

• add simp as an atomic step
• better ordering of lemmas (i.e. improve the output of rw?)
• use local hypotheses to discharge side condition of rewrites (i.e. do this in rw?)
• better heuristics for search (currently we use unweighted edit distance on a particular tokenisation scheme; either weights or different tokenisation could help; or drop in a neural model!)
• A* search instead of best-first search
• bidirectional search (currently if we rewrite lhs to lhs' and separately rhs to rhs' in a different search branch, we have no way of noticing if lhs' and rhs' are really close, until we do those rewrites sequentially)

[Scott Morrison]

However I would prefer that all of these improvements could be "tested in production"!

[Joachim Breitner]

Just host it online somehow, that's a great way to get testing before the PR gets merged, and because you get a stream of suggestions and bugreports, the PR never really settles down, but at least you can fix them without delay.
(Just kidding, of course doesn't apply to new tactics.)

[Scott Morrison]

We need an API for remote tactics.

[Scott Morrison]

(Only half joking?)

[Jireh Loreaux]

Isn't that sort of what polyrith is?

[Bolton Bailey]

I am trying to play around with it. I pulled the branch and copied

example (xs ys : List α) :
    (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by
  rw_search

from the test examples into Mathlib/Data/Polynomial/Div.lean. It took about two minutes , while the test in test/rw_search.lean only took a second at most. Why does it apparently take so much longer when using it IRL?

[Bolton Bailey]

Maybe it's the autoImplicit?

[Bolton Bailey]

Seems it is the autoImpilcit, sorry (although weirdly it does still produce the right output, even when there's an error in the definition.

[Scott Morrison]

What do you mean? Could you show me the fast and slow versions?

[Scott Morrison]

Does it suffice to just import Mathlib.Data.Polynomial.Div to get the slow down, rather than putting the example in that file?

[Bolton Bailey]

Here is the file I ran

/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
-/
import Mathlib.Data.Polynomial.AlgebraMap
import Mathlib.Data.Polynomial.Inductions
import Mathlib.Data.Polynomial.Monic
import Mathlib.RingTheory.Multiplicity
import Mathlib.Tactic.RewriteSearch


#align_import data.polynomial.div from "leanprover-community/mathlib"@"e1e7190efdcefc925cb36f257a8362ef22944204"

/-!
# Division of univariate polynomials

The main defs are `divByMonic` and `modByMonic`.
The compatibility between these is given by `modByMonic_add_div`.
We also define `rootMultiplicity`.
-/


noncomputable section

open Classical BigOperators Polynomial

open Finset

namespace Polynomial

universe u v w z

variable {R : Type u} {S : Type v} {T : Type w} {A : Type z} {a b : R} {n : ℕ}

example (xs ys : List α) :
    (xs ++ ys ++ ys).length = 2 * ys.length + xs.length := by
  rw_search

[Bolton Bailey]

I'm not too worried about it, I assume it's just something weird to do with things taking longer when you have a sorryAx in your state.

[Bolton Bailey]

Here's another thing which I'm now confused by though, if I try to replace the rw on line 440 of Polynomial.Div with rw_search it gives an error Goal is not an equality. Why is this?

[Bolton Bailey]

Sorry it's not easy to give a MWE here, I'll work on it.

[Bolton Bailey]

This is as much as I can get rid of

/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
-/
import Mathlib.Data.Polynomial.AlgebraMap
import Mathlib.Data.Polynomial.Inductions
import Mathlib.Data.Polynomial.Monic
import Mathlib.RingTheory.Multiplicity
import Mathlib.Tactic.RewriteSearch


#align_import data.polynomial.div from "leanprover-community/mathlib"@"e1e7190efdcefc925cb36f257a8362ef22944204"

/-!
# Division of univariate polynomials

The main defs are `divByMonic` and `modByMonic`.
The compatibility between these is given by `modByMonic_add_div`.
We also define `rootMultiplicity`.
-/


noncomputable section

open Classical BigOperators Polynomial

open Finset

namespace Polynomial

universe u v w z

variable {R : Type u} {S : Type v} {T : Type w} {A : Type z} {a b : R} {n : ℕ}

section CommSemiring

variable [CommSemiring R]

theorem X_dvd_iff {f : R[X]} : X ∣ f ↔ f.coeff 0 = 0 :=
  ⟨fun ⟨g, hfg⟩ => by rw [hfg, mul_comm, coeff_mul_X_zero], fun hf =>
    ⟨f.divX, by rw [mul_comm, ← add_zero (f.divX * X), ← C_0, ← hf, divX_mul_X_add]⟩⟩
set_option linter.uppercaseLean3 false in
#align polynomial.X_dvd_iff Polynomial.X_dvd_iff

theorem X_pow_dvd_iff {f : R[X]} {n : ℕ} : X ^ n ∣ f ↔ ∀ d < n, f.coeff d = 0 :=
  ⟨fun ⟨g, hgf⟩ d hd => by
    simp only [hgf, coeff_X_pow_mul', ite_eq_right_iff, not_le_of_lt hd, IsEmpty.forall_iff],
    fun hd => by
    induction' n with n hn
    · simp [pow_zero, one_dvd]
    · obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
      have := coeff_X_pow_mul g n 0
      rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
      obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
      use k
      rwa [pow_succ, mul_comm X _, mul_assoc, ← hgk]⟩
set_option linter.uppercaseLean3 false in
#align polynomial.X_pow_dvd_iff Polynomial.X_pow_dvd_iff

end CommSemiring

section CommSemiring

variable [CommSemiring R] {p q : R[X]}

theorem multiplicity_finite_of_degree_pos_of_monic (hp : (0 : WithBot ℕ) < degree p) (hmp : Monic p)
    (hq : q ≠ 0) : multiplicity.Finite p q :=
  have zn0 : (0 : R) ≠ 1 :=
    haveI := Nontrivial.of_polynomial_ne hq
    zero_ne_one
  ⟨natDegree q, fun ⟨r, hr⟩ => by
    have hp0 : p ≠ 0 := fun hp0 => by simp [hp0] at hp
    have hr0 : r ≠ 0 := fun hr0 => by subst hr0; simp [hq] at hr
    have hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1 := by simp [show _ = _ from hmp]
    have hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0 := hpn1.symm ▸ zn0.symm
    have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by
      simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_pow, one_mul, Ne.def,
          hr0]
    have hnp : 0 < natDegree p := Nat.cast_lt.1 <| by
      rw [← degree_eq_natDegree hp0]; exact hp
    have := congr_arg natDegree hr
    rw [natDegree_mul' hpnr0, natDegree_pow' hpn0', add_mul, add_assoc] at this
    exact
      ne_of_lt
        (lt_add_of_le_of_pos (le_mul_of_one_le_right (Nat.zero_le _) hnp)
          (add_pos_of_pos_of_nonneg (by rwa [one_mul]) (Nat.zero_le _)))
        this⟩
#align polynomial.multiplicity_finite_of_degree_pos_of_monic Polynomial.multiplicity_finite_of_degree_pos_of_monic

end CommSemiring

section Ring

variable [Ring R] {p q : R[X]}

theorem div_wf_lemma (h : degree q ≤ degree p ∧ p ≠ 0) (hq : Monic q) :
    degree (p - C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p :=
  have hp : leadingCoeff p ≠ 0 := mt leadingCoeff_eq_zero.1 h.2
  have hq0 : q ≠ 0 := hq.ne_zero_of_polynomial_ne h.2
  have hlt : natDegree q ≤ natDegree p :=
    Nat.cast_le.1
      (by rw [← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]; exact h.1)
  degree_sub_lt
    (by
      rw [hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
        degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt])
    h.2 (by rw [leadingCoeff_mul_monic hq, leadingCoeff_mul_X_pow, leadingCoeff_C])
#align polynomial.div_wf_lemma Polynomial.div_wf_lemma

/-- See `divByMonic`. -/
noncomputable def divModByMonicAux : ∀ (_p : R[X]) {q : R[X]}, Monic q → R[X] × R[X]
  | p, q, hq =>
    if h : degree q ≤ degree p ∧ p ≠ 0 then
      let z := C (leadingCoeff p) * X ^ (natDegree p - natDegree q)
      have _wf := div_wf_lemma h hq
      let dm := divModByMonicAux (p - z * q) hq
      ⟨z + dm.1, dm.2⟩
    else ⟨0, p⟩
  termination_by divModByMonicAux p q hq => p
#align polynomial.div_mod_by_monic_aux Polynomial.divModByMonicAux

/-- `divByMonic` gives the quotient of `p` by a monic polynomial `q`. -/
def divByMonic (p q : R[X]) : R[X] :=
  if hq : Monic q then (divModByMonicAux p hq).1 else 0
#align polynomial.div_by_monic Polynomial.divByMonic

/-- `modByMonic` gives the remainder of `p` by a monic polynomial `q`. -/
def modByMonic (p q : R[X]) : R[X] :=
  if hq : Monic q then (divModByMonicAux p hq).2 else p
#align polynomial.mod_by_monic Polynomial.modByMonic

@[inherit_doc]
infixl:70 " /ₘ " => divByMonic

@[inherit_doc]
infixl:70 " %ₘ " => modByMonic

theorem degree_modByMonic_lt [Nontrivial R] :
    ∀ (p : R[X]) {q : R[X]} (_hq : Monic q), degree (p %ₘ q) < degree q
  | p, q, hq =>
    if h : degree q ≤ degree p ∧ p ≠ 0 then by
      have _wf := div_wf_lemma ⟨h.1, h.2⟩ hq
      have :
        degree ((p - C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) %ₘ q) < degree q :=
        degree_modByMonic_lt (p - C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq
      unfold modByMonic at this ⊢
      unfold divModByMonicAux
      dsimp
      rw [dif_pos hq] at this ⊢
      rw [if_pos h]
      exact this
    else
      Or.casesOn (not_and_or.1 h)
        (by
          unfold modByMonic divModByMonicAux
          dsimp
          rw [dif_pos hq, if_neg h]
          exact lt_of_not_ge)
        (by
          intro hp
          unfold modByMonic divModByMonicAux
          dsimp
          rw [dif_pos hq, if_neg h, Classical.not_not.1 hp]
          exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 hq.ne_zero)))
  termination_by degree_modByMonic_lt p q hq => p
#align polynomial.degree_mod_by_monic_lt Polynomial.degree_modByMonic_lt

end Ring

section CommRing

variable [CommRing R] {p q : R[X]}

theorem X_dvd_sub_C : X ∣ p - C (p.coeff 0) := by
  simp [X_dvd_iff, coeff_C]

theorem modByMonic_eq_sub_mul_div :
    ∀ (p : R[X]) {q : R[X]} (_hq : Monic q), p %ₘ q = p - q * (p /ₘ q)
  | p, q, hq =>
    if h : degree q ≤ degree p ∧ p ≠ 0 then by
      have _wf := div_wf_lemma h hq
      have ih :=
        modByMonic_eq_sub_mul_div (p - C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) hq
      unfold modByMonic divByMonic divModByMonicAux
      dsimp
      rw [dif_pos hq, if_pos h]
      rw [modByMonic, dif_pos hq] at ih
      refine' ih.trans _
      unfold divByMonic
      rw [dif_pos hq, dif_pos hq, if_pos h, mul_add, sub_add_eq_sub_sub, mul_comm]
    else by
      unfold modByMonic divByMonic divModByMonicAux
      dsimp
      rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero]
  termination_by modByMonic_eq_sub_mul_div p q hq => p
#align polynomial.mod_by_monic_eq_sub_mul_div Polynomial.modByMonic_eq_sub_mul_div

@[simp]
theorem modByMonic_X_sub_C_eq_C_eval (p : R[X]) (a : R) : p %ₘ (X - C a) = C (p.eval a) := by
  nontriviality R
  have h : (p %ₘ (X - C a)).eval a = p.eval a := by
    rw [modByMonic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul, eval_sub, eval_X,
      eval_C, sub_self, zero_mul, sub_zero]
  have : degree (p %ₘ (X - C a)) < 1 :=
    degree_X_sub_C a ▸ degree_modByMonic_lt p (monic_X_sub_C a)
  have : degree (p %ₘ (X - C a)) ≤ 0 := by
    revert this
    cases degree (p %ₘ (X - C a))
    · exact fun _ => bot_le
    · exact fun h => WithBot.some_le_some.2 (Nat.le_of_lt_succ (WithBot.some_lt_some.1 h))
  rw [eq_C_of_degree_le_zero this, eval_C] at h
  rw_search
  rw [eq_C_of_degree_le_zero this, h]
set_option linter.uppercaseLean3 false in
#align polynomial.mod_by_monic_X_sub_C_eq_C_eval Polynomial.modByMonic_X_sub_C_eq_C_eval

end CommRing

end Polynomial

[Scott Morrison]

Ah, I think one problem here is that rw? still doesn't use local hypotheses, so you won't be able to do this rewrite anyway. :-(

[Bolton Bailey]

True. However, it's still concerning that the error message is misleading.

[Scott Morrison]

Oh, I'm wrong, it will rewrite by local hypotheses.

[Scott Morrison]

Looking at the incorrect "Goal is not an equality" error now.

[Scott Morrison]

What it won't do is discharge side conditions, so it can't do the rw [eq_C_of_degree_le_zero this] step.

[Bolton Bailey]

Incidentally, why did you opt for having rw_search only work on equalities? It seems like another option you could have taken would have been to let the metric be "number of tokens in the expression" rather than "Levenshtein distance between the sides of an equality". Would you expect the former not to work well for some reason?

[Scott Morrison]

Gah, it is stupid metadata nodes.

[Scott Morrison]

Ok, fixed.

[Mario Carneiro]

looks like a missing whnfR

[Scott Morrison]

Oh, hmm, that's better.

[Scott Morrison]

Bolton Bailey said:

Incidentally, why did you opt for having rw_search only work on equalities? It seems like another option you could have taken would have been to let the metric be "number of tokens in the expression" rather than "Levenshtein distance between the sides of an equality". Would you expect the former not to work well for some reason?

Good question. The original idea for rw_search was definitely about doing bidirectional search from both ends. This version is simpler, and while it can rewrite both sides of the equation, it's not keeping separate pools of LHSs and RHSs.

[Scott Morrison]

It would certainly be possible to have a version that just tried to make expressions smaller.

[Scott Morrison]

(but would still go uphill when it ran out of things to do, but only in the way that water can go uphill :-)

[Scott Morrison]

Huh. Allowing rw? to discharge side conditions using local hypotheses was surprisingly easy: #7770

[Bolton Bailey]

I sort of expected rw_search to be able to prove this lemma, and I was disappointed it didn't. Is this not the sort of lemma that rw_search targets?

import Mathlib.Data.Polynomial.Eval

@[simp]
theorem Polynomial.natDegree_sub_C {R : Type u} [Ring R] {p : Polynomial R} {a : R} :
    Polynomial.natDegree (p - Polynomial.C a) = Polynomial.natDegree p := by
  rw_search -- Try this: rw []
  -- rw [sub_eq_add_neg, ← Polynomial.C_neg, Polynomial.natDegree_add_C] -- works

[Bolton Bailey]

Maybe it's a "water flowing uphill" issue?

[Scott Morrison]

That is a frustrating example. rw? gets each individual step, (3rd suggestion for the first rewrite, 2nd suggestion for the second rewrite), so it certainly feels like rw_search should cope.

[Scott Morrison]

Okay, I have implemented basic tracing, and can see what is going wrong in this example.

[Scott Morrison]

The basic answer is that we need A* search.

[Scott Morrison]

But there are some other de-duplication problems as well.

[Scott Morrison]

I've solved the duplication problems, and have a relatively simple idea that may solve the problem with getting stuck.

[Scott Morrison]

Well, after spending a bit longer on this than I initially planned, it can do the Polynomial.natDegree_sub_C problem above, with maxHeartbeats 300000 (so 150% of the usual limit).

[Scott Morrison]

There is still a FIFO/FILO problem that is causing it to try unpromising lemmas before promising lemmas. :-(

[Bolton Bailey]

Scott Morrison said:

Well, after spending a bit longer on this than I initially planned, it can do the Polynomial.natDegree_sub_C problem above, with maxHeartbeats 300000 (so 150% of the usual limit).

That's awesome! I'll point out that that lemma was a completely new lemma that I needed for my project, so if rw_search can prove it then it has already proven its usefulness.

This maybe opens up a new discussion: Search tactics by their nature can take a long time, and it might be nice at some point to have the capability to sorry a short lemma and let it cook for a while in the hopes that it will be solved when one comes back to it. I'm not sure how this fits into the heartbeat infrastructure.

[Scott Morrison]

I think that same discussion applies to neural search! We need a mechanism for bots to go work on sorries offline. :-)

[Scott Morrison]

Unfortunately, making this example work has broken all the other examples, oops. I guess this PR is back to WIP until I have some more time for it.

[Scott Morrison]

It did not find your proof, by the way: it finds

rw [← @neg_sub, @natDegree_neg, @sub_eq_neg_add, @natDegree_add_C, @natDegree_neg]

[Scott Morrison]

Strangely, it wanders around for a while trying various things, and then when it eventually hits on neg_sub is finishes the remaining steps quickly. :woman_shrugging:

[Scott Morrison]

Oh no, @Bolton Bailey, your PR has been merged and it spoils my test, because rw_search now finds natDegree_sub_C :-)

[Bolton Bailey]

Do you want another theorem?

[Bolton Bailey]

theorem Polynomial.X_mul_divX [Field F] (p : Polynomial F) :
    Polynomial.X * Polynomial.divX p = p - Polynomial.C (Polynomial.coeff p 0) := by
  rw [eq_sub_iff_add_eq, Polynomial.X_mul_divX_add]

[Scott Morrison]

I think actually I want my test back sufficiently that I am going to implement rw_search [-natDegree_sub_C]!

[Alex J. Best]

Bolton Bailey said:

This maybe opens up a new discussion: Search tactics by their nature can take a long time, and it might be nice at some point to have the capability to sorry a short lemma and let it cook for a while in the hopes that it will be solved when one comes back to it. I'm not sure how this fits into the heartbeat infrastructure.

@Siddhartha Gadgil's https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Aesop.20etc.20in.20the.20background/near/378792005 seems related to what you want

[Scott Morrison]

Bolton Bailey said:

theorem Polynomial.X_mul_divX [Field F] (p : Polynomial F) :
    Polynomial.X * Polynomial.divX p = p - Polynomial.C (Polynomial.coeff p 0) := by
  rw [eq_sub_iff_add_eq, Polynomial.X_mul_divX_add]

I think this one is asking a bit much from rw_search. It's great at massaging subexpressions into the right shape, but anytime an initial segment of the rewrites is just completely changing the structure it's doesn't really have a chance.

[Scott Morrison]

Oops. As I was writing that, I left it on with maxHeartbeats 0, and it came up with

rw [@X_mul, @eq_sub_iff_add_eq, @divX_mul_X_add]

[Jireh Loreaux]

@Scott Morrison I just did this proof in another thread by hand (because it wasn't hard), but then I thought: :thinking: this is the kind of thing rw_search should be able to do. So, I pulled the branch and tested it, and I'm very pleased to report that this worked almost instantly :tada: :octopus:

import Mathlib

open Filter OnePoint Topology

example : comap ((↑) : ℕ → OnePoint ℕ) (𝓝 ∞) = atTop := by
  rw [@comap_coe_nhds_infty, @coclosedCompact_eq_cocompact, Nat.cocompact_eq]

and it even found a one-step shorter rewrite than I came up with by hand!

[Jireh Loreaux]

Needless to say, I'm stoked to have this hit mathlib.

[Scott Morrison]

I would be stoked to have this hit mathlib too. :-)

[Scott Morrison]

Since the last discussion here, I found time to do some basic optimisation of the "penalty function" n.lastIdx.log2 + n.ppGoal.length.log2 (this is the log base two of the index of the latest lemma tried from rw?, which encouraged "trusting" the ordering provided by rw?, plus the log base two of the entire pretty printed goal), and achieved a 2x speed-up on the test suite.

This penalty function is added to the Levenshtein distance between the two sides. It's pretty ad-hoc, but I sampled quite a few variants (coefficients, without logs, some other terms as well), and this gives the best performance on examples so far. Of course, 10x as many examples would allow better optimisation.

[Scott Morrison]

(Oh, and just reporting on some issues upthread: the FILO/FIFO issue above has been resolved, and the Polynomial.natDegree_sub_C example no longer requires a maxHeartbeats bump.)

[Jireh Loreaux]

Scott, can you cull (in an automated fashion) all theorems from Mathlib whose proof is just a sequence of rewrites to test on? Certainly some of them will include things that aren't declarations in the list, but maybe it's not too hard to remove those after the fact.

[Scott Morrison]

Yes, I can. There are tools for things like this in the lean-training-data repo. But I don't think I have the time available to do this for rw_search in the near future.

[Damiano Testa]

@Scott Morrison I wrote a rather crude tool that tries to extract "rw-only" proofs from a file and produce a standalone with the extracted lemmas. It is mostly string-based, so very buggy, but here is the output on Mathlib.Data.Polynomial.Degree.Definitions:

import Mathlib.Data.Polynomial.Degree.Definitions

universe u v

open
  BigOperators
  Finset
  Finsupp
  Polynomial

-- Polynomial.degree_of_subsingleton.{u}
example {R : Type u} [Semiring R] {p : Polynomial R} [Subsingleton R] :
    Polynomial.degree p = ⊥ := by
  rw [Subsingleton.elim p 0, degree_zero]
  done

-- Polynomial.natDegree_of_subsingleton.{u}
example {R : Type u} [Semiring R] {p : Polynomial R}
    [Subsingleton R] : Polynomial.natDegree p = 0 := by
  rw [Subsingleton.elim p 0, natDegree_zero]
  done

-- Polynomial.degree_C_mul_X_pow.{u}
example {R : Type u} {a : R} [Semiring R] (n : ℕ) (ha : a ≠ 0) :
    Polynomial.degree (Polynomial.C a * Polynomial.X ^ n) = n := by
  rw [C_mul_X_pow_eq_monomial, degree_monomial n ha]
  done

-- Polynomial.Monic.eq_X_add_C.{u}
example {R : Type u} [Semiring R] {p : Polynomial R} (hm : Polynomial.Monic p)
    (hnd : Polynomial.natDegree p = 1) : p = Polynomial.X + Polynomial.C (Polynomial.coeff p 0) := by
  rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]
  done

-- Polynomial.nonempty_support_iff.{u}
example {R : Type u} [Semiring R] {p : Polynomial R} :
    Finset.Nonempty (Polynomial.support p) ↔ p ≠ 0 := by
  rw [Ne.def, nonempty_iff_ne_empty, Ne.def, ← Polynomial.support_eq_empty]
  done

-- Polynomial.natDegree_int_cast.{u}
example {R : Type u} [Ring R] (n : ℤ) : Polynomial.natDegree (n : R[X]) = 0 := by
  rw [← C_eq_int_cast, natDegree_C]
  done

-- Polynomial.leadingCoeff_neg.{u}
example {R : Type u} [Ring R] (p : Polynomial R) :
    Polynomial.leadingCoeff (-p) = -Polynomial.leadingCoeff p := by
  rw [leadingCoeff, leadingCoeff, natDegree_neg, coeff_neg]
  done

-- Polynomial.leadingCoeff_ne_zero.{u}
example {R : Type u} [Semiring R] {p : Polynomial R} :
    Polynomial.leadingCoeff p ≠ 0 ↔ p ≠ 0 := by
  rw [Ne.def, leadingCoeff_eq_zero]
  done

-- Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot.{u}
example {R : Type u} [Semiring R] {p : Polynomial R} :
    Polynomial.leadingCoeff p = 0 ↔ Polynomial.degree p = ⊥ := by
  rw [leadingCoeff_eq_zero, degree_eq_bot]
  done

-- Polynomial.degree_add_eq_right_of_degree_lt.{u}
example {R : Type u} [Semiring R] {p q : Polynomial R}
    (h : Polynomial.degree p < Polynomial.degree q) : Polynomial.degree (p + q) = Polynomial.degree q := by
  rw [add_comm, degree_add_eq_left_of_degree_lt h]
  done

-- Polynomial.leadingCoeff_C_mul_X_pow.{u}
example {R : Type u} [Semiring R] (a : R) (n : ℕ) :
    Polynomial.leadingCoeff (Polynomial.C a * Polynomial.X ^ n) = a := by
  rw [C_mul_X_pow_eq_monomial, leadingCoeff_monomial]
  done

-- Polynomial.C_mul_X_pow_eq_self.{u}
example {R : Type u} [Semiring R] {p : Polynomial R}
    (h : Finset.card (Polynomial.support p) ≤ 1) :
    Polynomial.C (Polynomial.leadingCoeff p) * Polynomial.X ^ Polynomial.natDegree p = p := by
  rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]
  done

-- Polynomial.zero_le_degree_iff.{u}
example {R : Type u} [Semiring R] {p : Polynomial R} : 0 ≤ Polynomial.degree p ↔ p ≠ 0 := by
  rw [← not_lt, Nat.WithBot.lt_zero_iff, degree_eq_bot]
  done

-- Polynomial.natDegree_eq_zero_iff_degree_le_zero.{u}
example {R : Type u} [Semiring R] {p : Polynomial R} :
    Polynomial.natDegree p = 0 ↔ Polynomial.degree p ≤ 0 := by
  rw [← nonpos_iff_eq_zero, natDegree_le_iff_degree_le, Nat.cast_zero]
  done

-- Polynomial.degree_linear.{u}
example {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) :
    Polynomial.degree (Polynomial.C a * Polynomial.X + Polynomial.C b) = 1 := by
  rw [degree_add_eq_left_of_degree_lt <| degree_C_lt_degree_C_mul_X ha, degree_C_mul_X ha]
  done

-- Polynomial.natDegree_linear.{u}
example {R : Type u} {a b : R} [Semiring R] (ha : a ≠ 0) :
    Polynomial.natDegree (Polynomial.C a * Polynomial.X + Polynomial.C b) = 1 := by
  rw [natDegree_add_C, natDegree_C_mul_X a ha]
  done

-- Polynomial.degree_X_pow.{u}
example {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) :
    Polynomial.degree (Polynomial.X ^ n : R[X]) = n := by
  rw [X_pow_eq_monomial, degree_monomial _ (one_ne_zero' R)]
  done

-- Polynomial.degree_X_sub_C.{u}
example {R : Type u} [Ring R] [Nontrivial R] (a : R) :
    Polynomial.degree (Polynomial.X - Polynomial.C a) = 1 := by
  rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]
  done

-- Polynomial.natDegree_X_sub_C.{u}
example {R : Type u} [Ring R] [Nontrivial R] (x : R) :
    Polynomial.natDegree (Polynomial.X - Polynomial.C x) = 1 := by
  rw [natDegree_sub_C, natDegree_X]
  done

-- Polynomial.nextCoeff_X_sub_C.{v}
example {S : Type v} [Ring S] (c : S) :
    Polynomial.nextCoeff (Polynomial.X - Polynomial.C c) = -c := by
  rw [sub_eq_add_neg, ← map_neg C c, nextCoeff_X_add_C]
  done

-- Polynomial.degree_X_pow_sub_C.{u}
example {R : Type u} [Ring R] [Nontrivial R] {n : ℕ} (hn : 0 < n) (a : R) :
    Polynomial.degree (Polynomial.X ^ n - Polynomial.C a) = n := by
  rw [sub_eq_add_neg, ← map_neg C a, degree_X_pow_add_C hn]
  done

-- Polynomial.natDegree_X_pow_sub_C.{u}
example {R : Type u} [Ring R] [Nontrivial R] {n : ℕ} {r : R} :
    Polynomial.natDegree (Polynomial.X ^ n - Polynomial.C r) = n := by
  rw [sub_eq_add_neg, ← map_neg C r, natDegree_X_pow_add_C]
  done

-- Polynomial.leadingCoeff_X_sub_C.{v}
example {S : Type v} [Ring S] (r : S) :
    Polynomial.leadingCoeff (Polynomial.X - Polynomial.C r) = 1 := by
  rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_add_C]
  done

[Damiano Testa]

... and on Mathlib.Data.Nat.Basic

import Mathlib.Data.Nat.Basic

open
  Nat

-- Nat.lt_iff_add_one_le
example {m n : ℕ} : m < n ↔ m + 1 ≤ n := by
  rw [succ_le_iff]
  done

-- Nat.add_succ_sub_one
example (n m : ℕ) : n + Nat.succ m - 1 = n + m := by
  rw [add_succ, succ_sub_one]
  done

-- Nat.succ_add_sub_one
example (n m : ℕ) : Nat.succ n + m - 1 = n + m := by
  rw [succ_add, succ_sub_one]
  done

-- Nat.pred_sub
example (n m : ℕ) : Nat.pred n - m = Nat.pred (n - m) := by
  rw [← Nat.sub_one, Nat.sub_sub, one_add, sub_succ]
  done

-- Nat.pred_one_add
example (n : ℕ) : Nat.pred (1 + n) = n := by
  rw [add_comm, add_one, Nat.pred_succ]
  done

-- Nat.mul_left_eq_self_iff
example {a b : ℕ} (hb : 0 < b) : a * b = b ↔ a = 1 := by
  rw [mul_comm, Nat.mul_right_eq_self_iff hb]
  done

-- Nat.one_le_div_iff
example {a b : ℕ} (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a := by
  rw [le_div_iff_mul_le hb, one_mul]
  done

-- Nat.eq_of_dvd_of_div_eq_one
example {a b : ℕ} (w : a ∣ b) (h : b / a = 1) : a = b := by
  rw [← Nat.div_mul_cancel w, h, one_mul]
  done

-- Nat.eq_zero_of_dvd_of_div_eq_zero
example {a b : ℕ} (w : a ∣ b) (h : b / a = 0) : b = 0 := by
  rw [← Nat.div_mul_cancel w, h, zero_mul]
  done

-- Nat.mul_add_mod_of_lt
example {a b c : ℕ} (h : c < b) : (a * b + c) % b = c := by
  rw [Nat.mul_add_mod, Nat.mod_eq_of_lt h]
  done

[Damiano Testa]

Hopefully this is useful to have more tests for rewrite_search.

[Damiano Testa]

(and if you want me to run the code on a glob of files, I can give it a try! The main issues for this to work are (among others)

• ambiguous lemmas, due to the large open command,
• losing type ascriptions in lemma statements, resulting in non-typechecking statements or typeclass search being stuck.)

[Scott Morrison]

On Mathlib.Data.Polynomial.Degree.Definitions, rw_search works out of the box on 11/18 of the examples (I discarded those whose types are not equalities. There's no reason rw_search shouldn't work on iff, it just doesn't right now.

[Scott Morrison]

Unfortunately I don't really have time for more tweaking of rw_search right now, although it is very useful to have these additional examples.

[Scott Morrison]

Ideally I will find time to run it properly on all of Mathlib! The lean-training-data repo has a mechanism to run a tactic against every declaration in Mathlib. I'd like to add:

• filtering (so we can run only against "pure rewrite" theorems)
• running against every subgoal, not just top level goals

[Damiano Testa]

Well, 11/18 seems like a very good result!

If you decide to go back to trying stuff out and you do not want to do it properly with lean-training-data, let me know and I can generate more tests!

As for lean-training-data, I have not forgotten that you had already mentioned it to me, I definitely want to look at it carefully, but I doubt that I will have the time before the term ends, in a couple of months.

[Scott Morrison]

:ping_pong: any further interest in this? I am sad to see this PR with an interesting new tactic rotting. :-(

[Jireh Loreaux]

@Scott Morrison I'll take a look at this tomorrow. I'm still not fully qualified to review meta code, but I'd prefer to have it than not.

[Scott Morrison]

Thank you everyone for the feedback and review! Rob gave the delegation, and it's now landed in master for everyone to try out.

[Scott Morrison]

I'm happy to hear about working and non-working examples.

[Scott Morrison]

(And feel free to commit the output of rw_search says, as far as I'm concerned. :-)

[David Renshaw]

I don't necessarily expect the tactic to succeed here, but this error message definitely looks wrong:

import Mathlib.Data.Nat.Digits
import Mathlib.Tactic

lemma prepend_one_eq_append (n : ℕ) :
    Nat.digits 10 (10 ^ (List.length (Nat.digits 10 n)) + n) = (Nat.digits 10 n) ++ [1] := by
  induction' n using Nat.strong_induction_on with n' ih
  rw_search
  -- unknown free variable '_uniq.249'

[David Renshaw]

Ah, this seems to be fixed by

diff --git a/Mathlib/Tactic/RewriteSearch.lean b/Mathlib/Tactic/RewriteSearch.lean
index 6149acbd3..ba11a4357 100644
--- a/Mathlib/Tactic/RewriteSearch.lean
+++ b/Mathlib/Tactic/RewriteSearch.lean
@@ -292,7 +292,7 @@ to prevent `rw_search` from using the names theorems.
 syntax "rw_search" (forbidden)? : tactic

 elab_rules : tactic |
-    `(tactic| rw_search%$tk $[[ $[-$forbidden],* ]]?) => do
+    `(tactic| rw_search%$tk $[[ $[-$forbidden],* ]]?) => withMainContext do
   let forbidden : NameSet :=

[Patrick Massot]

Do we have a #patronsaints linkifier already?

[David Renshaw]

I submitted a fix: mathlib4#8101

[David Renshaw]

I was surprised that rw_search seems to not look in the local context for possible rewrites.

[David Renshaw]

(that makes my added test case a bit more involved)

[Scott Morrison]

Interesting, I thought it should. rw? uses the local hypotheses now, doesn't it??

[David Renshaw]

apparently not in this case

def makeSingleton : Nat → List Nat
  | 0 => [0]
  | b + 1 => makeSingleton b

example (n : Nat) : makeSingleton n = [0] := by
  induction' n with n' ih
  · simp
  · -- At one point, this failed with: unknown free variable '_uniq.62770'
    unfold makeSingleton
    rw? -- should find ih, but does not

[Schrodinger ZHU Yifan]

I see an integer log function is used for penalty. Could you elaborate more details?

[Scott Morrison]

@Schrodinger ZHU Yifan, have you read the doc-string on docs#Mathlib.Tactic.RewriteSearch.SearchNode.penalty ?

[Schrodinger ZHU Yifan]

Not really. Let me check it out.

[David Renshaw]

Scott Morrison said:

Interesting, I thought it should. rw? uses the local hypotheses now, doesn't it??

ah, there's a bug in localHypotheses. It needs to call whnfR.

diff --git a/Mathlib/Tactic/Rewrites.lean b/Mathlib/Tactic/Rewrites.lean
index 07ef42d1a..459f1a6ba 100644
--- a/Mathlib/Tactic/Rewrites.lean
+++ b/Mathlib/Tactic/Rewrites.lean
@@ -85,6 +85,7 @@ def localHypotheses (except : List FVarId := []) : MetaM (Array (Expr × Bool ×
   for h in r do
     if except.contains h.fvarId! then continue
     let (_, _, type) ← forallMetaTelescopeReducing (← inferType h)
+    let type ← whnfR type
     match type.getAppFnArgs with

[David Renshaw]

Though maybe using a ~q() match there would be more idiomatic?

[Scott Morrison]

Thanks for this! I'd prefer not to use quote4 here so it's easier to upstream this tactic later if desired.

[Scott Morrison]

If you want to turn that patch into a PR I can insta-merge!

[David Renshaw]

I tacked it onto mathlib4#8101

[David Renshaw]

hah, that makes 2 out of the 3 patron saints https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20error.20in.20structured.20proof/near/322950305

[David Renshaw]

rw_search saved me time just now, on something like this, where I was teeing up my goal to be handleable by gcongr:

import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.Positive.Field
import Mathlib.Tactic

example (a b : {x : ℝ | 0 < x}) : a * ((1:ℝ) / b) + b * (1/a) = a / b + b / a := by rw_search
-- Try this: rw [@mul_one_div, @add_left_cancel_iff, @mul_one_div]

:tada:

[Scott Morrison]

I hope we can get even more ambitious with rw_search in future.

I remember our prototype back in... 2019(!) once successfully finding a chain of 17 rewrites.

The actual rewrites are not the difficulty: when the problem has too much branching we get lost in the tree search.

Better premise selection, and better search heuristics, would both help.

[Eric Rodriguez]

I think rw_search has a reducibility issue:

import Mathlib.Tactic.RewriteSearch

example : 1 = id 1 := by
  rw_search says rw []
  rw [id]

Should I flag a tracker issue?

[Alex J. Best]

The issue is that rw_search uses a stronger rfl than rw I think. So oftentimes rw_search returns a rw [blah, blah] that should be rw [blah, blah]; rfl

[Alex J. Best]

I think we need an issue for this (not sure what the right fix is, it would be a shame to make rw_search weaker so probably adding the rfl to the suggestion when needed is best, unless it turns out rw_search is way faster with a weaker rfl of course (rw_search! anyone?))