alternate tactics

Stream: general

[Patrick Massot]

What is the nice way to alternate two tactics until the goal is closed or neither make any progress? I know I can do repeat (tac1 <|> tac2) but this is stupid, right?

[Jalex Stark]

why is it stupid? i thought the behavior is exactly as you described (so there probably isn't a more efficient implementation), and it's hard to imagine a shorter incantation

[Jalex Stark]

(also i usually write repeat { tac1 <|> tac2} instead, is there any difference?)

[Jalex Stark]

what would you like to type instead, and would the behavior be different from the repeat block?

[Patrick Massot]

I should have said that tac1 and tac2 cannot succeed twice in a row.

[Jalex Stark]

oh i see, the repeat block will incur possibly a factor of 2 penalty?

[Patrick Massot]

Say tac1 succeeds. Then you repeat and first try tac1 that you know will fail before trying tac2. etc.

[Patrick Massot]

Yes

[Patrick Massot]

I need a computer scientist. Is there a computer scientist in this plane?

[Jalex Stark]

i wonder if passing your tactics to tidy works?

[Kevin Buzzard]

The penalty factor might shoot up a lot more then :-)

[Alex J. Best]

I'm not sure I understand what you want but is repeat { tac1 , tac2} <|> repeat { tac2, tac1} better?

[Jalex Stark]

Right, I really meant "does tidy specifically know how to not re-apply a tactic it know will fail", and then if the answer is yes, looking at the tidy source will tell you the answer

but probably the answer is no, tidy doesn't have a way to know that a tactic won't succeed twice

[Jalex Stark]

Alex J. Best said:

I'm not sure I understand what you want but is repeat { tac1 , tac2} <|> repeat { tac2, tac1} better?

I think yes? I think this never applies tac1 twice in a row and applies tac2 twice in a row at most once

[Patrick Massot]

This will fail if tac1 closes the goal immediately for instance

[Jalex Stark]

then use a semicolon?

[Jalex Stark]

repeat { tac1; tac2 } <|> repeat { tac2; tac1 }

[Patrick Massot]

That one may work...

[Patrick Massot]

It works on 12 examples, and we're in meta-land so I guess it counts as a proof.

[Jalex Stark]

did you have examples when you opened the question? it's possible that posting them may have led to us getting the answer faster

[Jalex Stark]

oh, does "work" mean "close the goal" or "close the goal faster than repeat { tac1 <|> tac2 }"?

[Patrick Massot]

Close the goal without applying the same tactic twice in a row.

[Patrick Massot]

In my case it seems we can even assume we always start with tac1

[Patrick Massot]

so repeat (tac1 ; tac 2) is good enough

[Jannis Limperg]

Here's a direct implementation (untested, ymmv):

namespace tactic

meta def iterate_alternating_aux : tactic unit → tactic unit → bool → tactic unit
:= λ t₁ t₂ stop_on_fail, do
  progress ← try_core t₁,
  match progress, stop_on_fail with
  | some _, _ := iterate_alternating_aux t₂ t₁ ff
  | none, ff := iterate_alternating_aux t₂ t₁ tt
  | none, tt := pure ()
  end

meta def iterate_alternating (t₁ t₂ : tactic unit) : tactic unit :=
iterate_alternating_aux t₁ t₂ ff

end tactic


namespace tactic.interactive

meta def iterate_alternating (t₁ t₂ : itactic) : tactic unit :=
tactic.iterate_alternating t₁ t₂

end tactic.interactive

[Patrick Massot]

Thanks. Is there any advantage over the naive method that Jalex found?

[Jannis Limperg]

Jalex's tactic looks fishy to me because repeat t never fails, so the <|> ... should never be executed.

repeat (tac1; tac2) behaves slightly differently than my tactic: afaiu, it stops when either tac1 or tac2 fails for the first time, whereas my tactic only stops when both tac1 and tac2 fail. So my tactic permits the sequence tac2, tac2, ...whereas yours requires tac1, tac2, tac1, ....

[Patrick Massot]

Avoiding tac2, tac2 was exactly my request

[Jannis Limperg]

Then the repeat thing should have the right semantics.