[Hol-info] Counting Subgoals in a Proof

[Matthias Stockmayer]

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

[Thomas Tuerk]

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

Post by Matthias Stockmayer
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
https://lists.sourceforge.net/lists/listinfo/hol-info

[Konrad Slind]

To follow up on Thomas' post, you can easily write a tactical that will do
such counting. In
the following I print out the number, but you could also store it in a
reference cell, as Thomas
does.

fun COUNT_TAC tac g =
let val res as (sg,_) = tac g
val _ = print ("subgoals"^Int.toString (List.length sg)^"\n")
in res
end

The nice thing about this is that you can wrap any tactic with it and get a
count out, which
should help for your application.

Example (here the compound tactic generates 4 subgoals, three of which get
solved by
the trailing "simp_tac list_ss []" tactic):

g `!l1 l2. REVERSE(l1 ++ l2) = REVERSE l2 ++ REVERSE l1`;

e (COUNT_TAC (Induct >> (Induct ORELSE (gen_tac >> Induct))) >> simp_tac

list_ss []);
OK..
subgoals: 4
1 subgoal:
val it =


∀h'. REVERSE (l1 ++ h'::l2) = REVERSE l2 ++ [h'] ++ REVERSE l1
------------------------------------
0. ∀l2. REVERSE (l1 ++ l2) = REVERSE l2 ++ REVERSE l1
1. REVERSE (h::l1 ++ l2) = REVERSE l2 ++ REVERSE (h::l1)
:
proof

Konrad.

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

Post by Matthias Stockmayer
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
------------------------------------------------------------

------------------

Post by Matthias Stockmayer
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
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
https://lists.sourceforge.net/lists/listinfo/hol-info