tryAtEachStep: run a tactic on every step in your proofs

Stream: lean4

[David Renshaw]

tryAtEachStep is a little tool I made that runs a tactic (for example exact? or rw_search) on every proof step in a given Lean file.
I have found it to be surprisingly effective at finding ways to improve code. See the README for a list of some optimizations it has already found in the past two days.
For a laugh, try running it on Mathlib.Data.List.Basic -- it'll tell you about a lot of cruft!

[David Renshaw]

(Please use careful judgement when opening pull requests based on the output of this tool. Not every success of exact? necessarily represents an improvement. For example, it often suggests exact rfl in situations where that would commonly be considered to be defeq abuse.)

[Yaël Dillies]

Witchcraft! :mage:

[David Renshaw]

tryEachStep might also be considered interesting as an up-to-date example of how to abuse infotrees.

[David Renshaw]

previous examples being https://github.com/semorrison/lean-training-data/blob/master/TrainingData/InfoTree/Basic.lean and https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean

[Kim Morrison]

Nice!

[Kim Morrison]

I want to see what it does with omega.

[David Renshaw]

tryAtEachStep omega on the first file I looked at: https://github.com/dwrensha/compfiles/commit/98bad7c9c20e6369cdaa15a5e790fcc92e664659

[David Renshaw]

The old linarith needs the extra massaging before it works, and it's slower than omega.

[David Renshaw]

another nice one: https://github.com/dwrensha/compfiles/commit/48ecf3f73e85b4b5a45172de14db8c5ed8947e22

[Kim Morrison]

Here's a feature request: compare the timings of the original proof and the replacement tactic, and allow reporting only faster replacements!

[David Renshaw]

size of the generated proof term could be interesting too

[Kim Morrison]

I guess for timings you would want to time both the elaboration and sending the declaration to the kernel. Maybe too complicated. :-(

[David Renshaw]

@Scott Morrison you asked for it: mathlib4#11093

[Kevin Buzzard]

@David Renshaw you should !bench to see what the speedcenter thinks.

[Josha Dekker]

Very nice! A possible suggestion for a feature would be an optional functionality to see if you can reduce an assumption, both with the old proof and the new attempt. This has been discussed previously and was apparently present in some form Lean3. I think this might be a nice place to incorporate such a feature!

[David Renshaw]

What do you mean by "reduce an assumption"?

[Kevin Buzzard]

benchmark results are in and looking good :-)

[Patrick Massot]

@Joël Riou this is one is a gift for you:

+ ~Mathlib.AlgebraicTopology.DoldKan.Faces                     instructions   -46.9%

[Kevin Buzzard]

ha ha I just DMed him saying the same thing. It's not just that file, there is a ton of stuff he wrote before omega which can now be speeded up.

[Josha Dekker]

David Renshaw said:

What do you mean by "reduce an assumption"?

suppose we have a hypothesis [Property A], but Property extends BaseProperty. By reducing an assumption I meant seeing if the initial hypothesis can be replaced by the weaker assumption [BaseProperty A]? I see how my phrasing was unclear, it was late here :sleeping: …

[Kim Morrison]

Oof, unfortunately merging mathlib4#11093 was a bit premature: in v4.7.0-rc1 we are weakening omega slightly, because we decided that doing identification of atoms up to defeq was too expensive.

[Kim Morrison]

This means for example that it will no longer solve id x <= x.

[Kim Morrison]

So of the the omega calls introduced in mathlib4#11093 now need to be reverted on nightly-testing.

[Kim Morrison]

@David Renshaw, possibilities:

[Kim Morrison]

• just revert the PR, and redo it after we move to v4.7.0-rc1
• we go through nightly-testing reverting proofs that now break

[Mario Carneiro]

• We make omega! work

[Kim Morrison]

Yes, sure, but I'm not doing that before v4.7.0-rc1.

[Kim Morrison]

I'm just going the revert the uses of omega in NormNum/Basic, in the hope that they are the only "weird" ones.

[Mario Carneiro]

(we need a better way to compile which allows building to continue after a failed proof)

[David Renshaw]

I'm just going the revert the uses of omega in NormNum/Basic, in the hope that they are the only "weird" ones.

Looks like Mathlib/AlgebraicTopology/DoldKan/Faces.lean:210 is at least one other instance that no longer works.

[David Renshaw]

I suppose I should push fixes to the nightly-testing branch?

[David Renshaw]

I got it working locally, with the following changes:

diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean b/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
index c5056f751e..73cdfbcd25 100644
--- a/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
+++ b/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
@@ -115,7 +115,7 @@ noncomputable def mappingConeHomOfDegreewiseSplitIso :
     dsimp at r_f s_g
     set_option tactic.skipAssignedInstances false in
     simp [mappingConeHomOfDegreewiseSplitXIso, mappingCone.ext_from_iff _ _ _ rfl,
-      mappingCone.inl_v_d_assoc _ (p + 1) _ (p + 1 + 1) (by omega) (by omega),
+      mappingCone.inl_v_d_assoc _ (p + 1) _ (p + 1 + 1) (by linarith) (by omega),
       cocycleOfDegreewiseSplit, r_f]
     rw [← S.g.comm_assoc, reassoc_of% s_g]
     abel)
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Faces.lean b/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
index b98ec9e8b6..cf8483e0f1 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
@@ -193,6 +193,7 @@ theorem induction {Y : C} {n q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFacesVa
     rfl
   -- now, we assume j ≠ a (i.e. a < j)
   have haj : a < j := (Ne.le_iff_lt hj₂).mp (by omega)
+  have hj₃ := j.is_lt
   have ham : a ≤ m := by
     by_contra h
     rw [not_le, ← Nat.succ_le_iff] at h
@@ -207,14 +208,14 @@ theorem induction {Y : C} {n q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFacesVa
     swap
     · rw [Fin.le_iff_val_le_val]
       dsimp
-      omega
+      linarith
     simp only [← assoc, v j (by omega), zero_comp]
   · -- in the last case, a=m, q=1 and j=a+1
     rw [X.δ_comp_δ_self'_assoc]
     swap
     · ext
       dsimp
-      omega
+      linarith
     simp only [← assoc, v j (by omega), zero_comp]
 #align algebraic_topology.dold_kan.higher_faces_vanish.induction AlgebraicTopology.DoldKan.HigherFacesVanish.induction

diff --git a/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean b/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
index beb5d09cfb..42183d673f 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
@@ -75,7 +75,7 @@ theorem PInfty_comp_map_mono_eq_zero (X : SimplicialObject C) {n : ℕ} {Δ' : S
     · simp only [op_comp, X.map_comp, assoc, PInfty_f]
       erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ hj₁, zero_comp]
       by_contra
-      exact hj₁ (by simp only [Fin.ext_iff, Fin.val_zero]; omega)
+      exact hj₁ (by simp only [Fin.ext_iff, Fin.val_zero]; linarith)
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.P_infty_comp_map_mono_eq_zero AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero

diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
index 06a5858509..20a33366fa 100644
--- a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
+++ b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean
@@ -227,7 +227,7 @@ def rightAngleRotationAux₂ : E →ₗᵢ[ℝ] E :=
           have : Finset.card {x} = 1 := Finset.card_singleton x
           have : finrank ℝ K + finrank ℝ Kᗮ = finrank ℝ E := K.finrank_add_finrank_orthogonal
           have : finrank ℝ E = 2 := Fact.out
-          omega
+          linarith
         obtain ⟨w, hw₀⟩ : ∃ w : Kᗮ, w ≠ 0 := exists_ne 0
         have hw' : ⟪x, (w : E)⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
         have hw : (w : E) ≠ 0 := fun h => hw₀ (Submodule.coe_eq_zero.mp h)
diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean
index 9c59ed152a..97db8be398 100644
--- a/Mathlib/NumberTheory/Modular.lean
+++ b/Mathlib/NumberTheory/Modular.lean
@@ -346,7 +346,7 @@ variable {z}
 theorem exists_eq_T_zpow_of_c_eq_zero (hc : (↑ₘg) 1 0 = 0) :
     ∃ n : ℤ, ∀ z : ℍ, g • z = T ^ n • z := by
   have had := g.det_coe
-  replace had : (↑ₘg) 0 0 * (↑ₘg) 1 1 = 1 := by rw [det_fin_two, hc] at had; omega
+  replace had : (↑ₘg) 0 0 * (↑ₘg) 1 1 = 1 := by rw [det_fin_two, hc] at had; linarith
   rcases Int.eq_one_or_neg_one_of_mul_eq_one' had with (⟨ha, hd⟩ | ⟨ha, hd⟩)
   · use (↑ₘg) 0 1
     suffices g = T ^ (↑ₘg) 0 1 by intro z; conv_lhs => rw [this]
@@ -361,7 +361,7 @@ theorem exists_eq_T_zpow_of_c_eq_zero (hc : (↑ₘg) 1 0 = 0) :
 -- If `c = 1`, then `g` factorises into a product terms involving only `T` and `S`.
 theorem g_eq_of_c_eq_one (hc : (↑ₘg) 1 0 = 1) : g = T ^ (↑ₘg) 0 0 * S * T ^ (↑ₘg) 1 1 := by
   have hg := g.det_coe.symm
-  replace hg : (↑ₘg) 0 1 = (↑ₘg) 0 0 * (↑ₘg) 1 1 - 1 := by rw [det_fin_two, hc] at hg; omega
+  replace hg : (↑ₘg) 0 1 = (↑ₘg) 0 0 * (↑ₘg) 1 1 - 1 := by rw [det_fin_two, hc] at hg; linarith
   refine' Subtype.ext _
   conv_lhs => rw [Matrix.eta_fin_two (↑ₘg)]
   rw [hc, hg]
diff --git a/Mathlib/SetTheory/Surreal/Dyadic.lean b/Mathlib/SetTheory/Surreal/Dyadic.lean
index b4a3cd5e30..d12740d9b8 100644
--- a/Mathlib/SetTheory/Surreal/Dyadic.lean
+++ b/Mathlib/SetTheory/Surreal/Dyadic.lean
@@ -239,7 +239,7 @@ def dyadicMap : Localization.Away (2 : ℤ) →+ Surreal where
         apply dyadic_aux
         rwa [ha₁, ha₂, mul_comm, mul_comm m₂]
       · have : (1 : ℤ) ≤ 2 ^ y₃ := mod_cast Nat.one_le_pow y₃ 2 Nat.succ_pos'
-        omega
+        linarith
   map_zero' := Localization.liftOn_zero _ _
   map_add' x y :=
     Localization.induction_on₂ x y <| by

[David Renshaw]

I pushed these to nightly-testing. In the meantime, a new nightly got released and new (probably unrelated) breakage appeared elsewhere.

[David Renshaw]

I ran tryAtEachStep omega on all of mathlib again, this time using its new convenient tryAtEachStepInDirectory wrapper. It found 61 instances where linarith or nlinarith can be replaced by omega: mathlib4#19951

[Kim Morrison]

Here's a somewhat radical suggestion for tryAtEachStep. Could we investigate where it is possible to remove a lemma from either a simp or simp only without breaking the proof. I know this occurs fairly frequently in the wild, and arguably it is usually slightly more readable to remove or postpone unnecessary lemmas.

[Mario Carneiro]

this could be a linter

[Kim Morrison]

Another potential idea would be to find placeholder _ that could be replaced with a single character term (thereby strictly improving readability?) or could be replaced with a short term in exchange for a measurable improvement in heartbeats? (Some human consideration of whether that hurt or helped readability might be useful.)

[Mario Carneiro]

it can probably be answered faster by consulting the simp trace rather than running all subsets a la squeeze_simp

[Kim Morrison]

I was actually thinking about the case where we can remove a lemma from a simp only, which is actually being used, but it doesn't break the proof (often because a terminal simp would do it anyway). But I think this can't be checked except by brute forcing, so would be a job for this tool rather than a linter.

[Kim Morrison]

I think this often is a readability improvement, because it shrinks the simp only, and the terminal simp stays the same.

[Jireh Loreaux]

Kim Morrison said:

Another potential idea would be to find placeholder _ that could be replaced with a single character term (thereby strictly improving readability?)

I think I prefer _ actually. It tells me that Lean knows how to fill this in, so probably I do too. So I wouldn't consider filling them in a strict readability improvement. This is especially true where some variable was introduced, but it really didn't need to be, and now this linter would fill in an unnecessary variable.

Another reason to prefer _: when I refactored a bunch of Subobject.closure_induction lemmas, I ended up reordering some of their arguments. I then had to fix a bunch of downstream uses of those variables, but in many cases I wouldn't have had to do so if there had just been _ in their place.

[Kim Morrison]

Here's an example of my simp only request. I just wrote a proof that initially said

  simp [lex]
  cases lt a b <;> cases a != b <;> simp [Id.run]

and simp? expands this to

  simp only [lex, List.getElem_toArray, List.getElem_singleton, Id.pure_eq, Id.bind_eq,
    size_toArray, List.length_singleton, Nat.min_self, forIn'_eq_forIn,
    Std.Range.forIn_eq_forIn_range', Std.Range.size, Nat.sub_zero, Nat.reduceAdd,
    Nat.add_one_sub_one, Nat.div_one, List.range'_one, List.forIn_cons, List.forIn_nil,
    Nat.lt_irrefl, decide_false]
  cases lt a b <;> cases a != b <;> simp [Id.run]

but actually what I want is

  simp only [lex, List.getElem_toArray, List.getElem_singleton]
  cases lt a b <;> cases a != b <;> simp [Id.run]

[Yury G. Kudryashov]

Thanks a lot! I've run it with omega on Mathlib as an experiment, going through the output.
I have a few feature requests:

• When running on a directory, sort entries in RESULTS.json in the import graph order (forward or reverse), so that one can go through the file without waiting for rebuilds caused by earlier fixes.
• If the tactic closes the goal, then don't try it again after the next step. Currently, if I have a multiline proof that can be closed by omega at any moment, then I get many entries in the output.

[Kim Morrison]

@David Renshaw, could I request a feature? I would like to only run at steps where the existing tactic matches some pattern (or perhaps even matches a constant string).

[Kim Morrison]

I would like to, for example, find all places in the library where there is a terminal aesop that could just be simp or simp_all.

[Kim Morrison]

(I am trying to generate interesting test cases for the new grind tactic by looking at places where we use aesop in Mathlib currently, but it is just swamped by situations where we don't really need to be using aesop in the first place.)

[David Renshaw]

To accomplish that with the current version of tryAtEachStep, I would do:

lake exe tryAtEachStepInDirectory "simp_all" .lake/packages/mathlib/Mathlib --filter-by-fewer-steps false

and then filter on the originalText field in the output json file tryAtEachStep-out/RESULTS.json.

[David Renshaw]

... which still runs simp_all on all steps, but at least you should be able to achieve your goal (eventually).

[David Renshaw]

Doing the filtering before trying simp_all, as you suggest, would save a lot of computation.

[David Renshaw]

Opening such a request as an issue on https://github.com/dwrensha/tryAtEachStep/issues would probably be the best way to make sure that I remember it.

[Kim Morrison]

https://github.com/dwrensha/tryAtEachStep/issues/1

[Kim Morrison]

@David Renshaw, I see that you closed my issue https://github.com/dwrensha/tryAtEachStep/issues/4, but I think this was based on a misunderstanding of the intent. I did not mean to record the number of "proof steps", but the instruction count, so that we can decide whether a given change would be an improvement to build time.

Heartbeats is much more accessible that instruction count, of course, and that would be a fine proxy.

[Kim Morrison]

Could we reopen the issue (or I'll make a new one)?

[David Renshaw]

sorry for the confusion!

[David Renshaw]

I think opening a new issue would be best.

[David Renshaw]

... perhaps with a link to the old one.

[Kim Morrison]

https://github.com/dwrensha/tryAtEachStep/issues/12