feat(tactic/tidy): limit the amount of time spent on refl

[semorrison]

I have mixed feelings about refl in tidy.

On the one hand, including it near the top of default_tactics list (as it is now) saves about 60s in compiling mathlib.

On the other hand, it potentially makes tidy very slow, as it is willing to tackle "heavy rfl" problems, even when other tactics would be more advisable.

As a compromise, in this PR we run refl inside a try_for wrapper.
The time limit was chosen as a smallest value for which we get the full compilation time benefits
(in fact a slight overall improvement).

This PR also

1. replaces the unique proof by tidy that fails if refl is removed entirely
2. satisfies the linter on tactic/tidy.lean

---

[semorrison]

This proof still works by tidy and could be omitted, but the whole declaration is up against the -T100000 limit, and now apparently slightly over, so I've put the map_comp proof in by hand.

It would be better to improve the simp lemmas so this refl isn't even needed, but not today.

[gebner]

I am very uneasy about this change.

In my experience it only needs one small and unrelated change to push the 49 to 51, and then some definitions in the category theory library will fail in a completely unclear way. Even worse, tidy is used extensively in auto params so the failure is even more mysterious.

What is the debugging story here? Is there a tracing option that gives some information about how tidy fails and what to do to make it work?

Ideally we'd also have an option to specify the refl timeout.

[semorrison]

The one (very weak) counter argument, is that you can actually remove refl entirely from the list of tidy tactics, and everything still compiles (just a bit slower).

I agree this is not a satisfactory answer to your objection!

[semorrison]

Nevertheless I think a reasonable solution may be to just remove refl. It will cost us a slight slow down, but apparently make tidy more useful.

[semorrison]

Let me #xy the problem:

import algebra.category.CommRing.basic
import data.polynomial

noncomputable theory

attribute [simp] polynomial.coeff_map

def CommRing.polynomial : CommRing ⥤ CommRing :=
{ obj := λ R, CommRing.of (polynomial R),
  map := λ R S f, ring_hom.of (polynomial.map f),
  map_comp' := λ R S T f g, by { ext, dsimp, simp, }, }

def CommRing.polynomial' : CommRing ⥤ CommRing :=
{ obj := λ R, CommRing.of (polynomial R),
  map := λ R S f, ring_hom.of (polynomial.map f),
  map_comp' := λ R S T f g, by { refl, }, } -- `refl` fails, but takes 12 seconds to do so!

This sort of slow failure of refl makes tidy completely unusable here. If we leave out refl from the list of tidy tactics it essentially reproduces the first proof, in a reasonable time.

[robertylewis]

I know nothing about the category theory library, but when I hear "refl takes 12 seconds to fail," I have to assume there's an @[irreducible] annotation missing somewhere.

[semorrison]

In fact, this proof with a slow refl is just about polynomials. Let me extract it better...

[semorrison]

Here's the further minimised slow refl failure, no category theory involved:

import data.polynomial

noncomputable theory

example {R S T : Type} [comm_ring R] [comm_ring S] [comm_ring T]
  (f : R →+* S)
  (g : S →+* T) :
  ring_hom.of (polynomial.map (g.comp f)) =
    (ring_hom.of (polynomial.map g)).comp (ring_hom.of (polynomial.map f)) :=
begin
  refl, -- `refl` fails, but takes 6 seconds to do so!
end

[gebner]

Any one of the following works:

attribute [irreducible] polynomial.eval₂  --  1ms
attribute [irreducible] finsupp.sum       --  1ms
attribute [irreducible] finset.sum        --  1ms
attribute [irreducible] multiset.map      -- 25ms

[semorrison]

I experimented with attribute [irreducible] polynomial.eval₂, and can get things to work, but I there are six different files where I need to add local attribute [semireducible] polynomial.eval₂ to get existing proofs to work.

Does it seem reasonable to do this? That is, make something irreducible, adding local attributes to make existing proofs work, and defer the real work of fixing those proofs to use a proper API for later? Or is this adding more technical debt, and it would be better to only mark things as [irreducible] if we fix all subsequent proofs at the same time?

[semorrison]

(I guess that this was going to be the cheapest change to make, out of those four.)

[gebner]

Does it seem reasonable to do this? That is, make something irreducible, adding local attributes to make existing proofs work, and defer the real work of fixing those proofs to use a proper API for later? Or is this adding more technical debt, and it would be better to only mark things as [irreducible] if we fix all subsequent proofs at the same time?

If possible, I think we should try to add enough API that we don't need local attribute [semireducible]. In cast that fails, I'd try to use sections to only change the reducibility for a single lemma. Do you have a branch with the changes somewhere?

[semorrison]

eval2_irreducible

[gebner]

eval2_irreducible

Thanks! That doesn't look so bad. I think some parts can be easily replaced by unfold eval₂ (or by rw eval₂_def which would be a bit more future-proof).

I heard on Zulip that somebody wanted to do a big refactor of the polynomials. Maybe it would be best to do this as part of the refactor.

[semorrison]

That was me... :-) But it keeps getting postponed!

I will close this for now.