interval_cases bug

Stream: general

[Heather Macbeth]

I believe I have found a bug in interval_cases. In a situation with multiple goals (which of course doesn't happen in mathlib), it will act on a later goal rather than the current goal.

import tactic.interval_cases

example {x : ℤ}
  (hx1 : -1 ≤ x)
  (hx2 : x ≤ 1) :
  x + 17 = 4 :=
begin
  have : x < 3,
  { interval_cases x, -- works
     },
end

example {x : ℤ}
  (hx1 : -1 ≤ x)
  (hx2 : x ≤ 1) :
  x + 17 = 4 :=
begin
  have : x < 3,
  interval_cases x, -- acts on the second goal

end

[Heather Macbeth]

Goal-juggling happens to be one of the topics not covered by @Rob Lewis's tutorials, so I don't know how to fix it :)

[Damiano Testa]

What happens if you add focus1 $ right after := in docs#tactic.interactive.interval_cases? (I'm on mobile, so cannot test myself)

[Damiano Testa]

(Ideally, this would be the analogue of putting the tactic inside { ... }.)

[Damiano Testa]

Except that there is no obligation to close the goal, I think.

[Damiano Testa]

If you look at the implementation of interval_cases, it calls docs#tactic.fin_cases_at. fin_cases_at, is also called by docs#tactic.interactive.fin_cases and seems to always be called inside a focus1, supporting the evidence that also interval_cases should similarly protect the main goal before calling fin_cases_at.

[Heather Macbeth]

So maybe in fact we shoult move the focus1 inside docs#tactic.fin_cases_at?

[Damiano Testa]

I do not know what causes leakage, but many tactics apply indiscriminately to all available goals. I was very surprised by this at first, but have gotten accustomed to this behaviour.

[Heather Macbeth]

This is worse, though -- it doesn't get applied to the current goal!

[Damiano Testa]

Maybe, though I would have to look at fin_cases_at on a computer: it may not fix the issue if fin_cases_at receives already the wrong expression.

[Damiano Testa]

Somewhere, lists appear reversed, so it may be that the tactic applies to the first available goal of a reversed list? I am really grasping here, just browsing the code on mobile, though! :upside_down:

[Heather Macbeth]

Actually, I think I described it wrong. It acts on the first goal, but it sends those goals to the end of the list, after the preexisting goals.

[Heather Macbeth]

So the goal state goes from

⊢ x < 3
⊢ x + 17 = 4

to

⊢ x + 17 = 4
⊢ -1 < 3
⊢ 0 < 3
⊢ 1 < 3

(hypotheses omitted)

[Damiano Testa]

Ok, so there may be some get/set_goals weirdness? Still, focus1 did not help?

[Damiano Testa]

docs#tactic.fin_cases_at_aux has a suspicious rotate_left call that might achieve a weird positioning of goals if there are goals that are not generated by the tactic itself.

[Damiano Testa]

Oh link does not work, since the def fin_cases_at_aux is private. :face_palm:

[Damiano Testa]

My current guess is that the issue arises from docs#tactic.rotate_left applied by fin_cases_at_aux, but I still hope that focus1 may force rotate_left to achieve the intended behaviour.

[Damiano Testa]

The working hypothesis being that rotate_left mangles the extra goal with the ones that interval_cases produces and expects.

[Damiano Testa]

(this is all very speculative, since I actually never used interval/fin_cases!)

[Damiano Testa]

Speculating some more: once the wrong goal gets moved to a prominent position, one of the tactics that would make progress on the "correct" side-goals no longer succeeds. interval_cases therefore thinks that it made all the progress that it was expected to do and stops. However, the int inequalities that you copied above have not been norm_nummed, as they were "in the shadow" of the x + 17 = 4 goal.

[Damiano Testa]

I do not know exactly what causes the issue, but encasing interval_cases in a focus1 seems to produce a behaviour that is closer to the expected one.

#16752

[Heather Macbeth]

Thanks for tracking this down, Damiano!!

[Damiano Testa]

I just tried to put the focus1 on fin_cases_at and removing all the other focus1 that I could find in fin_cases and the new one on interval_cases and it also seems to fix the issue and not create another one in the test files.

It seems like a more stable solution: should I put the focus1 on fin_cases_at?

[Heather Macbeth]

That seems like a nicer solution to me. But I'm not an expert.

[Damiano Testa]

I agree with you: I pushed the focus1 inside fin_cases_at and removed it from fin_cases and the newly added one in interval_cases.

This solution seems more stable: as it currently is, if some other tactic wants to call the non-interactive fin_cases_at, they do not need to worry about focusing.