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.
On Tue, Jul 11, 2017 at 6:36 AM, Thomas Tuerk <tho...@tuerk-brechen.de>
wrote:
> 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
>
------------------------------------------------------------------------------
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
