Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: congr' is slow


view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:01):

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?

view this post on Zulip Simon Hudon (Oct 18 2020 at 23:06):

How does it compare to congr?

view this post on Zulip Simon Hudon (Oct 18 2020 at 23:19):

Is of_function_apply a new function?

view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:25):

Ah, congr is also slow.

view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:33):

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

view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:33):

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

view this post on Zulip Simon Hudon (Oct 18 2020 at 23:40):

Sounds like it's happening in refl

view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:43):

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

local attribute [irreducible] tsum

makes this instantaneous.

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 23:45):

Should we add it as a global attribute?

view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:46):

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

view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:46):

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

view this post on Zulip Simon Hudon (Oct 18 2020 at 23:48):

In your case the proof will fail if you do that

view this post on Zulip Simon Hudon (Oct 18 2020 at 23:49):

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

view this post on Zulip Simon Hudon (Oct 18 2020 at 23:50):

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.

view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:55):

Ah, I see.

view this post on Zulip Floris van Doorn (Oct 18 2020 at 23:56):

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

view this post on Zulip Simon Hudon (Oct 19 2020 at 00:01):

What's the error message you get?

view this post on Zulip Floris van Doorn (Oct 19 2020 at 00:02):

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.

view this post on Zulip Simon Hudon (Oct 19 2020 at 00:04):

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

view this post on Zulip Floris van Doorn (Oct 19 2020 at 00:06):

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

view this post on Zulip Simon Hudon (Oct 19 2020 at 00:16):

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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 04:23):

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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 04:24):

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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 04:26):

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

view this post on Zulip Simon Hudon (Oct 19 2020 at 05:16):

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.

view this post on Zulip Simon Hudon (Oct 19 2020 at 05:18):

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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 05:21):

congr is not the place for heavy refls

view this post on Zulip Mario Carneiro (Oct 19 2020 at 05:21):

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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 05:22):

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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 05:22):

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

view this post on Zulip Floris van Doorn (Oct 19 2020 at 19:28):

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

view this post on Zulip Floris van Doorn (Oct 19 2020 at 19:29):

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

view this post on Zulip Floris van Doorn (Oct 19 2020 at 20:20):

@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?

view this post on Zulip Mario Carneiro (Oct 20 2020 at 01:07):

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

view this post on Zulip Mario Carneiro (Oct 20 2020 at 01:08):

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


Last updated: May 09 2021 at 23:10 UTC