!4#4183 `simps` maximum recursion depth

Stream: mathlib4

[Jireh Loreaux]

@Floris van Doorn would you mind having a look at the simps problem present in !4#4183? I have temporarily worked around the problem by adding the simp lemmas manually, but it would be good to understand the issue here and I'm out of ideas. The problem is mentioned in the PR comment and as porting notes in the file.

[Floris van Doorn]

I found time to investigate this. The error occurs at the declaration

@[simps! (config := { fullyApplied := false }) apply symm_apply]
def addEquivBoundedOfCompact [AddMonoid β] [LipschitzAdd β] : C(α, β) ≃+ (α →ᵇ β) :=
  ({ toContinuousMapAddHom α β, (equivBoundedOfCompact α β).symm with } : (α →ᵇ β) ≃+ C(α, β)).symm

The behavior of simps! is to call dsimp; simp to simplify the resulting right-hand sides of the generated simp-lemmas. After minimizing the RHS a little bit, we get the following mwe, which indeed loops:

import Mathlib.Topology.ContinuousFunction.Compact

open BoundedContinuousFunction

variable {α β : Type _} [TopologicalSpace α] [CompactSpace α] [MetricSpace β]
   [AddMonoid β] [LipschitzAdd β]
set_option trace.Debug.Meta.Tactic.simp true
set_option maxRecDepth 100
example :
  (({ toEquiv := (ContinuousMap.equivBoundedOfCompact α β).symm,
      map_add' := (BoundedContinuousFunction.toContinuousMapAddHom α β).map_add } : _ ≃+ _).invFun :
        C(α, β) → α →ᵇ β) = sorry := by
  dsimp -- max recursion depth reached

Looking at the simp trace, the problem is the lemma docs4#AddEquiv.symm_mk

theorem symm_mk (f : M ≃ N) (h) :
  (MulEquiv.mk f h).symm = ⟨f.symm, (MulEquiv.mk f h).symm.map_mul'⟩ := rfl

It makes sense that this simp-lemma causes loops, since the right-hand side contains the left-hand side as a subexpression! I'm surprised we don't have a linter that catches this.
We should remove this simp-lemma from the simp-set.

[Yaël Dillies]

Hmm... That wasn't the case in mathlib, was it? Why is it rewriting the proof?

[Yaël Dillies]

And certainly this simp lemma is useful.

[Yaël Dillies]

If nothing else can save it, turn (MulEquiv.mk h).symm.map_mul' into a private lemma and use it using symm_mk.

[Reid Barton]

Does (d)simp really simplify inside proofs?

[Matthew Ballard]

Did anything come of this discussion? I just ran into the mul version :/

[Floris van Doorn]

I opened #7407 as a temporary fix. We should either make sure that simp doesn't rewrite inside propositions, finds that it loops in this case, or add a linter that guards against lemmas like this.