Hi Matthias,
I'm not aware of an easy way. Moreover, for me it is unclear how to
count subgoals. I could well imagine that one wants to count only
"interesting ones", i.e. ignore trivial ones like "Cases_on `x:num` >>
ASM_REWRITE_TAC[...]", where the case for "0" is automatically discarded.
One idea would be to define a tactic for counting, i.e. something like
val subgoal_counter = ref 0;
fun COUNT_TAC (asm, g) = (subgoal_counter := !subgoal_counter + 1;
ALL_TAC (asm, g))
You can then add it at the places, where you want counting to happen,
e.g. after a "REPEAT CASE_TAC". Add some stuff for resetting the counter
and printing it, e.g. by a tactical like
fun PRINT_COUNT tac (asm, g) = let
val _ = subgoal_counter := 0;
val res = tac (asm, g);
val _ = print ("\n\nCOUNTER: "^(int_to_string (!subgoal_counter))^"\n\n");
in res end;
And you have some basic infrastructure. Very hackish, but probably
working, flexible and not too much work.
Cheers
Thomas
On 11.07.2017 12:34, Matthias Stockmayer wrote:
> Hi,
>
> I'm working on a proof that produces many subgoals due to a rather
> complex case-splitting structure. To see, if some changes to the proof
> increase or decrease the complexity, I'd like to know how many
> subgoals are produced and solved in the whole proof.
>
> So, is there any way to find out the number of subgoals, without
> manually stepping through the proof and counting?
>
> I know I can use the running time of the proof to compare different
> approaches, but I'm not sure how accurate this will be.
>
>
> With regards,
>
> Matthias
>
>
>
> ------------------------------------------------------------------------------
>
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
