Stream: General

Topic: Applying method n times

Josh Chen (Sep 30 2019 at 15:42):

Is there any way to apply a given method some fixed number of times, instead of arbitrarily many times using "+"? I am aware of [n] and it doesn't (always) do what I want; I want something that will also apply to new subgoals, but not all of them.

More specifically, I want to apply a given rule exactly n times in order to derive a term I want, and I can't use + because the rule loops. (Reformulating it is probably out of the question.)

Kevin Kappelmann (Sep 30 2019 at 16:06):

Maybe Eisbach will help in that case (note: I personally never used it)

Josh Chen (Sep 30 2019 at 16:18):

I don't think it does. About a year ago I hacked together a rough solution using Eisbach and ML, but it wasn't very nice.

But I suppose [n] is working well for my uses at the moment.

EDIT: Maybe you're right, another look at the Eisbach source brings up determ, which sounds promising... If this lets me limit the number of method applications, I can't figure it out.

Mathias Fleury (Oct 01 2019 at 06:38):

An ML solution:

lemma imp: ‹P ∧ P ⟹ P›
  by auto
lemma P
  apply (tactic ‹REPEAT_DETERM_N 3 (HEADGOAL (resolve_tac @{context} @{thms imp}))›)

Mathias Fleury (Oct 01 2019 at 06:43):

(and the Eisbach solution is probably either to lift REPEAT_DETERM_N to Eisbach -- I don't know how -- or to introduce a predicate "repeat n = True" and, add "repeat n" as assumption to the goal you want to change, repeat the rule as long as n > 0 and decrease the n, and finally remove the "repeat 0" from the assumptions)

Josh Chen (Oct 01 2019 at 09:05):

An ML solution:
[...]

Thanks! That's basically what I have. It would be nice if there were a way to directly pass a method instead of a tactic, though.

Last updated: Apr 23 2024 at 12:29 UTC