Tactic timeout

Stream: general

[Rémy Degenne]

I have observed a weird timeout in the measurability tactic and I would like to debug it but I don't know anything about how to do that. Here is the mwe:

import measure_theory.tactic
import measure_theory.constructions.prod

example : measurable (λ p : ℝ × ℝ, p.fst + p.snd) :=
by measurability  -- fast

example {ι : Type*} (i k : ι) (hik : i ≠ k) : measurable (λ p : ℝ × ℝ, p.fst + p.snd) :=
by measurability  -- deterministic timeout

in the second example I added some variables which are completely irrelevant, and I get a timeout. Removing hik makes it fast. I am interested in understanding why that happens, but I would be even more thankful if somebody could give me indications on how to debug that tactic myself.

[Rémy Degenne]

Replacing i ≠ k by i = k also makes it fast.

[Rob Lewis]

First the explanation, then how I got there: the measurability tactic tries to call a bunch of different rules. One of them is apply_assumption, which will cause a loop if there's any negated hypothesis. First apply_any tries to apply each hypothesis directly. Then it calls symmetry and goes again. Then it calls exfalso and goes again. But if you have h : ¬ P in your context, this will always apply after calling exfalso. So measurability (via tidy) ends up in an infinite loop of exfalso, apply hik.

[Rob Lewis]

To figure this out I looked at the definition of measurability and saw that it's essentially tactic.tidy { tactics := measurability_tactics }. I pasted this into your example and still saw the same behavior. Then I copied measurability_tactics and commented out the first one, and the behavior changed; I commented everything but the first one and the behavior returned, so that meant it was likely something with the apply_assumption rule.

[Rémy Degenne]

Thanks for the explanation!
That call to apply_assumption is something I added when I adapted the continuity tactic to prove measurability. It has been there for a while and now I am surprised that we did not stumble upon that problem earlier.

[Rémy Degenne]

The only assumptions I really want to apply are of the shape measurable or measurable_set etc. I guess the safe way to replace apply_assumption is to write a tactic that applies only the ones I want.

[Rob Lewis]

You could also modify apply_assumption to take an optional apply_any_opt config argument, which you can use to disable the exfalso behavior

[Rémy Degenne]

Thanks! That's what I also realized and I am doing that right now! I need to figure out the syntax for passing config options first :)

[Rob Lewis]

You should be able to do something like

meta def apply_assumption (opt : apply_any_opt := {}) : tactic unit :=
local_context >>= apply_any opt

meta def measurability_tactics' (md : transparency := semireducible) : list (tactic string) :=
[
  propositional_goal >> apply_assumption {use_exfalso := ff}
                        >> pure "apply_assumption"
 ...]

[Rémy Degenne]

I could almost write exactly that. The apply_assumption tactic you wrote returns an error, but can be written as

meta def apply_assumption' (opt : apply_any_opt := {}) : tactic unit :=
do l ← local_context, apply_any l opt

It looks like it all works now. Thanks again!