Email Gateway (Aug 18 2022 at 17:49): Email Gateway (Aug 18 2022 at 17:49):From: Abderrahmane FELIACHI <Abderrahmane.Feliachi@lri.fr>
Hi all,
I'm trying to write the (recursive) tactic described as below:
A - apply some elimination rule to the subgoal n producing 3 subgoals
(n, n+1, n+2), then :
1 - simultaneously apply some elimination rules to the 3
subgoals. then
2 - apply the same tactic to the 3 subgoals (with different
parameters for each case).
My problem is that when applying the elimination rules in 1, this can
lead to 0 or more subgoals,
so I cannot apply the tactics in 2 to the subgoals (n, n+1, n+2).
My question is: Wich combinator should I use in step 1 and 2 in order to
apply (locally) these steps with rules (n, n+1, n+2) whatever the result
of applying the rule 1.
Thanks a lot,
Abdou
Email Gateway (Aug 18 2022 at 17:50):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
It sounds like you need THEN_ALL_NEW, which is generally pretty useful.
So you can write your tactic a bit like this. I'm referring to your stage (1) as tac2.
fun tac arg n =
(etac erule_thm n
THEN (tac2 THEN_ALL_NEW tac 1) (n + 2)
THEN (tac2 THEN_ALL_NEW tac 2) (n + 1)
THEN (tac2 THEN_ALL_NEW tac 3) n
That's a bit ugly, obviously, you could clean up the repetition with some kind of EVERY.
BTW, passing different parameters to tac positionally can work well, but always consider whether it's possible to figure out what to do by inspecting the goal state with SUBGOAL or similar, giving you tactics that are easier to compose.
Yours,
Thomas.
Last updated: Apr 25 2024 at 12:23 UTC