bad simp discrimination tree keys

Stream: mathlib4

[Kevin Buzzard]

Props to @Jovan Gerbscheid who, in a one-line PR #21329 , did this:

+ ~Mathlib.Algebra.Homology.BifunctorShift                        instructions   -39.2%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit      instructions   -52.2%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift      instructions   -25.1%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated      instructions   -32.1%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.Shift                instructions   -26.4%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence        instructions   -45.0%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors       instructions   -41.4%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.Triangulated         instructions   -30.7%
+ ~Mathlib.Algebra.Homology.TotalComplexShift                     instructions   -30.6%
+ ~Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated   instructions   -26.3%

The "unfavourable discrimination tree key" he mentions in the PR description is

#discr_tree_key CategoryTheory.shiftFunctor_of_induced
-- @Eq (CategoryTheory.Functor _ _ _ _) (CategoryTheory.shiftFunctor _ _ _ _ _ _) _

Thanks also to the person who wrote #discr_tree_key because it's the only tool I have to understand what people are talking about when they talk about discrimination trees.

My question is: how many other simp lemmas are there out there with "unfavourable discrimination tree key" s and how much more of a speedup can we win by finding them and removing @[simp] from them?

[Matthew Ballard]

You want #discr_tree_simp_key for simp theorems.

I’ve thought about a broader search over the environment using the keys but what are the criteria to filter by?

[Jovan Gerbscheid]

Two things that could be done:

• check for simp lemmas where the #discr_tree_simp_key has the form foo _ _ _ _ _
• keep track of how much simp time is spent on failing, on a lemma-per-lemma basis.

[Jovan Gerbscheid]

However the form foo _ _ _ _ isn't the only bad form. I also stumbled upon LinearMap.map_coe_ker, which has the key@DFunLike.coe _ _ _ _ _ _.1 (where the .1 is a projection on a subtype). This is also too general.

But that lemma is actually used so maybe scoping it would be a better middleground.

[Matthew Ballard]

How bad the first is overall depends a lot on foo and its ubiquity.

[Matthew Ballard]

Do we have a metric for this though?

[Jovan Gerbscheid]

It's not too hard to go through the types of each declaration and determine which constants appear there. Then each constant has a count of how many declarations use it. So I guess we can use that for a metric.

[Matthew Ballard]

I’ve done (or at least tried) the second. There’s a thread here with my results. My approach through an environment extension to store things didn’t comport with the ongoing parallelization work though

[Matthew Ballard]

Jovan Gerbscheid said:

It's not too hard to go through the types of each declaration and determine which constants appear there. Then each constant has a count of how many declarations use it. So I guess we can use that for a metric.

I’d be interested to see this regardless

[Matthew Ballard]

If someone wants to hunt for things with bad keys this might be a good place to look.

[Jovan Gerbscheid]

I made some code to check for keys of the form foo _ _ _ _, but it turns out there are way too many lemmas like this to check them one by one. However, what I did find out is that there are simp lemmas which have the form (fun _ => _) = _, and this is a very bad form of lemmas, because the discrimination tree key of a lambda expression is just <other>. Here's the quick code I used:

import Mathlib

open Lean Meta

open Batteries Tactic Lint

private def mkKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
  let (_, _, type) ← withReducible <| forallMetaTelescopeReducing e
  let type ← whnfR type
  withSimpGlobalConfig do
    if let some (_, lhs, _) := type.eq? then
      DiscrTree.mkPath lhs
    else if let some (lhs, _) := type.iff? then
      DiscrTree.mkPath lhs
    else if let some (_, lhs, _) := type.ne? then
      DiscrTree.mkPath lhs
    else if let some p := type.not? then
      match p.eq? with
      | some (_, lhs, _) =>
        DiscrTree.mkPath lhs
      | _ => DiscrTree.mkPath p
    else
      DiscrTree.mkPath type

def isBadKeys (keys: Array DiscrTree.Key) : MetaM Bool := do
  for key in keys[1:] do
    if !(key matches .star) then
      return false
  return true

@[env_linter] def simpNF' : Lint.Linter where
  noErrorsFound := "NOTHING"
  errorsFound := "FOUND SOME!"
  test := fun declName => do
    unless ← isSimpTheorem declName do return none
    let e := (← getConstInfo declName).type
    let keys ← mkKey e
    unless ← isBadKeys keys do return none

    return m!"{e} might be a bad lemma. It has keys {keys}"

#lint only simpNF' in all

[Jovan Gerbscheid]

And here are the offending lemmas:

-- Init.Data.Array.Lemmas
Array.filterMap_eq_map /- ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
  (fun as => Array.filterMap (some ∘ f) as) = Array.map f -/
Array.filterMap_eq_filter /- ∀ {α : Type u_1} (p : α → Bool),
  (fun as => Array.filterMap (Option.guard fun x => p x = true) as) = fun as =>
    Array.filter p as -/

-- Mathlib.Analysis.Fourier.AddCircle
coe_fourierBasis /- ∀ {T : ℝ} [hT : Fact (0 < T)],
  (fun i => fourierBasis.repr.symm (lp.single 2 i 1)) = fourierLp 2 -/

-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.coe_mFourierBasis /- ∀ {d : Type u_1} [inst : Fintype d],
  (fun i => UnitAddTorus.mFourierBasis.repr.symm (lp.single 2 i 1)) =
    UnitAddTorus.mFourierLp 2 -/

-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.coe_mk /- ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {v : ι → E}
  (hv : Orthonormal 𝕜 v) (hsp : ⊤ ≤ (Submodule.span 𝕜 (Set.range v)).topologicalClosure),
  (fun i => (HilbertBasis.mk hv hsp).repr.symm (lp.single 2 i 1)) = v -/
HilbertBasis.coe_mkOfOrthogonalEqBot /- ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {v : ι → E}
  (hv : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥),
  (fun i => (HilbertBasis.mkOfOrthogonalEqBot hv hsp).repr.symm (lp.single 2 i 1)) =
    v -/
OrthonormalBasis.coe_toHilbertBasis /- ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] [inst_4 : Fintype ι]
  (b : OrthonormalBasis ι 𝕜 E),
  (fun i => b.toHilbertBasis.repr.symm (lp.single 2 i 1)) = ⇑b -/

-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.map_apply /- ∀ {α : Type u_5} {α' : Type u_6} {ι : Type u_7} (f : α → α')
  (l : Combinatorics.Line α ι) (x : α),
  (fun x i => ((Combinatorics.Line.map f l).idxFun i).getD x) (f x) =
    f ∘ (fun x i => (l.idxFun i).getD x) x -/
Combinatorics.Line.vertical_apply /- ∀ {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (v : ι → α)
  (l : Combinatorics.Line α ι') (x : α),
  (fun x i => ((Combinatorics.Line.vertical v l).idxFun i).getD x) x =
    Sum.elim v ((fun x i => (l.idxFun i).getD x) x) -/
Combinatorics.Line.horizontal_apply /- ∀ {α : Type u_5} {ι : Type u_6} {ι' : Type u_7}
  (l : Combinatorics.Line α ι) (v : ι' → α) (x : α),
  (fun x i => ((l.horizontal v).idxFun i).getD x) x =
    Sum.elim ((fun x i => (l.idxFun i).getD x) x) v -/
Combinatorics.Line.prod_apply /- ∀ {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (l : Combinatorics.Line α ι)
  (l' : Combinatorics.Line α ι') (x : α),
  (fun x i => ((l.prod l').idxFun i).getD x) x =
    Sum.elim ((fun x i => (l.idxFun i).getD x) x)
      ((fun x i => (l'.idxFun i).getD x) x) -/
Combinatorics.Line.diagonal_apply /- ∀ {α : Type u_5} {ι : Type u_6} [inst : Nonempty ι] (x : α),
  (fun x i => ((Combinatorics.Line.diagonal α ι).idxFun i).getD x) x = fun x_1 =>
    x -/

-- Mathlib.Data.Fin.VecNotation
Matrix.empty_val' /- ∀ {α : Type u} {n' : Type u_1} (j : n'),
  (fun i => ![] i j) = ![] -/

[Jovan Gerbscheid]

There should definitely be a linter warning about simp lemmas with a lambda as the head symbol, because all of these simp lemmas are attempted every time when there is a lambda.

[Kim Morrison]

Jovan Gerbscheid said:

-- Init.Data.Array.Lemmas
Array.filterMap_eq_map /- ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
  (fun as => Array.filterMap (some ∘ f) as) = Array.map f -/
Array.filterMap_eq_filter /- ∀ {α : Type u_1} (p : α → Bool),
  (fun as => Array.filterMap (Option.guard fun x => p x = true) as) = fun as =>
    Array.filter p as -/

Fixed.

[Kim Morrison]

This linter seems like a great idea. Could you PR it to Batteries?

[Kim Morrison]

I'll clean up the rest of this report, it looks like most of them can just be dropped.

[Jovan Gerbscheid]

Kim Morrison said:

This linter seems like a great idea. Could you PR it to Batteries?

I've made a PR to lean (lean#6936) that marks the relevant function as public, so that I can then use it in a linter in Batteries. Nevermind, I can use the same machinery as simpVarHead and simpNF

[Kim Morrison]

#21395

[Yaël Dillies]

Jovan Gerbscheid said:

-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.map_apply /- ∀ {α : Type u_5} {α' : Type u_6} {ι : Type u_7} (f : α → α')
  (l : Combinatorics.Line α ι) (x : α),
  (fun x i => ((Combinatorics.Line.map f l).idxFun i).getD x) (f x) =
    f ∘ (fun x i => (l.idxFun i).getD x) x -/
Combinatorics.Line.vertical_apply /- ∀ {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (v : ι → α)
  (l : Combinatorics.Line α ι') (x : α),
  (fun x i => ((Combinatorics.Line.vertical v l).idxFun i).getD x) x =
    Sum.elim v ((fun x i => (l.idxFun i).getD x) x) -/
Combinatorics.Line.horizontal_apply /- ∀ {α : Type u_5} {ι : Type u_6} {ι' : Type u_7}
  (l : Combinatorics.Line α ι) (v : ι' → α) (x : α),
  (fun x i => ((l.horizontal v).idxFun i).getD x) x =
    Sum.elim ((fun x i => (l.idxFun i).getD x) x) v -/
Combinatorics.Line.prod_apply /- ∀ {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (l : Combinatorics.Line α ι)
  (l' : Combinatorics.Line α ι') (x : α),
  (fun x i => ((l.prod l').idxFun i).getD x) x =
    Sum.elim ((fun x i => (l.idxFun i).getD x) x)
      ((fun x i => (l'.idxFun i).getD x) x) -/
Combinatorics.Line.diagonal_apply /- ∀ {α : Type u_5} {ι : Type u_6} [inst : Nonempty ι] (x : α),
  (fun x i => ((Combinatorics.Line.diagonal α ι).idxFun i).getD x) x = fun x_1 =>
    x -/

#21405

[Yaël Dillies]

Jovan Gerbscheid said:

-- Mathlib.Analysis.Fourier.AddCircle
coe_fourierBasis /- ∀ {T : ℝ} [hT : Fact (0 < T)],
  (fun i => fourierBasis.repr.symm (lp.single 2 i 1)) = fourierLp 2 -/

-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.coe_mFourierBasis /- ∀ {d : Type u_1} [inst : Fintype d],
  (fun i => UnitAddTorus.mFourierBasis.repr.symm (lp.single 2 i 1)) =
    UnitAddTorus.mFourierLp 2 -/

-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.coe_mk /- ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {v : ι → E}
  (hv : Orthonormal 𝕜 v) (hsp : ⊤ ≤ (Submodule.span 𝕜 (Set.range v)).topologicalClosure),
  (fun i => (HilbertBasis.mk hv hsp).repr.symm (lp.single 2 i 1)) = v -/
HilbertBasis.coe_mkOfOrthogonalEqBot /- ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {v : ι → E}
  (hv : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥),
  (fun i => (HilbertBasis.mkOfOrthogonalEqBot hv hsp).repr.symm (lp.single 2 i 1)) =
    v -/
OrthonormalBasis.coe_toHilbertBasis /- ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] [inst_4 : Fintype ι]
  (b : OrthonormalBasis ι 𝕜 E),
  (fun i => b.toHilbertBasis.repr.symm (lp.single 2 i 1)) = ⇑b -/

Now also fixed in #21405

[Matthew Ballard]

but it turns out there are way too many lemmas like this to check them one by one.

Yeah, this is was why I was getting a filtering heuristic. You can argue that anything of this shape is bad but the practical effect is negligible when foo is rarely used.

You see that with the lambdas at the heads. Not a good idea in general but the practical effect is small compared to other situations.

[Matthew Ballard]

Jovan Gerbscheid said:

Nevermind, I can use the same machinery as simpVarHead and simpNF

If things weren't private in the simp processing, that would be optimal. You could reuse the same things that are actually used instead of cribbing them (and setting those to private because you cribbed them) like in the implementation of #discr_tree_key.

[Jannis Limperg]

Can open private be used to get the private defs? It's a hack, but it's better than copy-and-paste.

[Jovan Gerbscheid]

Yes, I hadn't though of that before

[Matthew Ballard]

Where is that? I thought it was batteries

[Matthew Ballard]

Yes docs#Lean.Elab.Command.elabOpenPrivate. Maybe too implicit in what I said was that I was working in core. If you are importing batteries, then I think this is ok.

[Matthew Ballard]

Yes docs#Lean.Elab.Command.elabOpenPrivate. Maybe too implicit in what I said was that I was working in core. If you are importing batteries, then I think this is ok.

[Jovan Gerbscheid]

I also tried linting for simp lemmas that simplify proofs (and hence don't usually apply). These seem to all originate from the @[simps!] tag. All of these failed the simpNF test when I tried fixing lean#6960. Here are the offending lemmas:

-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.AffineOpenCover.openCover_covers

-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.compFunctor_map_down_down

-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_inverse_obj_hom_down_down
CategoryTheory.Comma.toPUnitIdEquiv_unitIso_inv_app_right_down_down
CategoryTheory.Comma.toPUnitIdEquiv_inverse_map_right_down_down
CategoryTheory.Comma.toPUnitIdEquiv_inverse_obj_hom_down_down
CategoryTheory.Comma.toPUnitIdEquiv_unitIso_hom_app_right_down_down
CategoryTheory.Comma.toIdPUnitEquiv_inverse_map_left_down_down
CategoryTheory.Comma.toIdPUnitEquiv_unitIso_inv_app_left_down_down
CategoryTheory.Comma.toIdPUnitEquiv_unitIso_hom_app_left_down_down
CategoryTheory.Comma.toIdPUnitEquiv_inverse_obj_hom_down_down

-- Mathlib.CategoryTheory.Comma.Over
CategoryTheory.Over.postComp_inv_app_right_down_down
CategoryTheory.Over.postComp_hom_app_right_down_down
CategoryTheory.Over.postCongr_inv_app_right_down_down
CategoryTheory.Over.postCongr_hom_app_right_down_down
CategoryTheory.Under.postComp_hom_app_left_down_down
CategoryTheory.Under.postComp_inv_app_left_down_down
CategoryTheory.Under.postCongr_inv_app_left_down_down
CategoryTheory.Under.postCongr_hom_app_left_down_down
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_right_left_down_down
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_map_left_down_down
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_left_down_down
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse_map_right_left_down_down
CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_map_left_down_down
CategoryTheory.StructuredArrow.ofDiagEquivalence.functor_map_right_left_down_down
CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse_map_left_down_down
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_map_left_down_down
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_map_right_down_down
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor_map_left_right_down_down
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_map_right_down_down
CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse_map_left_right_down_down
CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_map_left_right_down_down
CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_map_right_down_down
CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_map_right_down_down
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_map_right_down_down

-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceFunctor_map_left_down_down
CategoryTheory.StructuredArrow.preEquivalenceInverse_map_left_down_down
CategoryTheory.StructuredArrow.preEquivalenceInverse_map_right_left_down_down
CategoryTheory.StructuredArrow.preEquivalenceInverse_obj_hom_left_down_down
CategoryTheory.CostructuredArrow.preEquivalence.functor_map_right_down_down
CategoryTheory.CostructuredArrow.preEquivalence.inverse_map_right_down_down
CategoryTheory.CostructuredArrow.preEquivalence.inverse_obj_hom_right_down_down
CategoryTheory.CostructuredArrow.preEquivalence.inverse_map_left_right_down_down

-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_inv_app_left_down_down
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_hom_app_left_down_down
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_left_left_down_down
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_left_left_down_down
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_hom_app_right_left_down_down
CategoryTheory.StructuredArrow.commaMapEquivalenceCounitIso_inv_app_right_left_down_down

-- Mathlib.CategoryTheory.PUnit
CategoryTheory.Functor.star_map_down_down
CategoryTheory.Functor.punitExt_inv_app_down_down
CategoryTheory.Functor.punitExt_hom_app_down_down

-- Mathlib.Topology.Sheaves.MayerVietoris
Opens.mayerVietorisSquare_f₁₂_down_down
Opens.mayerVietorisSquare_f₂₄_down_down
Opens.mayerVietorisSquare_f₃₄_down_down
Opens.mayerVietorisSquare_f₁₃_down_down

[Matthew Ballard]

Is there an easy fix in simps!?

[Jovan Gerbscheid]

The underlying issue is that the PLift.down field is universe polymorphic, so it can be a proposition or a type, so when simps checks if this is a proposition, it gets a negative result. So this can be fixed by either using a non-universe polymorphic version of PLift, or fixing simps. In #21578, I've added another isProof check at the point in simps where the universe levels get instantiated. This solves the problem.

[Jovan Gerbscheid]

Another bad simp lemma was added in core recently: Std.ReflCmp.compare_self, which has a metavariable as the head (so it is tried everywhere). I hope this one doesn't make it to the next release :)
lean4#7218

[Jovan Gerbscheid]

Another bad simp lemma has appeared: docs#Option.elim_none_some applies on every lambda.

[Yaël Dillies]

That's because Option.elim should take its Option argument last

[Jovan Gerbscheid]

Right, or it has to be stated as

x.elim (f none) (f ∘ some)) = f x

[Jovan Gerbscheid]

There is Option.elim' which has the argument order you suggest. Did you want to remove the current Option.elim altogether?

[Jovan Gerbscheid]

Oh and Option.casesOn' is a copy of Option.elim, and they have different simp lemmas. Surely that can't be a good state of affairs?

[Yury G. Kudryashov]

Yes, @Yaël Dillies suggests we remove Option.elim and replace it with Option.elim', see discussions in #15448 and lean4#5096

[Jovan Gerbscheid]

Nice, but that will not be solved soon, so what do we do with the lemma, unsimp it, change the definition to avoid the lambda, or change it to Option.elim'?

[Yury G. Kudryashov]

I suggest that for now we leave 2 versions of the lemma:

• fully applied with Option.elim
• partially applied with Option.elim'.

[Jovan Gerbscheid]

#22985