Infrastructure for tracking frequently applied simp theorems

Stream: mathlib4

[Matthew Ballard]

Currently, we don't have any observable or quantifiable way to figure out which simp theorems frequently apply and frequently fail.

What mechanisms/metrics can we use to remedy this? Some possibilities:

1. Catalog the number of attempts and failures of a simp theorem across all of mathlib in some way
2. Similar to 2 but make it part of the simpNF linter and only look at these numbers when applying it to other simp theorems
3. Have some heuristic for the strength of the discrimination tree keys of a simp theorem to use a a filter.

Thoughts and feedback on this would be super useful before we engineer anything.

[Jireh Loreaux]

Personally, I think some form of (3) is necessary, unless we really manage (1), but I suspect the latter will be computationally intensive, and it would be nice to have immediate feedback when tagging something @[simp]. I fear (2) will not be sufficient to track that bad lemmas (especially because if we only retain lemmas whose head expressions don't match too much, then the bad lemmas won't match the heads of the good lemmas either :sad:).

[Patrick Massot]

Even if 1 is computationally intensive we could have statistics running once a day.

[Damiano Testa]

There is an option that make simp trace which lemmas it tried and did not use, right?

So a cheap way of achieving 1 could be to set that option on, build mathlib and tally the report, right?

[Matthew Ballard]

For 1, do we want an option to store a record with each declaration on build and then query afterward to generate the raw data?

For 3, I don't really know of a good heuristic to use to draw a line here. Of course, a lot of *'s is bad. But what is reasonable rule for a general set of keys?

[Patrick Massot]

Yes, storing the statistics in raw form would be best, especially in the beginning, unless the amount of data is really huge.

[Matthew Ballard]

Comments requested on the following linter. I just randomly choose <= 2 non-stars/others.

open private preprocess from Lean.Meta.Tactic.Simp.SimpTheorems in
/--
A linter for simp theorems whose keys are weak, i.e. they contain few non stars and other symbols.
-/
@[env_linter] def simpWeakKeys : Linter where
  noErrorsFound := "No simp lemmas have weak keys."
  errorsFound := "Some simp lemmas have weak keys."
  test := fun declName => do
    unless ← isSimpTheorem declName do return none
    let info ← getConstInfo declName
    unless info.hasValue do return none
    let l ← preprocess info.value! info.type false true
    let arr ← l.toArray.mapM fun (_, type) => withReducible do
      let (_, _, type) ← forallMetaTelescopeReducing type
      let type ← whnfR type
      let keys ←
        match type.eq? with
        | some (_, lhs, _) => pure (← DiscrTree.mkPath lhs simpDtConfig false)
        | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}"
      let isWeakKey := keys.filter (fun key => key != .star || key != .other)
      if isWeakKey.size ≤ 2 then
        return keys
      else
        return #[]
    if arr.flatten.isEmpty then
      return none
    else
      let msgs ← arr.mapM (fun keys => DiscrTree.keysAsPattern keys)
      return m!"{declName} has weak keys: {msgs}"

[Yury G. Kudryashov]

Did you run it on Mathlib?

[Matthew Ballard]

Getting in position now. But withReducible needs to go first and this catches some reasonable things like docs#Rat.zero_num

[Damiano Testa]

It looks like all the checks that the linter does are "local", right? If you write it as a syntax linter, it might be easier to debug.

[Matthew Ballard]

Yeah, I guess that is true

[Matthew Ballard]

It would be really nice if there were some getDeclName method on Syntax so I don't have to match over all the myriad of constructions to get the name of a declaration.

[Damiano Testa]

You can do stx.find? ``declId and, unless the declaration is a nameless instance (or a couple of extra edge cases), you should find the name (to resolve).

[Damiano Testa]

Also, is d : TSyntax ``declId, then d[0] is an `ident. Or maybe d.raw[0].

[Matthew Ballard]

Thanks! My knowledge of the various syntax categories is pretty thin. I had just found these in DeprecateMe and MinImports. Glad people put them there :)

[Damiano Testa]

I use a command to look at syntax that produces a tree output with all the parser names and whatever other information is encoded in the syntax. I find it more useful than dbg_trace stx to read. I am thinking of how to PR it, since it is not very polished now.

[Damiano Testa]

In case it is useful in this form, here it is, with an example use at the end:

import Mathlib.Lean.Expr.Basic

open Lean Elab Tactic

/-- replaces line breaks with the literal string `⟨['\', 'n']⟩`
for better formatting of syntax that includes line breaks.
-/
def rmLB (s : String) : String :=
  "⏎".intercalate (s.splitOn "\n")

#eval show MetaM _ from
  guard ("hi⏎⏎" == rmLB "hi\n
")

def si : (info : SourceInfo) → MessageData
  | .original leading _pos trailing _endPos =>
    m!"original: ⟨{leading}⟩" ++ m!"⟨{rmLB trailing.toString}⟩"
  | .synthetic _pos _endPos canonical => m!"synthetic: {canonical}"
  | .none => "none"

/--  `treeM ex` takes a `Syntax` and returns a pair consisting of
*  `MessageData` for the non-`Syntax` arguments of `stx`,
*  an array of the `Syntax` arguments to `stx`.
-/
def treeM : Syntax → MessageData × Array Syntax
  | .missing => default
  | stx@(.node   info _kind args) => ("node " ++ stx.getKind ++ ", " ++ si info, args)
  | .atom   info val => ("atom " ++ si info ++ "-- '" ++ val ++ "'", default)
  | .ident  info rawVal val _preresolved =>
    ("ident " ++ si info ++ "-- (" ++ val ++ "," ++ rawVal.toString ++ ")", default)

/--  `treeR stx` recursively formats the output of `treeM`. -/
partial
def treeR (stx : Syntax) (indent : MessageData := "\n") (sep : MessageData := "  ") :
    MessageData :=
  let (msg, es) := treeM stx
  let mes := es.map (treeR (indent := indent ++ sep) (sep := sep))
  mes.foldl (fun x y => (x.compose indent).compose ((m!"|-").compose y)) msg

/-- `inspect ex` calls `logInfo` on the output of `treeR stx`.
-/
def Meta.inspect {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
    (stx : Syntax) : m Unit :=
  logInfo (m!"inspect: '{stx}'\n\n".compose (treeR stx (sep := "|   ")))

/--  `inspect cmd` displays the tree structure of the `Syntax` in the command `cmd`.
 -/
syntax (name := inspectStx) "inspect " command : command

elab_rules : command
  | `(command| inspect $cmd) => do
    logInfo (m!"inspect: '{cmd}'\n\n".compose (treeR cmd (sep := "|   ")))
    Command.elabCommand cmd


/-
inspect: 'theorem hello : True := by
  refine ?_
  exact .intro'

node Lean.Parser.Command.declaration, none
|-node Lean.Parser.Command.declModifiers, none
|   |-node null, none
|   |-node null, none
|   |-node null, none
|   |-node null, none
|   |-node null, none
|   |-node null, none
|-node Lean.Parser.Command.theorem, none
|   |-atom original: ⟨⟩⟨ ⟩-- 'theorem'
|   |-node Lean.Parser.Command.declId, none
|   |   |-ident original: ⟨⟩⟨ ⟩-- (hello,hello)
|   |   |-node null, none
|   |-node Lean.Parser.Command.declSig, none
|   |   |-node null, none
|   |   |-node Lean.Parser.Term.typeSpec, none
|   |   |   |-atom original: ⟨⟩⟨ ⟩-- ':'
|   |   |   |-ident original: ⟨⟩⟨ ⟩-- (True,True)
|   |-node Lean.Parser.Command.declValSimple, none
|   |   |-atom original: ⟨⟩⟨ ⟩-- ':='
|   |   |-node Lean.Parser.Term.byTactic, none
|   |   |   |-atom original: ⟨⟩⟨⏎  ⟩-- 'by'
|   |   |   |-node Lean.Parser.Tactic.tacticSeq, none
|   |   |   |   |-node Lean.Parser.Tactic.tacticSeq1Indented, none
|   |   |   |   |   |-node null, none
|   |   |   |   |   |   |-node Lean.Parser.Tactic.refine, none
|   |   |   |   |   |   |   |-atom original: ⟨⟩⟨ ⟩-- 'refine'
|   |   |   |   |   |   |   |-node Lean.Parser.Term.syntheticHole, none
|   |   |   |   |   |   |   |   |-atom original: ⟨⟩⟨⟩-- '?'
|   |   |   |   |   |   |   |   |-node Lean.Parser.Term.hole, none
|   |   |   |   |   |   |   |   |   |-atom original: ⟨⟩⟨⏎  ⟩-- '_'
|   |   |   |   |   |   |-node null, none
|   |   |   |   |   |   |-node Lean.Parser.Tactic.exact, none
|   |   |   |   |   |   |   |-atom original: ⟨⟩⟨ ⟩-- 'exact'
|   |   |   |   |   |   |   |-node Lean.Parser.Term.dotIdent, none
|   |   |   |   |   |   |   |   |-atom original: ⟨⟩⟨⟩-- '.'
|   |   |   |   |   |   |   |   |-ident original: ⟨⟩⟨⟩-- (intro,intro)
|   |   |-node Lean.Parser.Termination.suffix, none
|   |   |   |-node null, none
|   |   |   |-node null, none
|   |   |-node null, none
-/
inspect
theorem hello : True := by
  refine ?_
  exact .intro

[Damiano Testa]

Most of the time, just knowing the SyntaxNodeKind is enough. Sometimes, knowing how many arguments what you are matching on has is also important. inspect usually prints everything that can be printed, just in case.

[Matthew Ballard]

https://gist.github.com/mattrobball/45df3dae500af5a13f3aaaee7bda251b

[Yury G. Kudryashov]

Many theorems at the top look like false positives to me.

[Matthew Ballard]

Oh yeah, that is way too many but gives you some sense of what such keys look like.

I am going to see what pops out of an instance version next. I suspect that will still have some noise but will be better tuned since we immediately turning on (possibly) expensive operations.

[Matthew Ballard]

This is unfortunate

././././Mathlib/GroupTheory/QuotientGroup.lean:144:3: error: @QuotientAddGroup.mk_add Declaration has weak keys: [@QuotientAddGroup.mk _ _ _ (@HAdd.hAdd _ _ _ _ _ _)]
././././Mathlib/GroupTheory/QuotientGroup.lean:145:1: error: @QuotientGroup.mk_mul Declaration has weak keys: [@Quotient.mk'' _ _ (@HMul.hMul _ _ _ _ _ _)]

[Matthew Ballard]

Comments on this filter?

      let common :=
        #[`HAdd.hAdd, `HMul.hMul, `HSMul.hSMul, `HSub.hSub, `HDiv.hDiv,
          `Neg.neg, `Inv.inv, `Zero.zero, `One.one, `Top.top, `Bot.bot,
          `Quotient.mk, `Quotient.mk', `Quotient.mk'', `Eq, `Membership.mem, `DFunLike.coe]
      let goodKeyWeight : Key → Nat
        | .star => 0
        | .other => 0
        | .const n _ => if common.contains n then 0 else 2
        | _ => 1
      if keys.foldl (init := 0) (fun w k => w + goodKeyWeight k) ≤ 1 then
        return keys
      else
        return #[]

[Damiano Testa]

I do not have an opinion on the filter itself, but it could be that using a NameSet for common is slightly faster.

[Matthew Ballard]

The only thing that has decent signal are keys of the form DFunLike.coe _ _ _ _ _ _ etc with the name coming from the common set above.

[Matthew Ballard]

I'll try to write an environmental extension to capture the statistics on simps/instances attempts and simps failures. There might be a simple way to get the instance application failures but I don't see it at the moment.

[Matthew Ballard]

Here are the usages attempts across batteries (and maybe core?) that exceed 500

(eq_self, 4779),
 (Array.data_length, 1540),
 (and_imp, 997),
 (implies_true, 993),
 (imp_self, 980),
 (imp_false, 974),
 (imp_not_self, 974),
 (forall_exists_index, 936),
 (false_implies, 936),
 (forall_false, 924),
 (forall_eq_or_imp, 909),
 (forall_eq, 901),
 (true_implies, 890),
 (forall_const, 890),
 (forall_apply_eq_imp_iff₂, 884),
 (forall_eq', 882),
 (forall_eq_apply_imp_iff, 872),
 (Decidable.not_imp_self, 872),
 (Bool.eq_true_imp_eq_false, 872),
 (List.forall_mem_ne, 872),
 (Bool.eq_false_imp_eq_true, 872),
 (forall_apply_eq_imp_iff, 872),
 (Subtype.forall, 870),
 (List.forall_mem_ne', 870),
 (and_self, 805),
 (if_pos, 651),
 (if_neg, 525)

Does this output seem sane?

[Matthew Ballard]

And here are the successful rewrites over 25

simpsSuccess: [(eq_self, 784),
 (Array.data_length, 260),
 (List.append_assoc, 167),
 (iff_self, 147),
 (if_pos, 126),
 (if_neg, 119),
 (ne_eq, 117),
 (and_self, 94),
 (Batteries.RBNode.All, 91),
 (Nat.add_assoc, 89),
 (List.cons_append, 83),
 (reduceIte, 78),
 (Batteries.RBNode.toList_node, 71),
 (Nat.add_left_comm, 65),
 (List.nil_append, 63),
 (not_false_eq_true, 63),
 (Bool.not_eq_true, 62),
 (Array.get_eq_getElem, 60),
 (List.singleton_append, 60),
 (Nat.zero_add, 55),
 (String.utf8Len_nil, 54),
 (List.mem_cons, 54),
 (List.append_nil, 54),
 (String.utf8Len_append, 51),
 (Batteries.RBNode.reverse, 50),
 (Nat.add_zero, 50),
 (String.utf8Len_cons, 49),
 (Batteries.AssocList.toList, 48),
 (dif_pos, 46),
 (Bool.false_eq_true, 46),
 (dif_neg, 46),
 (List.length_cons, 44),
 (implies_true, 41),
 (Rat.divInt_ofNat, 40),
 (Nat.succ_eq_add_one, 35),
 (imp_false, 33),
 (Array.toList_eq, 32),
 (List.map_cons, 32),
 (and_assoc, 30),
 (Option.mem_def, 30),
 (reduceDIte, 29),
 (and_left_comm, 29),
 (decide_eq_true_eq, 28),
 (Nat.le_refl, 27),
 (Batteries.PairingHeapImp.Heap.size, 27),
 (Batteries.BinomialHeap.Imp.Heap.realSize, 26),
 (List.get?_eq_getElem?, 26),
 (forall_and, 25),
 (String.utf8Len_reverse, 25)

[Matthew Ballard]

Here's a fun one so far: docs#List.forall_mem_ne was tried 872 times and successful 2

[Matthew Ballard]

docs#Decideable.not_imp_self also tried 872 times but successful 0

[Matthew Ballard]

docs#Subtype.forall 0/870

[Matthew Ballard]

All three have keys just <arrow>

[Matthew Ballard]

From the top 100 simp theorems by attempt in mathlib, here are those with a success rate of < 0.05

simpsAttempts: [Set.coe_setOf : 0.002680 : 51858,
 SetLike.coe_sort_coe : 0.006100 : 48856,
 Finset.coe_sort_coe : 0.003399 : 48836,
 OfNat.ofNat_eq_ofNat : 0.000000 : 46478,
 imp_false : 0.005638 : 41329,
 Matrix.empty_val' : 0.003936 : 34042,
 le_refl : 0.032834 : 32619,
 ge_iff_le : 0.006394 : 32532,
 le_of_subsingleton : 0.000354 : 31054,
 and_imp : 0.026419 : 28729,
 imp_self : 0.026351 : 24212,
 imp_not_self : 0.000256 : 23466,
 false_implies : 0.015744 : 22929,
 Ordinal.sup_iterate_eq_nfp : 0.000000 : 22829,
 forall_false : 0.000355 : 22556,
 forall_exists_index : 0.016796 : 21255,
 Prod.forall : 0.008357 : 19745,
 true_implies : 0.015201 : 19406,
 forall_const : 0.011523 : 19352,
 forall_eq : 0.012462 : 19259,
 forall_apply_eq_imp_iff₂ : 0.007189 : 19196,
 forall_eq_or_imp : 0.006946 : 19005,
 Subtype.forall : 0.010180 : 18861,
 forall_eq' : 0.002831 : 18721,
 forall_apply_eq_imp_iff : 0.004873 : 18673,
 forall_eq_apply_imp_iff : 0.000813 : 18456,
 List.forall_mem_ne : 0.000381 : 18361,
 forall_true_left : 0.004631 : 18354,
 Decidable.not_imp_self : 0.000163 : 18349,
 Bool.eq_true_imp_eq_false : 0.000000 : 18342,
 Bool.eq_false_imp_eq_true : 0.000000 : 18342,
 List.forall_mem_ne' : 0.000000 : 18340,
 eq_iff_eq_cancel_right : 0.000000 : 17827,
 eq_iff_eq_cancel_left : 0.000000 : 17827,
 not_imp_self : 0.000000 : 17827,
 Sum.forall : 0.001178 : 17825,
 Nonempty.forall : 0.000168 : 17817,
 IsEmpty.forall_iff : 0.003875 : 17807,
 Bool.forall_bool : 0.008245 : 17223,
 Sigma.forall : 0.002106 : 17097,
 Lex.forall : 0.000177 : 16981,
 OrderDual.forall : 0.000354 : 16972,
 PSigma.forall : 0.000000 : 16758,
 Set.forall_subset_image_iff : 0.000122 : 16438,
 Set.forall_subset_range_iff : 0.000000 : 16424,
 gt_iff_lt : 0.012303 : 16256,
 PProd.forall : 0.000063 : 15762,
 lt_self_iff_false : 0.027571 : 15415,
 Additive.forall : 0.000000 : 14457,
 Multiplicative.forall : 0.000000 : 14457,
 Ordinal.enum_le_enum : 0.000000 : 14430,
 ULift.forall : 0.000149 : 13447,
 PLift.forall : 0.000000 : 13447,
 Fin.forall_fin_zero_pi : 0.000750 : 13334,
 List.forall_mem_ofFn_iff : 0.000151 : 13278,
 LowerAdjoint.closure_le_closed_iff_le : 0.000000 : 12597,
 Algebra.id.smul_eq_mul : 0.009179 : 12529,
 Finset.forall_mem_not_eq : 0.000000 : 12342,
 Finset.forall_mem_not_eq' : 0.000162 : 12342,
 OfNat.ofNat_ne_zero : 0.026288 : 11298,
 Sym.val_eq_coe : 0.001676 : 10740,
 Finset.diag_mem_sym2_mem_iff : 0.000097 : 10317,
 tsub_eq_zero_of_le : 0.014120 : 9065,
 IsEmpty.exists_iff : 0.003771 : 8752,
 exists_const : 0.030980 : 8683,
 NNRat.val_eq_cast : 0.000000 : 8625,
 exists_false : 0.021565 : 8486,
 exists_eq_right : 0.043825 : 8397,
 exists_and_left : 0.020610 : 8394,
 exists_eq_left : 0.016123 : 8311,
 cast_eq : 0.041231 : 8222,
 exists_eq : 0.004622 : 8222,
 exists_and_right : 0.020902 : 7942,
 exists_eq_left' : 0.006554 : 7629,
 Module.End.ofNat_apply : 0.000000 : 7582,
 exists_eq_right' : 0.007396 : 7572,
 exists_eq_right_right : 0.006252 : 7517,
 exists_apply_eq_apply : 0.012773 : 7516,
 exists_eq_or_imp : 0.002396 : 7513,
 exists_eq_right_right' : 0.000939 : 7454,
 exists_or_eq_right : 0.000000 : 7447,
 exists_or_eq_left' : 0.000000 : 7447,
 exists_or_eq_right' : 0.000000 : 7447,
 exists_or_eq_left : 0.000000 : 7447]

[Matthew Ballard]

Read as name : rate : attempts

[Matthew Ballard]

branch#mrb/simp_stats has a working copy of mathlib with an env extension called simpStatExt and you can pull its data with (simpStatExt.getState env).stats which will give you an PersistentHashMap Name (Nat \times Nat) where the first entry is the attempt and the second is the successes

[Matthew Ballard]

(oleans still building)

[Kevin Buzzard]

Wow! Thanks!

[Matthew Ballard]

Next step: see if lake exe refactor can de-simp all non-applying simp theorems with the number of attempts greater than some bound.

[Matthew Ballard]

Ultimately, there will need to be an RFC to

• add a statistics or debug persistent extension
• wrap it in a flag
• disable certain other checks (eg heartbeats)

Then we’ll need to build the tool chain in CI and run workflows off it periodically.

There is a chance the performance penalty of on-by-default isn’t that bad though.

[Matthew Ballard]

All non-applying simp theorems with more than 100 attempts

noSuccess: [(OfNat.ofNat_eq_ofNat, 46478),
 (Ordinal.sup_iterate_eq_nfp, 22829),
 (Bool.eq_true_imp_eq_false, 18342),
 (Bool.eq_false_imp_eq_true, 18342),
 (List.forall_mem_ne', 18340),
 (eq_iff_eq_cancel_right, 17827),
 (eq_iff_eq_cancel_left, 17827),
 (not_imp_self, 17827),
 (PSigma.forall, 16758),
 (Set.forall_subset_range_iff, 16424),
 (Additive.forall, 14457),
 (Multiplicative.forall, 14457),
 (Ordinal.enum_le_enum, 14430),
 (PLift.forall, 13447),
 (LowerAdjoint.closure_le_closed_iff_le, 12597),
 (Finset.forall_mem_not_eq, 12342),
 (NNRat.val_eq_cast, 8625),
 (Module.End.ofNat_apply, 7582),
 (exists_or_eq_left', 7447),
 (exists_or_eq_right, 7447),
 (exists_or_eq_left, 7447),
 (exists_or_eq_right', 7447),
 (exists_apply_eq_apply3', 7120),
 (exists_apply_eq_apply3, 7120),
 (exists_apply_eq_apply2', 7120),
 (exists_subtype_mk_eq_iff, 6985),
 (CharTwo.add_self_eq_zero, 6513),
 (AddSubgroup.forall_zmultiples, 6277),
 (Subgroup.forall_zpowers, 6277),
 (Prod.snd_ofNat, 3337),
 (List.mem_of_find?_eq_some, 3127),
 (Prod.fst_ofNat, 3009),
 (CategoryTheory.Limits.IsZero.map, 2910),
 (le_one_iff_eq_one, 2850),
 (Finset.sum_pi_single, 2118),
 (Nat.ofNat_pos', 2021),
 (Module.isTorsionBySet_singleton_iff, 1764),
 (Set.setOf_bot, 1713),
 (Set.setOf_top, 1672),
 (Set.sep_setOf, 1644),
 (Set.sep_inter, 1247),
 (Set.sep_union, 1247),
 (IsAddUnit.add_neg_cancel, 1147),
 (Set.biUnion_and, 1078),
 (Set.biUnion_self, 1070),
 (Nat.ofNat_nonneg', 1049),
 (bot_eq_one', 1021),
 (Set.biUnion_preimage_singleton, 1006),
 (mul_div_cancel_of_invertible, 958),
 (Bool.cond_self, 935),
 (div_mul_cancel_right, 931),
 (div_mul_cancel_left, 931),
 (Polynomial.coeff_ofNat_succ, 931),
 (left_eq_mul₀, 867),
 (right_eq_mul₀, 867),
 (eq_self_iff_true, 822),
 (IsAddUnit.neg_add_cancel, 807),
 (Finsupp.univ_sum_single_apply', 806),
 (Int.neg_eq_of_add_eq_zero, 788),
 (Set.biInter_and, 770),
 (le_mul_iff_one_le_left', 734),
 (Set.iUnion_Ico_left, 730),
 (Set.iUnion_Ioo_left, 730),
 (Set.iUnion_Ioc_left, 730),
 (Set.iUnion_Icc_left, 730),
 (le_mul_iff_one_le_left, 692),
 (CategoryTheory.MonoidalCoherence.hom, 665),
 (Set.iUnion_vadd_set, 655),
 (Set.iUnion_neg_vadd, 655),
 (Set.iUnion_op_vadd_set, 655),
 (Set.iUnion_op_smul_set, 655),
 (map_eq_zero_iff_eq_zero, 631),
 (map_eq_zero_iff_eq_one, 631),
 (CategoryTheory.Monoidal.transportStruct_whiskerLeft, 628),
 (CategoryTheory.Monoidal.transportStruct_whiskerRight, 609),
 (not_uncountable, 606),
 (Nat.not_even_bit1, 598),
 (Finset.prod_dite_eq, 596),
 (Finset.prod_dite_eq', 596),
 (Finset.prod_ite_irrel, 594),
 (Finset.prod_dite_irrel, 594),
 (Denumerable.ofNat_of_decode, 561),
 (one_le, 542),
 (Finset.prod_inv_distrib, 527),
 (IsAddUnit.add_sub_cancel_right, 524),
 (mul_le_iff_le_one_left', 522),
 (commutatorElement_self, 514),
 (MonoidHom.CompTriple.comp_assoc, 480),
 (Nat.exists_ne_zero, 464),
 (mul_le_iff_le_one_left, 461),
 (lt_mul_iff_one_lt_right', 448),
 (lt_mul_iff_one_lt_left', 448),
 (not_countable, 446),
 (lt_mul_iff_one_lt_left, 446),
 (lt_mul_iff_one_lt_right, 446),
 (IsField.nontrivial, 430),
 (CategoryTheory.Limits.IsLimit.lift_self, 430),
 (Nat.not_ofNat_lt_one, 422),
 (MulOpposite.op_ofNat, 412),
 (Finset.filter_const, 407),
 (isUnit_of_map_unit, 396),
 (MeasurableSpace.measurableSet_inf, 367),
 (IsAddUnit.sub_add_cancel, 366),
 (Set.Icc_eq_empty_of_lt, 363),
 (MeasurableSpace.measurableSet_sInf, 361),
 (HMul.hMul, 352),
 (IsRegular.right, 344),
 (AlternatingMap.map_eq_zero_of_eq, 329),
 (Set.exists_subset_image_iff, 325),
 (CategoryTheory.BicategoricalCoherence.tensorRight'_hom, 295),
 (CategoryTheory.Arrow.hom.congr_right, 295),
 (Nat.lt_mul_iff_one_lt_left, 289),
 (Nat.lt_mul_self_iff, 286),
 (Nat.lt_mul_iff_one_lt_right, 286),
 (mul_cancel_left_mem_nonZeroDivisors, 270),
 (IsNoetherian.coeSort_finsetBasisIndex, 263),
 (ULift.up_ofNat, 262),
 (Filter.eventually_all_finset, 237),
 (le_div_self_iff, 222),
 (AffineBasis.linear_combination_coord_eq_self, 221),
 (himp_self, 220),
 (Finsupp.sum_sub, 218),
 (Finsupp.sum_neg, 218),
 (div_eq_self, 216),
 (MulOpposite.unop_ofNat, 216),
 (Cardinal.lift_umax', 215),
 (Cardinal.lift_umax, 215),
 (MeasureTheory.lintegral_add_right, 207),
 (Set.Ioo_eq_empty_of_le, 205),
 (Set.range_id', 203),
 (mul_lt_iff_lt_one_right', 194),
 (mul_lt_iff_lt_one_right, 191),
 (Polynomial.coeff_ofNat_zero, 188),
 (intervalIntegral.integral_add, 185),
 (LinearMap.identityMapOfZeroModuleIsZero, 183),
 (Set.Ico_eq_empty_of_le, 177),
 (div_self_mul_self, 177),
 (div_mul_cancel₀, 177),
 (WithBot.coe_ofNat, 173),
 (Classical.imp_iff_left_iff, 169),
 (intervalIntegral.integral_mul_const, 168),
 (Int.le_refl, 167),
 (GradedMonoid.GradeZero.smul_eq_mul, 166),
 (MulCharClass.map_nonunit, 161),
 (IsRightRegular.mul_right_eq_zero_iff, 160),
 (dif_ctx_congr, 159),
 (Mathlib.Tactic.NoncommRing.mul_nat_lit_eq_nsmul, 155),
 (Mathlib.Tactic.NoncommRing.nat_lit_mul_eq_nsmul, 155),
 (Complex.cpow_ofNat, 153),
 (Nat.cast_le_ofNat, 149),
 (ULift.down_ofNat, 148),
 (lt_inv_self_iff, 147),
 (IsAddUnit.add_neg_cancel_left, 146),
 (tsum_const, 144),
 (CategoryTheory.Limits.Fork.condition, 142),
 (mul_le_mul_iff_right, 141),
 (BEq.refl, 140),
 (Classical.choose_eq', 131),
 (Classical.choose_eq, 131),
 (mul_isLeftRegular_iff, 130),
 (CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right', 129),
 (div_le_self_iff, 128),
 (inv_mul_cancel_comm_assoc, 127),
 (PNat.mk_ofNat, 127),
 (EuclideanDomain.mod_self, 127),
 (Cardinal.lift_ofNat, 124),
 (Matrix.transpose_ofNat, 123),
 (CategoryTheory.Iso.symm_self_id, 121),
 (le_inv_self_iff, 120),
 (mul_le_mul_left_of_neg, 119),
 (Norm.norm, 116),
 (Finset.filter_univ_mem, 114),
 (CategoryTheory.Limits.Cofork.condition, 114),
 (Bind.bind, 112),
 (MeasureTheory.Integrable.of_finite, 112),
 (Multiset.prod_map_inv, 111),
 (Multiset.prod_map_div, 111),
 (Disjoint.of_image_finset, 110),
 (Option.map_id'', 109),
 (mul_self_mul_inv, 107),
 (div_lt_self_iff, 107),
 (ZMod.unitsMap_self, 107),
 (Polynomial.eval₂_ofNat, 106),
 (intervalIntegral.integral_comp_add_left, 105),
 (coe_fourierBasis, 105),
 (List.prod_take_succ, 105),
 (OrthonormalBasis.coe_toHilbertBasis, 105),
 (HilbertBasis.coe_mk, 105),
 (HilbertBasis.coe_mkOfOrthogonalEqBot, 105),
 (Complex.ofNat_arg, 102),
 (OfNat.ofNat, 102)]

#15676 is sanity check which de-simps the worst offender

[Damiano Testa]

Matt, I can take a look into using refactor for removing the simp tag: if you can you provide the predicate to choose when to remove the tag, I can try to automate the removal.

[Matthew Ballard]

env.getSuccesses declName == some 0 && env.getAttempts declName |>get! > 100 probably

[Damiano Testa]

Ok, let me try this out!

[Damiano Testa]

Out of curiosity, is there every in mathlib a place with @[simp, simp]?

[Damiano Testa]

Are getSuccesses and getAttempts defined somewhere else?

[Matthew Ballard]

Only on that branch above

[Damiano Testa]

Ah, got it!

[Damiano Testa]

I am looking in branch#mrb/simp_stats but I can't seem to find those functions either...

[Matthew Ballard]

Oops they return options so end in ?. Sorry. They should populate when dotting off an environment.

[Damiano Testa]

I grepped for getSuccesses in your branch but could not find them (I had guessed that env was an Environment, but that did not help).

[Damiano Testa]

I am also finding that I cannot get refactor to run:

$ lake exe refactor --help
PANIC at List.head! Init.Data.List.BasicAux:58:12: empty list
backtrace:
././.lake/build/bin/refactor(lean_panic_fn+0x9e)[0x56470a31b1ee]
././.lake/build/bin/refactor(_lean_main+0x5f3)[0x5647066befc3]
././.lake/build/bin/refactor(+0xe5fed3)[0x5647066c9ed3]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90)[0x7f773ffb8d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80)[0x7f773ffb8e40]
././.lake/build/bin/refactor(_start+0x25)[0x56470667de65]
uncaught exception: [anonymous] not found

[Damiano Testa]

I should have working code that selects all simp attributes (the "easy" ones, passed as @[..., simp,...], for a command. What is missing is the filter on the declarations for when to perform the removal and refactor actually working...

[Matthew Ballard]

It’s defined in a modified tool chain

[Matthew Ballard]

Here is the code that defines it

import Lean.Environment

open Lean

structure SimpStatEntry where
  name : Name
  attempts : Nat := 0
  successes : Nat := 0
deriving Inhabited

structure SimpStatState where
  stats : PersistentHashMap Name (Nat × Nat) := {}
deriving Inhabited

namespace SimpStatState

def addEntry (s : SimpStatState) (entry : SimpStatEntry) : SimpStatState :=
  { s with stats :=
      if let some stats := s.stats.find? entry.name then
        s.stats.insert entry.name (stats.1 + entry.attempts, stats.2 + entry.successes)
      else
        s.stats.insert entry.name (entry.attempts, entry.successes) }

end SimpStatState

open SimpStatState

builtin_initialize simpStatExt : SimplePersistentEnvExtension SimpStatEntry SimpStatState ←
  registerSimplePersistentEnvExtension {
    addEntryFn    := SimpStatState.addEntry
    addImportedFn := fun es => (mkStateFromImportedEntries addEntry {} es)}

def Lean.Environment.getAttempts? (env : Environment) (declName : Name) : Option Nat :=
  (simpStatExt.getState env).stats.find? declName |>.map (·.1)

def Lean.Environment.getAllAttempts (env : Environment) : Array (Name × Nat) :=
  (simpStatExt.getState env).stats.toArray |>.map fun (n, (a, _)) => (n, a)

def Lean.Environment.getSuccesses? (env : Environment) (declName : Name) : Option Nat :=
  (simpStatExt.getState env).stats.find? declName |>.map (·.2)

def Lean.Environment.getAllSuccesses (env : Environment) : Array (Name × Nat) :=
  (simpStatExt.getState env).stats.toArray |>.map fun (n, (_, s)) => (n, s)

I just tested that cache pulls down everything ok on the branch.

[Matthew Ballard]

Here is the snippet I ran to get the last output

import Mathlib

open Lean Meta

run_cmd do
  let env ← getEnv
  let noSuccess := env.getAllSuccesses.filter (fun a => a.2 == 0)
  let mut arr := #[]
  for (n, _) in noSuccess do
    if let some attempts := env.getAttempts? n then
      if attempts > 100 then
      arr := arr.push (n, attempts)
      -- msgs := msgs.push m!"{n} : {attempts}"
  arr := arr.qsort (fun a b => a.2 > b.2)
  logInfo m!"noSuccess: {arr}"

[Damiano Testa]

I was not really able to get this to work: even without your filter, lake exe refactor would just tell me what the edits are, but not actually perform them.

#15679 has what I got so far: I merged refactor and your branch into master, added some modifications to Refactor.Main and nothing else. CI has a step before build that runs refactor, but it really does nothing.

If you fill in the sorry in getSimpAttrEdits in Refactor.Main with your filter, and if you get refactor to work with lake exe refactor, then this may do what is desired! :smile:

[Yury G. Kudryashov]

Note that some of the matched lemmas are multiplicative versions of useful additive lemmas.

[Yury G. Kudryashov]

Why Norm.norm is in the list?

[Matthew Ballard]

I tracked heartbeats for the main step. Here are the most expensive 100

[(not_isEmpty_of_nonempty, 11228823956),
 (IsEmpty.forall_iff, 4907042842),
 (IsEmpty.exists_iff, 4018388635),
 (map_zero, 1580293036),
 (Mathlib.Tactic.Coherence.assoc_liftHom, 1489564221),
 (tsub_eq_zero_of_le, 1454666275),
 (le_of_subsingleton, 1439108160),
 (map_mul, 1436879370),
 (map_add, 1435809953),
 (Finset.univ_eq_empty, 1224721722),
 (CategoryTheory.shiftFunctor_of_induced, 1018155319),
 (map_one, 985383823),
 (forall_const, 831695985),
 (Fintype.card_eq_zero, 811649670),
 (map_sub, 786178350),
 (eq_self, 724576940),
 (map_smul, 719096597),
 (Mathlib.Tactic.BicategoryCoherence.assoc_liftHom₂, 704402159),
 (mul_div_cancel_left, 567565396),
 (MeasureTheory.lintegral_of_isEmpty, 548997894),
 (SetLike.coe_sort_coe, 532177001),
 (mul_ne_zero, 527068999),
 (mul_div_cancel_right, 523964399),
 (ModuleCat.restrictScalars.smul_def, 470762956),
 (Set.iUnion_of_empty, 432129914),
 (one_smul, 418809849),
 (map_eq_zero, 409856181),
 (Nat.sub_eq_zero_of_le, 343354425),
 (sup_of_le_left, 338554766),
 (eq_div_iff, 336465676),
 (Cardinal.mk_eq_zero, 322847692),
 (inf_of_le_left, 317363600),
 (add_comm, 299955379),
 (mul_comm, 299256764),
 (Int.neg_eq_of_add_eq_zero, 292057969),
 (sup_of_le_right, 286474836),
 (add_zero, 285187247),
 (map_neg, 284181960),
 (CategoryTheory.Category.assoc, 284044997),
 (mul_eq_right₀, 279422307),
 (LinearMap.map_coe_ker, 279413415),
 (mul_eq_left₀, 279289046),
 (zero_smul, 278138245),
 (inf_of_le_right, 277297725),
 (div_eq_iff, 273798186),
 (CharP.cast_eq_zero, 267760549),
 (nhds_discrete, 263663518),
 (OfNat.ofNat_eq_ofNat, 263554531),
 (CharTwo.sub_eq_add, 262935525),
 (CStarRing.norm_of_mem_unitary, 244229265),
 (AddSubgroup.coe_norm, 237801347),
 (smul_zero, 237094212),
 (Submodule.coe_norm, 235752765),
 (map_sum, 230792264),
 (add_right_eq_self, 225163652),
 (Set.coe_setOf, 224096524),
 (CategoryTheory.Monoidal.transportStruct_tensorObj, 223240399),
 (Set.iInter_of_empty, 221876410),
 (smul_smul, 220748228),
 (CategoryTheory.Functor.comp_obj, 218055277),
 (mul_one, 209126875),
 (add_left_eq_self, 204996520),
 (Finset.coe_sort_coe, 201067534),
 (mul_div_mul_left_eq_div, 197108257),
 (tsum_empty, 195885727),
 (le_refl, 193008550),
 (smul_add, 188465791),
 (Set.insert_eq_of_mem, 183702419),
 (mul_div_mul_right_eq_div, 181501000),
 (Function.extend_apply', 179814865),
 (CharTwo.neg_eq, 174198934),
 (cast_eq, 173123288),
 (exists_const, 169861143),
 (reduceIte, 164249838),
 (isNilpotent_iff_eq_zero, 159571500),
 (nsmul_eq_mul, 156038399),
 (mul_right_eq_self, 152760948),
 (zsmul_eq_mul, 152084922),
 (Cardinal.mk_eq_aleph0, 150586486),
 (mul_left_eq_self, 149895549),
 (max_eq_left, 149358694),
 (zero_le, 149024858),
 (Set.Icc_eq_empty, 148324858),
 (dreduceIte, 147362608),
 (MulZeroClass.mul_zero, 147254384),
 (add_eq_zero_iff, 139860498),
 (isUnit_iff_ne_zero, 136702874),
 (map_pow, 135382430),
 (Disjoint.of_image_finset, 134899921),
 (map_eq_zero_iff_eq_zero, 134186741),
 (add_le_iff_nonpos_left, 133157265),
 (div_sub', 132196134),
 (CompTriple.comp_eq, 129192320),
 (List.mem_of_find?_eq_some, 128817146),
 (CommRingCat.forget_obj, 128240941),
 (div_eq_div_iff, 123703284),
 (add_add_add_comm, 122143332),
 (CategoryTheory.Discrete.functor_map_id, 121272918),
 (Nat.cast_ofNat, 119380375),
 (mul_eq_zero, 118788662)]

[Matthew Ballard]

Yury G. Kudryashov said:

Why Norm.norm is in the list?

It is tracking unfolding things in simp also

[Matthew Ballard]

More context: (name, (attempts, (success rate, heartbeats)))

sorted: [(not_isEmpty_of_nonempty, (30735, (0.309094, 11228823956))),
 (IsEmpty.forall_iff, (17807, (0.003875, 4907042842))),
 (IsEmpty.exists_iff, (8752, (0.003771, 4018388635))),
 (map_zero, (1368, (0.733918, 1580293036))),
 (Mathlib.Tactic.Coherence.assoc_liftHom, (8263, (0.332688, 1489564221))),
 (tsub_eq_zero_of_le, (9065, (0.014120, 1454666275))),
 (le_of_subsingleton, (31054, (0.000354, 1439108160))),
 (map_mul, (1589, (0.707363, 1436879370))),
 (map_add, (1051, (0.758325, 1435809953))),
 (Finset.univ_eq_empty, (1231, (0.033306, 1224721722))),
 (CategoryTheory.shiftFunctor_of_induced, (3736, (0.005086, 1018155319))),
 (map_one, (1437, (0.408490, 985383823))),
 (forall_const, (19352, (0.011523, 831695985))),
 (Fintype.card_eq_zero, (597, (0.010050, 811649670))),
 (map_sub, (602, (0.699336, 786178350))),
 (eq_self, (175970, (0.182582, 724576940))),
 (map_smul, (475, (0.616842, 719096597))),
 (Mathlib.Tactic.BicategoryCoherence.assoc_liftHom₂, (1636, (0.496333, 704402159))),
 (mul_div_cancel_left, (1174, (0.001704, 567565396))),
 (MeasureTheory.lintegral_of_isEmpty, (383, (0.015666, 548997894))),
 (SetLike.coe_sort_coe, (48856, (0.006100, 532177001))),
 (mul_ne_zero, (291, (0.725086, 527068999))),
 (mul_div_cancel_right, (1177, (0.003398, 523964399))),
 (ModuleCat.restrictScalars.smul_def, (24, (0.291667, 470762956))),
 (Set.iUnion_of_empty, (1253, (0.033520, 432129914))),
 (one_smul, (862, (0.967517, 418809849))),
 (map_eq_zero, (1072, (0.058769, 409856181))),
 (Nat.sub_eq_zero_of_le, (1363, (0.014674, 343354425))),
 (sup_of_le_left, (975, (0.112821, 338554766))),
 (eq_div_iff, (241, (0.780083, 336465676))),
 (Cardinal.mk_eq_zero, (360, (0.030556, 322847692))),
 (inf_of_le_left, (873, (0.076747, 317363600))),
 (add_comm, (3028, (0.209709, 299955379))),
 (mul_comm, (4392, (0.186703, 299256764))),
 (Int.neg_eq_of_add_eq_zero, (788, (0.000000, 292057969))),
 (sup_of_le_right, (878, (0.046697, 286474836))),
 (add_zero, (4602, (0.994785, 285187247))),
 (map_neg, (195, (0.625641, 284181960))),
 (CategoryTheory.Category.assoc, (11555, (0.999913, 284044997))),
 (mul_eq_right₀, (1286, (0.001555, 279422307))),
 (LinearMap.map_coe_ker, (375, (0.021333, 279413415))),
 (mul_eq_left₀, (1288, (0.002329, 279289046))),
 (zero_smul, (610, (0.893443, 278138245))),
 (inf_of_le_right, (808, (0.074257, 277297725))),
 (div_eq_iff, (199, (0.723618, 273798186))),
 (CharP.cast_eq_zero, (3125, (0.042880, 267760549))),
 (nhds_discrete, (844, (0.015403, 263663518))),
 (OfNat.ofNat_eq_ofNat, (46478, (0.000000, 263554531))),
 (CharTwo.sub_eq_add, (4025, (0.000248, 262935525))),
 (CStarRing.norm_of_mem_unitary, (1939, (0.000516, 244229265))),
 (AddSubgroup.coe_norm, (35, (0.057143, 237801347))),
 (smul_zero, (460, (0.941304, 237094212))),
 (Submodule.coe_norm, (37, (0.243243, 235752765))),
 (map_sum, (162, (0.938272, 230792264))),
 (add_right_eq_self, (3578, (0.013695, 225163652))),
 (Set.coe_setOf, (51858, (0.002680, 224096524))),
 (CategoryTheory.Monoidal.transportStruct_tensorObj, (5666, (0.032298, 223240399))),
 (Set.iInter_of_empty, (821, (0.019488, 221876410))),
 (smul_smul, (324, (0.867284, 220748228))),
 (CategoryTheory.Functor.comp_obj, (14098, (1.000000, 218055277))),
 (mul_one, (4269, (0.988756, 209126875))),
 (add_left_eq_self, (3537, (0.005655, 204996520))),
 (Finset.coe_sort_coe, (48836, (0.003399, 201067534))),
 (mul_div_mul_left_eq_div, (367, (0.002725, 197108257))),
 (tsum_empty, (206, (0.009709, 195885727))),
 (le_refl, (32619, (0.032834, 193008550))),
 (smul_add, (331, (0.933535, 188465791))),
 (Set.insert_eq_of_mem, (584, (0.041096, 183702419))),
 (mul_div_mul_right_eq_div, (371, (0.010782, 181501000))),
 (Function.extend_apply', (56, (0.035714, 179814865))),
 (CharTwo.neg_eq, (3368, (0.000297, 174198934))),
 (cast_eq, (8222, (0.041231, 173123288))),
 (exists_const, (8683, (0.030980, 169861143))),
 (reduceIte, (8812, (0.145030, 164249838))),
 (isNilpotent_iff_eq_zero, (58, (0.017241, 159571500))),
 (nsmul_eq_mul, (534, (0.372659, 156038399))),
 (mul_right_eq_self, (1386, (0.009380, 152760948))),
 (zsmul_eq_mul, (348, (0.255747, 152084922))),
 (Cardinal.mk_eq_aleph0, (280, (0.039286, 150586486))),
 (mul_left_eq_self, (1371, (0.008753, 149895549))),
 (max_eq_left, (583, (0.190395, 149358694))),
 (zero_le, (1939, (0.170707, 149024858))),
 (Set.Icc_eq_empty, (378, (0.039683, 148324858))),
 (dreduceIte, (7467, (0.003348, 147362608))),
 (MulZeroClass.mul_zero, (2521, (0.980167, 147254384))),
 (add_eq_zero_iff, (1425, (0.011228, 139860498))),
 (isUnit_iff_ne_zero, (2813, (0.091006, 136702874))),
 (map_pow, (360, (0.900000, 135382430))),
 (Disjoint.of_image_finset, (110, (0.000000, 134899921))),
 (map_eq_zero_iff_eq_zero, (631, (0.000000, 134186741))),
 (add_le_iff_nonpos_left, (889, (0.175478, 133157265))),
 (div_sub', (77, (0.974026, 132196134))),
 (CompTriple.comp_eq, (1312, (0.006098, 129192320))),
 (List.mem_of_find?_eq_some, (3127, (0.000000, 128817146))),
 (CommRingCat.forget_obj, (602, (0.397010, 128240941))),
 (div_eq_div_iff, (51, (0.000000, 123703284))),
 (add_add_add_comm, (73, (0.301370, 122143332))),
 (CategoryTheory.Discrete.functor_map_id, (4774, (0.011730, 121272918))),
 (Nat.cast_ofNat, (18386, (0.113510, 119380375))),
 (mul_eq_zero, (383, (0.522193, 118788662)))]

[Matthew Ballard]

Heartbeats per attempt

sorted: [(Finset.inv_op_smul_finset_distrib, 83170014.000000),
 (Finset.inv_smul_finset_distrib, 24826784.333333),
 (ModuleCat.restrictScalars.smul_def, 19615123.166667),
 (Submodule.coe_inner, 18632432.666667),
 (SubalgebraClass.coe_algebraMap, 7486192.666667),
 (Set.inv_op_smul_set_distrib, 7061247.000000),
 (AddSubgroup.coe_norm, 6794324.200000),
 (Basis.baseChange_repr_tmul, 6430519.000000),
 (Submodule.coe_norm, 6371696.351351),
 (Mathlib.Vector.mapAccumr₂_eq_map₂_of_unused_state, 5451155.750000),
 (map_dfinsupp_sum, 5342288.500000),
 (NonUnitalSubalgebra.coe_smul, 5028333.000000),
 (ENNReal.ofReal_lt_ofReal_iff, 4870833.000000),
 (LinearMap.trace_id, 4843904.000000),
 (TensorProduct.LieModule.lie_tmul_right, 4628821.714286),
 (algebraicIndependent_empty_type_iff, 4553185.400000),
 (mul_lt_mul, 4418742.000000),
 (IsClopen.frontier_eq, 4382894.555556),
 (map_rat_smul, 4225411.500000),
 (Basis.baseChange_apply, 4166844.000000),
 (Abelianization.mk_eq_of, 4164122.000000),
 (Nat.cast_le_one, 4020733.200000),
 (div_sub_div, 3994255.000000),
 (Algebra.norm_zero, 3849456.000000),
 (Matrix.rank_mul_eq_right_of_isUnit_det, 3673892.000000),
 (Subtype.mk_inf_mk, 3634497.000000),
 (AlgebraicGeometry.StructureSheaf.res_const, 3607583.000000),
 (Mathlib.Vector.mapAccumr₂_unused_input_right, 3534614.800000),
 (Mathlib.Vector.mapAccumr_eq_map_of_unused_state, 3533604.125000),
 (Cardinal.card_lt_of_card_iUnion_lt, 3439133.611111),
 (Mathlib.Vector.mapAccumr₂_unused_input_left, 3416460.235294),
 (Ideal.radical_bot_of_noZeroDivisors, 3325406.500000),
 (Function.extend_apply', 3210979.732143),
 (Subtype.coe_inf, 3106751.666667),
 (AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent, 2988032.000000),
 (HomologicalComplex₂.total.map_comp, 2897436.000000),
 (Matrix.rank_mul_eq_left_of_isUnit_det, 2886457.000000),
 (Metric.smul_sphere, 2757356.000000),
 (isNilpotent_iff_eq_zero, 2751232.758621),
 (MeasureTheory.measure_vadd, 2743770.000000),
 (rootsOfUnityEquivOfPrimitiveRoots_symm_apply, 2497438.000000),
 (isOpen_biUnion, 2479237.000000),
 (div_eq_div_iff, 2425554.588235),
 (Submodule.orthogonal_eq_bot_iff, 2390252.666667),
 (Function.Injective.of_comp_iff', 2378635.538462),
 (Fintype.card_pos, 2372341.000000),
 (Finsupp.sum_add_index, 2352309.800000),
 (Submodule.finrank_eq_zero, 2347932.750000),
 (unitary.star_mul_self_of_mem, 2244604.745098),
 (MeasureTheory.measure_smul, 2236712.333333),
 (isClopen_discrete, 2166347.055556),
 (HomologicalComplex₂.homMk_f_f, 2136987.500000),
 (LinearMap.map_smul_of_tower, 2124068.190476),
 (Set.inv_smul_set_distrib, 2106113.666667),
 (TensorProduct.tmul_smul, 2094319.550000),
 (div_nonneg, 2077201.000000),
 (Finset.sum_image, 2007987.000000),
 (Submodule.smul_bot', 1972433.000000),
 (Algebra.norm_eq_zero_iff, 1966722.000000),
 (MvPolynomial.aeval_map_algebraMap, 1956308.000000),
 (Matrix.dotProduct_smul, 1909540.000000),
 (Basis.mem_span_iff_repr_mem, 1843813.000000),
 (mul_ne_zero, 1811233.673540),
 (mem_closure_iff_seq_limit, 1805393.000000),
 (Mathlib.Vector.mapAccumr₂_eq_map₂_of_constant_state, 1775023.684211),
 (div_sub', 1716832.909091),
 (WeierstrassCurve.Affine.slope_of_Y_ne, 1700805.500000),
 (units_smul_eq_neg_iff, 1692275.000000),
 (LieModule.traceForm_eq_zero_of_isNilpotent, 1683455.951220),
 (add_add_add_comm, 1673196.328767),
 (ContinuousLinearMap.map_smul_of_tower, 1670938.833333),
 (BoundedContinuousFunction.norm_eq_zero_of_empty, 1656178.720000),
 (Cardinal.mul_aleph0_eq, 1596180.000000),
 (map_ratCast, 1587507.200000),
 (IsOpen.inter, 1585011.000000),
 (Finsupp.prod_add_index, 1578030.000000),
 (mul_pos_iff, 1554729.000000),
 (LinearMap.comp_smul, 1534000.500000),
 (map_smul, 1513887.572632),
 (Finset.prod_image, 1509163.333333),
 (smul_ceilDiv, 1491045.000000),
 (smul_floorDiv, 1491027.000000),
 (ENNReal.inv_mul_cancel, 1471952.000000),
 (mul_nonneg, 1464974.666667),
 (map_neg, 1457343.384615),
 (nilradical_eq_zero, 1443550.000000),
 (MeasureTheory.lintegral_of_isEmpty, 1433414.866841),
 (CategoryTheory.GradedObject.mapMap_comp, 1429147.000000),
 (map_sum, 1424643.604938),
 (TensorProduct.gradedMul_algebraMap, 1420836.000000),
 (mul_neg_iff, 1396360.000000),
 (eq_div_iff, 1396123.136929),
 (Polynomial.aeval_algebraMap_eq_zero_iff, 1391559.500000),
 (mul_nonpos_iff, 1382966.000000),
 (Nat.one_le_cast, 1381660.941176),
 (TensorProduct.gradedComm_one, 1378706.000000),
 (div_eq_iff, 1375870.281407),
 (map_add, 1366136.967650),
 (DFinsupp.sum_eq_sum_fintype, 1360130.000000),
 (Fintype.card_eq_zero, 1359547.185930)]

I don't know the significant digits function for Float

[Matthew Ballard]

Most expensive for total heartbeats with no successes and attempts listed

noSuccess: [(Int.neg_eq_of_add_eq_zero, (788, 292057969)),
 (OfNat.ofNat_eq_ofNat, (46478, 263554531)),
 (Disjoint.of_image_finset, (110, 134899921)),
 (map_eq_zero_iff_eq_zero, (631, 134186741)),
 (List.mem_of_find?_eq_some, (3127, 128817146)),
 (div_eq_div_iff, (51, 123703284)),
 (Ordinal.enum_le_enum, (14430, 105116509)),
 (LowerAdjoint.closure_le_closed_iff_le, (12597, 101160280)),
 (not_countable, (446, 95697687)),
 (map_eq_zero_iff_eq_one, (631, 91893225)),
 (not_uncountable, (606, 91232635)),
 (mul_le_iff_le_one_left', (522, 90653126)),
 (CategoryTheory.Limits.IsZero.map, (2910, 90167377)),
 (Set.Ico_eq_empty_of_le, (177, 89289302)),
 (Nat.ofNat_pos', (2021, 85695222)),
 (Finset.inv_op_smul_finset_distrib, (1, 83170014)),
 (CharTwo.add_self_eq_zero, (6513, 76430415)),
 (Finset.inv_smul_finset_distrib, (3, 74480353)),
 (ULift.up_ofNat, (262, 73136873)),
 (Set.Ioo_eq_empty_of_le, (205, 72189867)),
 (LieModule.traceForm_eq_zero_of_isNilpotent, (41, 69021694)),
 (Submodule.smul_torsionBy, (70, 67309370)),
 (Set.Icc_eq_empty_of_lt, (363, 64921232)),
 (Cardinal.card_lt_of_card_iUnion_lt, (18, 61904405)),
 (mul_le_mul_iff_right, (141, 58196620)),
 (Mathlib.Vector.mapAccumr₂_unused_input_left, (17, 58079824)),
 (Submodule.coe_inner, (3, 55897298)),
 (le_one_iff_eq_one, (2850, 54404312)),
 (Mathlib.Vector.mapAccumr₂_unused_input_right, (15, 53019222)),
 (Nat.not_ofNat_lt_one, (422, 52765867)),
 (MonoidHom.CompTriple.comp_assoc, (480, 49067233)),
 (IsField.nontrivial, (430, 48989440)),
 (IsAddUnit.add_sub_cancel_right, (524, 48527977)),
 (mul_div_cancel_of_invertible, (958, 45980310)),
 (Module.End.ofNat_apply, (7582, 45706315)),
 (SubalgebraClass.coe_algebraMap, (6, 44917156)),
 (AlternatingMap.map_eq_zero_of_eq, (329, 44836056)),
 (Nat.ofNat_nonneg', (1049, 44354161)),
 (bot_eq_one', (1021, 43852452)),
 (BoundedContinuousFunction.norm_eq_zero_of_empty, (25, 41404468)),
 (IsUnit.smul_eq_zero, (79, 41259111)),
 (IsClopen.frontier_eq, (9, 39446051)),
 (isClopen_discrete, (18, 38994247)),
 (MeasureTheory.measure_univ_of_isMulLeftInvariant, (85, 36555750)),
 (IsRightRegular.mul_right_eq_zero_iff, (160, 36237481)),
 (Multiset.bijective_iff_map_univ_eq_univ, (62, 33800657)),
 (Mathlib.Vector.mapAccumr₂_eq_map₂_of_constant_state, (19, 33725450)),
 (Denumerable.ofNat_of_decode, (561, 33241550)),
 (Nat.card_of_isEmpty, (27, 31925699)),
 (not_imp_self, (17827, 31600556)),
 (MulCharClass.map_nonunit, (161, 31272959)),
 (Function.Injective.of_comp_iff', (13, 30922262)),
 (AddConstMapClass.map_const, (96, 30416170)),
 (le_mul_iff_one_le_left, (692, 29580998)),
 (Submodule.smul_coe_torsionBy, (53, 29077380)),
 (IsAddUnit.neg_add_cancel, (807, 28695055)),
 (Mathlib.Vector.mapAccumr_eq_map_of_unused_state, (8, 28268833)),
 (NNRat.val_eq_cast, (8625, 26358050)),
 (multiplicity.isUnit_left, (81, 25410663)),
 (mul_le_iff_le_one_left, (461, 24718913)),
 (LinearMap.identityMapOfZeroModuleIsZero, (183, 24359064)),
 (CategoryTheory.Monoidal.transportStruct_whiskerLeft, (628, 23695643)),
 (CategoryTheory.Monoidal.transportStruct_whiskerRight, (609, 22937415)),
 (IsAddUnit.sub_add_cancel, (366, 22239217)),
 (Mathlib.Vector.mapAccumr₂_eq_map₂_of_unused_state, (4, 21804623)),
 (MeasureTheory.Measure.sum_of_isEmpty, (21, 21742663)),
 (lt_mul_iff_one_lt_left', (448, 20969180)),
 (List.forall_mem_ne', (18340, 20489625)),
 (Prod.snd_ofNat, (3337, 19817017)),
 (div_eq_self, (216, 19607621)),
 (tprod_empty, (15, 19509021)),
 (mul_le_mul_left_of_neg, (119, 18652091)),
 (Prod.fst_ofNat, (3009, 18420507)),
 (GradedMonoid.GradeZero.smul_eq_mul, (166, 18370648)),
 (le_mul_iff_one_le_left', (734, 18321675)),
 (List.prod_map_mul, (63, 18320320)),
 (one_le, (542, 16929598)),
 (mul_lt_mul_iff_right, (39, 16903523)),
 (mul_cancel_left_mem_nonZeroDivisors, (270, 16811634)),
 (eq_iff_eq_cancel_left, (17827, 16717964)),
 (eq_iff_eq_cancel_right, (17827, 16683980)),
 (Basis.orientation_isEmpty, (14, 16041890)),
 (IsRegular.right, (344, 15727940)),
 (exists_apply_eq_apply3, (7120, 15275202)),
 (exists_apply_eq_apply3', (7120, 15267073)),
 (Finset.forall_mem_not_eq, (12342, 14756517)),
 (smul_le_iff_le_one_left, (12, 14410706)),
 (Nat.cast_le_ofNat, (149, 14031693)),
 (exists_apply_eq_apply2', (7120, 13824453)),
 (mul_isLeftRegular_iff, (130, 13470493)),
 (mul_lt_iff_lt_one_right', (194, 13073532)),
 (isUnit_of_map_unit, (396, 12035234)),
 (left_eq_mul₀, (867, 11988823)),
 (exists_or_eq_right, (7447, 11930417)),
 (exists_or_eq_left, (7447, 11925900)),
 (exists_or_eq_right', (7447, 11923827)),
 (exists_or_eq_left', (7447, 11918242)),
 (le_smul_iff_one_le_left, (28, 11762239)),
 (right_eq_mul₀, (867, 11757824)),
 (PSigma.forall, (16758, 11302933))]

[Kevin Buzzard]

I couldn't resist trying #15696

[Yaël Dillies]

You were not the first one to not resist trying: #15676

[Matthew Ballard]

Here are the no successes with their keys. Some simprocs made it in and they don't have keys

noSuccess: [(OfNat.ofNat_eq_ofNat, (46478, [Eq, *, *, *])),
 (Ordinal.sup_iterate_eq_nfp, (22829, [◾])),
 (Bool.eq_true_imp_eq_false, (18342, [→])),
 (Bool.eq_false_imp_eq_true, (18342, [→])),
 (List.forall_mem_ne', (18340, [→])),
 (eq_iff_eq_cancel_right, (17827, [→])),
 (eq_iff_eq_cancel_left, (17827, [→])),
 (not_imp_self, (17827, [→])),
 (PSigma.forall, (16758, [→])),
 (Set.forall_subset_range_iff, (16424, [→])),
 (Additive.forall, (14457, [→])),
 (Multiplicative.forall, (14457, [→])),
 (Ordinal.enum_le_enum, (14430, [Not, *])),
 (PLift.forall, (13447, [→])),
 (LowerAdjoint.closure_le_closed_iff_le, (12597, [LE.le, *, *, *, *])),
 (Finset.forall_mem_not_eq, (12342, [→])),
 (NNRat.val_eq_cast, (8625, [Subtype.0, *])),
 (Module.End.ofNat_apply,
  (7582, [DFunLike.coe, LinearMap, *, *, *, *, RingHom.id, *, *, *, *, *, *, *, *, *, *, *, *, *])),
 (exists_or_eq_right, (7447, [Exists, *, ◾])),
 (exists_or_eq_left', (7447, [Exists, *, ◾])),
 (exists_or_eq_right', (7447, [Exists, *, ◾])),
 (exists_or_eq_left, (7447, [Exists, *, ◾])),
 (exists_apply_eq_apply3, (7120, [Exists, *, ◾])),
 (exists_apply_eq_apply3', (7120, [Exists, *, ◾])),
 (exists_apply_eq_apply2', (7120, [Exists, *, ◾])),
 (exists_subtype_mk_eq_iff, (6985, [Exists, *, ◾])),
 (Nat.reduceGT,
  (6640,
   [ReaderT,
    _private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.MethodsRef,
    ReaderT,
    Lean.Meta.Simp.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Meta.Simp.State,
    ReaderT,
    Lean.Meta.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Meta.State,
    ReaderT,
    Lean.Core.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Core.State,
    EIO,
    Lean.Exception,
    Lean.Meta.Simp.Step])),
 (CharTwo.add_self_eq_zero, (6513, [HAdd.hAdd, *, *, *, *, *, *])),
 (Subgroup.forall_zpowers, (6277, [→])),
 (AddSubgroup.forall_zmultiples, (6277, [→])),
 (Prod.snd_ofNat, (3337, [Prod.1, *])),
 (List.mem_of_find?_eq_some, (3127, [Membership.mem, *, List, *, *, *, *])),
 (Prod.fst_ofNat, (3009, [Prod.0, *])),
 (CategoryTheory.Limits.IsZero.map, (2910, [Prefunctor.1, *, *, *, CategoryTheory.Functor.0, *])),
 (le_one_iff_eq_one, (2850, [LE.le, *, *, *, 1])),
 (Finset.sum_pi_single, (2118, [Finset.sum, *, *, *, *, ◾])),
 (Nat.ofNat_pos', (2021, [LT.lt, *, *, 0, *])),
 (Module.isTorsionBySet_singleton_iff, (1764, [→])),
 (Set.setOf_bot, (1713, [setOf, *, ◾])),
 (Set.setOf_top, (1672, [setOf, *, ◾])),
 (Set.sep_setOf, (1644, [setOf, *, ◾])),
 (Set.sep_union, (1247, [setOf, *, ◾])),
 (Set.sep_inter, (1247, [setOf, *, ◾])),
 (IsAddUnit.add_neg_cancel, (1147, [HAdd.hAdd, *, *, *, *, *, Neg.neg, *, *, *])),
 (Set.biUnion_and, (1078, [Set.iUnion, *, *, ◾])),
 (Set.biUnion_self, (1070, [Set.iUnion, *, *, ◾])),
 (Nat.ofNat_nonneg', (1049, [LE.le, *, *, 0, *])),
 (bot_eq_one', (1021, [Bot.bot, *, *])),
 (Set.biUnion_preimage_singleton, (1006, [Set.iUnion, *, *, ◾])),
 (mul_div_cancel_of_invertible, (958, [HDiv.hDiv, *, *, *, *, HMul.hMul, *, *, *, *, *, *, *])),
 (Bool.cond_self, (935, [cond, *, *, *, *])),
 (Polynomial.coeff_ofNat_succ, (931, [Polynomial.coeff, *, *, *, *])),
 (div_mul_cancel_right, (931, [HDiv.hDiv, *, *, *, *, *, HMul.hMul, *, *, *, *, *, *])),
 (div_mul_cancel_left, (931, [HDiv.hDiv, *, *, *, *, *, HMul.hMul, *, *, *, *, *, *])),
 (right_eq_mul₀, (867, [Eq, *, *, HMul.hMul, *, *, *, *, *, *])),
 (left_eq_mul₀, (867, [Eq, *, *, HMul.hMul, *, *, *, *, *, *])),
 (eq_self_iff_true, (822, [Eq, *, *, *])),
 (IsAddUnit.neg_add_cancel, (807, [HAdd.hAdd, *, *, *, *, Neg.neg, *, *, *, *])),
 (Finsupp.univ_sum_single_apply', (806, [Finset.sum, *, *, *, Finset.univ, *, *, ◾])),
 (Int.neg_eq_of_add_eq_zero, (788, [Neg.neg, Int, *, *])),
 (Set.biInter_and, (770, [Set.iInter, *, *, ◾])),
 (Int.reduceGT,
  (756,
   [ReaderT,
    _private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.MethodsRef,
    ReaderT,
    Lean.Meta.Simp.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Meta.Simp.State,
    ReaderT,
    Lean.Meta.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Meta.State,
    ReaderT,
    Lean.Core.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Core.State,
    EIO,
    Lean.Exception,
    Lean.Meta.Simp.Step])),
 (Int.reduceLT,
  (756,
   [ReaderT,
    _private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.MethodsRef,
    ReaderT,
    Lean.Meta.Simp.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Meta.Simp.State,
    ReaderT,
    Lean.Meta.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Meta.State,
    ReaderT,
    Lean.Core.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Core.State,
    EIO,
    Lean.Exception,
    Lean.Meta.Simp.Step])),
 (le_mul_iff_one_le_left', (734, [LE.le, *, *, *, HMul.hMul, *, *, *, *, *, *])),
 (Set.iUnion_Icc_left, (730, [Set.iUnion, *, *, ◾])),
 (Set.iUnion_Ioo_left, (730, [Set.iUnion, *, *, ◾])),
 (Set.iUnion_Ico_left, (730, [Set.iUnion, *, *, ◾])),
 (Set.iUnion_Ioc_left, (730, [Set.iUnion, *, *, ◾])),
 (le_mul_iff_one_le_left, (692, [LE.le, *, *, *, HMul.hMul, *, *, *, *, *, *])),
 (CategoryTheory.MonoidalCoherence.hom, (665, [Quiver.Hom, *, *, *, *])),
 (Set.iUnion_neg_vadd, (655, [Set.iUnion, *, *, ◾])),
 (Set.iUnion_op_vadd_set, (655, [Set.iUnion, *, *, ◾])),
 (Set.iUnion_vadd_set, (655, [Set.iUnion, *, *, ◾])),
 (Set.iUnion_op_smul_set, (655, [Set.iUnion, *, *, ◾])),
 (Int.reduceNe,
  (651,
   [ReaderT,
    _private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.MethodsRef,
    ReaderT,
    Lean.Meta.Simp.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Meta.Simp.State,
    ReaderT,
    Lean.Meta.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Meta.State,
    ReaderT,
    Lean.Core.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Core.State,
    EIO,
    Lean.Exception,
    Lean.Meta.Simp.Step])),
 (map_eq_zero_iff_eq_zero, (631, [Eq, *, DFunLike.coe, *, *, *, *, *, *, 0])),
 (map_eq_zero_iff_eq_one, (631, [Eq, *, DFunLike.coe, *, *, *, *, *, *, 0])),
 (CategoryTheory.Monoidal.transportStruct_whiskerLeft,
  (628, [CategoryTheory.MonoidalCategoryStruct.whiskerLeft, *, *, *, *, *, *, *])),
 (CategoryTheory.Monoidal.transportStruct_whiskerRight,
  (609, [CategoryTheory.MonoidalCategoryStruct.whiskerRight, *, *, *, *, *, *, *])),
 (not_uncountable, (606, [Uncountable, *])),
 (Nat.not_even_bit1, (598, [Even, Nat, *, *])),
 (Finset.prod_dite_eq', (596, [Finset.prod, *, *, *, *, ◾])),
 (Finset.prod_dite_eq, (596, [Finset.prod, *, *, *, *, ◾])),
 (Finset.prod_dite_irrel, (594, [Finset.prod, *, *, *, *, ◾])),
 (Finset.prod_ite_irrel, (594, [Finset.prod, *, *, *, *, ◾])),
 (Denumerable.ofNat_of_decode, (561, [Denumerable.ofNat, *, *, *])),
 (one_le, (542, [LE.le, *, *, 1, *])),
 (Finset.prod_inv_distrib, (527, [Finset.prod, *, *, *, *, ◾])),
 (IsAddUnit.add_sub_cancel_right, (524, [HSub.hSub, *, *, *, *, HAdd.hAdd, *, *, *, *, *, *, *])),
 (mul_le_iff_le_one_left', (522, [LE.le, *, *, HMul.hMul, *, *, *, *, *, *, *])),
 (commutatorElement_self, (514, [Bracket.bracket, *, *, *, *, *])),
 (Fin.reduceNe,
  (514,
   [ReaderT,
    _private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.MethodsRef,
    ReaderT,
    Lean.Meta.Simp.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Meta.Simp.State,
    ReaderT,
    Lean.Meta.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Meta.State,
    ReaderT,
    Lean.Core.Context,
    StateRefT',
    IO.RealWorld,
    Lean.Core.State,
    EIO,
    Lean.Exception,
    Lean.Meta.Simp.Step])),
 (MonoidHom.CompTriple.comp_assoc, (480, [MonoidHom.CompTriple, *, *, *, *, *, *, *, *, *])),
 (Nat.exists_ne_zero, (464, [Exists, Nat, ◾])),
 (mul_le_iff_le_one_left, (461, [LE.le, *, *, HMul.hMul, *, *, *, *, *, *, *])),
 (lt_mul_iff_one_lt_left', (448, [LT.lt, *, *, *, HMul.hMul, *, *, *, *, *, *])),
 (lt_mul_iff_one_lt_right', (448, [LT.lt, *, *, *, HMul.hMul, *, *, *, *, *, *])),
 (not_countable, (446, [Countable, *])),
 (lt_mul_iff_one_lt_right, (446, [LT.lt, *, *, *, HMul.hMul, *, *, *, *, *, *])),
 (lt_mul_iff_one_lt_left, (446, [LT.lt, *, *, *, HMul.hMul, *, *, *, *, *, *]))]

[Matthew Ballard]

That certainly helps with the heuristics for the simp key linter

[Violeta Hernández]

Yeesh, one of my theorems got second place

[Violeta Hernández]

I can see how it happened though, that should absolutely not have been a simp lemma

[Violeta Hernández]

I'll fix pronto

[Henrik Böving]

And now we can have 3 PRs that remove simp tags!

[Violeta Hernández]

#15721

[Tomas Skrivan]

Once I noticed that lots of the theorems that often fail to unify contain binders which are not keyed properly by Lean's DiscrTree e.g. all those forall_* theorems. If people want to have these as simp theorems I would recommend merging the RefinedDiscrTree PR #11968 and implementing custom simproc applying these theorems.

[Matthew Ballard]

Analogous instance information otw

[Matthew Ballard]

TIL: trying to write to the environment inside docs#Lean.Meta.synthInstance hits unreachable code.

[Matthew Ballard]

(Well, actually yesterday I learned)

[Matthew Ballard]

Matthew Ballard said:

Analogous instance information otw

Maybe not. Certain files overflow the stack with their abundance of instances attempted.

[Matthew Ballard]

Too many instances attempted in

Mathlib.Algebra.Star.NonUnitalSubalgebra
Mathlib.Algebra.Module.LocalizedModule
Mathlib.LinearAlgebra.SesquilinearForm
Mathlib.Analysis.Convex.Segment

[Matthew Ballard]

Henrik Böving said:

And now we can have 3 PRs that remove simp tags!

More! Some predate this weekend :) #15631 is pretty straight forward: when you are in characteristic two or zero and use facts dependent on those settings you really need to be clear about it.

[Jireh Loreaux]

@Frédéric Dupuis and I were lamenting instance issues in the Star hierarchy. We've guessed that everything there is too unbundled.

[Matthew Ballard]

#14477 disconnects bundled ordered algebra classes from Star.NonUnitalSubalgebra.

[Matthew Ballard]

lean#5019 is an RFC for global diagnostics. Please :+1: if you feel inclined.

[Kim Morrison]

#16175 turns off some of the worst simp lemmas

[Kim Morrison]

and lean#5180

[Yaël Dillies]

@Yury G. Kudryashov flagged docs#PSigma.exists' as a potential lemma that's always tried in https://github.com/leanprover-community/mathlib4/pull/16322#discussion_r1740972375

[Kim Morrison]

I can't find PSigma.exists'?

[Yury G. Kudryashov]

It got renamed back to docs#PSigma.exists

[Matthew Ballard]

The keys are @Exists (@Sigma _ _) _ so I think this is fine. Compare to (de-simped) docs@Sigma.forall with keys →.

[Yaël Dillies]

docs#PSigma.forall is still, though?

[Matthew Ballard]

It appears so

[Kim Morrison]

#16469

[Johan Commelin]

It would be useful in theory if simp could handle this lemma, right? Can the discrimination tree get special support for Pi types? (maybe not urgent)
Because the type does contain info to index on, about Sigma.

[Matthew Ballard]

It never actually unifies though (see above).

[Yuyang Zhao]

docs#tsub_eq_zero_of_le got worse in #17444. It seems that Lean is searching CanonicallyOrderedAdd for types that are not ordered at all, then doing some slow unification of instances with metavariables that is impossible to succeed.

[Yuyang Zhao]

I made a #mwe showing what's happening. (deleted) I made an incorrect #mwe.

[Yuyang Zhao]

(deleted)

[Yuyang Zhao]

No, it's not a correct #mwe... Lean thinks a and b are Nat.

[Yuyang Zhao]

Here's another #mwe that shows what's happening in mathlib now. OrderedSub is a mixin type class that requires LE, but Lean tries to synthesize an instance of OrderedSub without looking for LE.

import Mathlib

set_option trace.Meta.Tactic.simp true in
example {K : Type*} [Field K] (a b : NumberField.RingOfIntegers K) : a - b = 0 := by
  simp

/-
info: [Elab.command] [0.043274] example {K : Type*} [Field K] (a b : NumberField.RingOfIntegers K) : a - b = 0 := by simp
  [Elab.step] [0.016559] expected type: Sort ?u.21, term
      a - b = 0
    [Elab.step] [0.016545] expected type: Sort ?u.21, term
        binrel% Eq✝ (a - b) 0
  [Elab.step] [0.025065] simp
    [Elab.step] [0.025025] simp
      [Elab.step] [0.025012] simp
        [Meta.synthInstance] [0.018060] 💥️ OrderedSub (NumberField.RingOfIntegers K)
          [Meta.synthInstance] [0.018005] 💥️ apply @AddGroup.toOrderedSub to OrderedSub (NumberField.RingOfIntegers K)
            [Meta.synthInstance.tryResolve] [0.017959] 💥️ OrderedSub (NumberField.RingOfIntegers K) ≟ OrderedSub ?m.1133
              [Meta.isDefEq] [0.017951] 💥️ OrderedSub (NumberField.RingOfIntegers K) =?= OrderedSub ?m.1133
                [Meta.isDefEq] [0.011259] 💥️ AddCommMagma.toAdd =?= AddSemigroup.toAdd
                  [Meta.isDefEq] [0.011207] 💥️ AddSemigroup.toAdd =?= AddSemigroup.toAdd
                    [Meta.isDefEq.delta] [0.011190] 💥️ AddSemigroup.toAdd =?= AddSemigroup.toAdd
                      [Meta.isDefEq] [0.011138] 💥️ AddCommSemigroup.toAddSemigroup =?= AddMonoid.toAddSemigroup
                        [Meta.isDefEq] [0.011101] 💥️ AddMonoid.toAddSemigroup =?= AddMonoid.toAddSemigroup
                          [Meta.isDefEq.delta] [0.011086] 💥️ AddMonoid.toAddSemigroup =?= AddMonoid.toAddSemigroup
                            [Meta.isDefEq] [0.010325] 💥️ AddCommMonoid.toAddMonoid =?= SubNegMonoid.toAddMonoid
                              [Meta.isDefEq] [0.010181] 💥️ AddCommMonoid.toAddMonoid =?= AddCommMonoid.toAddMonoid
                                [Meta.isDefEq.delta] [0.010167] 💥️ AddCommMonoid.toAddMonoid =?= AddCommMonoid.toAddMonoid
                                  [Meta.isDefEq] [0.010124] 💥️ OrderedAddCommMonoid.toAddCommMonoid =?= NonUnitalNonAssocSemiring.toAddCommMonoid
-/

[Yuyang Zhao]

I've run into this problem again and noticed something suspicious.

import Mathlib.Computability.AkraBazzi.GrowsPolynomially

set_option trace.Meta.synthInstance true in
#synth NoZeroDivisors ℝ

/-
[Meta.synthInstance] ✅️ NoZeroDivisors ℝ ▼
  [] new goal NoZeroDivisors ℝ ▶
  [] ✅️ apply Subsingleton.to_noZeroDivisors to NoZeroDivisors ℝ ▶
  [] ❌️ apply instSubsingleton to Subsingleton ℝ ▶
  [] ✅️ apply @Unique.instSubsingleton to Subsingleton ℝ ▶
  [] ✅️ apply @IsEmpty.instSubsingleton to Subsingleton ℝ ▶
  [] ❌️ apply @CanonicallyOrderedCommSemiring.toNoZeroDivisors to NoZeroDivisors ℝ ▶
  [] ✅️ apply @LinearOrderedSemiring.noZeroDivisors to NoZeroDivisors ℝ ▶
  [] ✅️ apply @StarOrderedRing.toExistsAddOfLE to ExistsAddOfLE ℝ ▶
  [] ✅️ apply instStarRingReal to StarRing ℝ ▶
  [resume] propagating StarRing ℝ to subgoal StarRing ℝ of ExistsAddOfLE ℝ ▶
  [] ❌️ apply CanonicallyOrderedAddCommMonoid.existsAddOfLE to ExistsAddOfLE ℝ ▼
  [tryResolve] ❌️ ExistsAddOfLE ℝ ≟ ExistsAddOfLE ?m.180 ▼
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ❌️ CanonicallyOrderedAddCommMonoid ℝ ▶
  [] ✅️ apply AddGroup.existsAddOfLE to ExistsAddOfLE ℝ ▶
  [resume] propagating ExistsAddOfLE ℝ to subgoal ExistsAddOfLE ℝ of NoZeroDivisors ℝ ▶
  [] result LinearOrderedSemiring.noZeroDivisors
-/

[Yuyang Zhao]

In #17444 this becomes 200 lines of [] ❌️ IdemSemiring ℝ ▶.

[Yuyang Zhao]

I think it's lean4#2055. Is this still enough to cause the performance change in #17512?

[Kevin Buzzard]

Because of caching (I guess), this still only takes 300 heartbeats.