congr' is slow

Stream: metaprogramming / tactics

[Floris van Doorn]

In the follow example congr' is very slow:

import measure_theory.outer_measure

open measure_theory measure_theory.outer_measure

variables {α : Type*}
set_option profiler true
example {m : set (outer_measure α)} {t : set α} :
  Inf m t =
    ⨅ (s : ℕ → set α) (h2 : t ⊆ ⋃ n, s n), ∑' n, ⨅ (μ : outer_measure α) (h3 : μ ∈ m), μ (s n) :=
begin
  rw [Inf_eq_of_function_Inf_gen, of_function_apply],
  congr',
  sorry
end

Almost all of the time is spent in relation_tactic

elaboration: tactic execution took 7.51s
 7296ms    97.2%   relation_tactic

@Simon Hudon any ideas why this is so slow?

[Simon Hudon]

How does it compare to congr?

[Simon Hudon]

Is of_function_apply a new function?

[Floris van Doorn]

Ah, congr is also slow.

[Floris van Doorn]

Sorry for that. I updated the example to work in the current master.

[Floris van Doorn]

congr and congr' both spend ~7s in relation_tactic.

[Simon Hudon]

Sounds like it's happening in refl

[Floris van Doorn]

I see, thanks for the investigation. I now see that adding

local attribute [irreducible] tsum

makes this instantaneous.

[Yury G. Kudryashov]

Should we add it as a global attribute?

[Floris van Doorn]

I think so. I'm not sure which of tsum, summable and has_sum should be made irreducible (any of them solves this issue).

[Floris van Doorn]

I wonder if we should also add a try_for around the offending refl in relation_tactic.

[Simon Hudon]

In your case the proof will fail if you do that

[Simon Hudon]

(btw, refl calls relation_tactic, not the other way around)

[Simon Hudon]

You might want to make the try_for optional. Otherwise, you're going to get weird breaking points where congr will work in some cases and then you wrap your definition into one more definition and it stops working.

[Floris van Doorn]

Ah, I see.

[Floris van Doorn]

congr doesn't fail if the refl fails, that is just something tried to close the goal. I'm thinking something like this:

import measure_theory.outer_measure

open measure_theory measure_theory.outer_measure

set_option profiler true

open tactic
meta def tactic.my_congr : tactic unit :=
do focus1 (try assumption >> congr_core >> all_goals' (try (try_for 1000 reflexivity) >> try congr))


example {α : Type*} {m : set (outer_measure α)} {t : set α} :
  (⨅ (f : ℕ → set α) (h : t ⊆ set.Union f), ∑' (n : ℕ), Inf_gen m (f n)) =
    ⨅ (f : ℕ → set α) (h2 : t ⊆ set.Union f), ∑' n, ⨅ (μ : outer_measure α) (h3 : μ ∈ m), μ (f n) :=
begin
  tactic.my_congr,
end

[Simon Hudon]

What's the error message you get?

[Floris van Doorn]

There is no error message, tactic.my_congr succeeds with exactly the same tactic state as congr', but gets there quicker. It tried to solve the goal by refl, but gave up.

[Simon Hudon]

I see. It gives up quicker. You can give it a low default and we can override it with an optional argument

[Floris van Doorn]

That's what I did. I just opened #4678 (no way to override the timeout interactively yet).

[Simon Hudon]

If you put it in a structure, you can call congr' as congr' 3 { timeout := 500 } or congr' 3 { timeout := none }

[Mario Carneiro]

why would you ever want to set the timeout to something other than 0 or infinity? in a given application either refl is useful or it isn't

[Mario Carneiro]

I think it would be better to just lower the transparency on that refl. It's only supposed to be cleaning up syntactic refl subgoals

[Mario Carneiro]

I don't like tactics which time out in real working code

[Simon Hudon]

I think the timeout is defensible. One extreme case would be to guard the use of refl with the condition that the lhs and rhs be alpha equivalent. That is very strict. I think we want to allow some unfolding. How much? One could say that we want as much as reducibility hints will allow but beyond a certain point, there's little hope that unfolding some more will yield any useful results.

[Simon Hudon]

An alternative to putting this kind of safeguard in congr' or other tactics would be to have a linter tell us when a definition allows too much unfolding. I don't know how to judge that though

[Mario Carneiro]

congr is not the place for heavy refls

[Mario Carneiro]

if you want a heavy refl, the only tactic that should do that is refl

[Mario Carneiro]

I think it's fine to have the "very strict" alpha equality here, because you can easily clean up the non-alpha equivalent subterms withrefl

[Mario Carneiro]

however if congr_core is already unfolding reducibles then there is no reason not to have the same level of unfolding in the refl before it

[Floris van Doorn]

I'm happy to replace the timeout by a "refl, but only unfold reducibles".

[Floris van Doorn]

I do feel like that would be breaking much more things than the timeout in mathlib, though.

[Floris van Doorn]

@Mario Carneiro: I tried a couple of options in #4678:

• try_for 1000 reflexivity passes on all of mathlib
• try_for 100 reflexivity fails for the first time in analysis/calculus/times_cont_diff
• reflexivity reducible fails for the first time in data/nat/basic

I think we are relying a lot on congr solving goals by unfolding semireducible definitions, so I don't think that is a good change.
I think we should go for the second option: there might be a couple of places where congr will now create an extra subgoal.

Should I also add an option to congr' that tells it to not use reflexivity?

[Mario Carneiro]

If it's a big job we can put it off, but I do think we should change the default behavior to be less aggressive, and introduce congr! to unfold semireducibles

[Mario Carneiro]

this is the sort of thing that deserves a marker in the source