Proposal

unlike simp, dsimp traverses subexpressions that are proofs, and simplifies them. This is very bad for performance, particularly in Category Theory, where aesop_cat uses simp, which uses dsimp, and this is run on the result of other aesop_cat tactic calls.

I propose that when encountering a proof, dsimp does one of two things:

• leave the proofs as-is, without simplification
• simplify the type of the proof and wrap the proof in a cast so that it gets the new type.

Minimal working example

@[simp]
theorem foo (i : Nonempty α) : Nonempty.intro (Classical.choice i) = i := rfl

set_option pp.proofs true

example : Classical.choice (Nonempty.intro (Classical.choice instNonemptyFloat)) = 0 := by
  dsimp

Expected behaviour: dsimp fails
Actual behaviour: dsimp applies the simp lemma

Community Feedback

I first suggested this on Zulip.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.