Hi Yaqing,
Try this below - it returns a minimal thm list, based on the "black box"
technique. But I haven't tested it properly..
Apply it like this:
shrink_rewrite_list REWRITE_CONV [th1;th2;th3;th4] tm;;
Cheers,
Mark.
(* Utils *)
let remove_nth_elem n xs =
let (xs1,xs2) = chop_list (n-1) xs in
(xs1 @ tl xs2);;
let remove_one_combs xs =
map (C remove_nth_elem xs) (1 -- length xs);;
let smaller xs1 xs2 =
if (length xs1 <= length xs2)
then xs1
else xs2;;
let smallest xss = end_itlist smaller xss;;
(* shrink_arg_list *)
let rec shrink_arg_list (eqr:'a->'a->bool)
(f:'b list -> 'a) (xs:'b list) : 'b list =
let y = f xs in (* fails overall if fails on original list *)
let xss1 = remove_one_combs xs in
let foo xs1 = try
let y' = f xs1 in
(eqr y' y)
with Failure _ -> false in
let xss2 = filter foo xss1 in
if (xss2 = [])
then xs
else let xss3 = map (shrink_arg_list eqr f) xss2 in
smallest xss3;;
(* thm_eq *)
let list_eq eqr xs1 xs2 =
try
forall (uncurry eqr) (zip xs1 xs2)
with Failure _ -> false;;
let thm_eq th1 th2 =
let (hs1,c1) = dest_thm th1 in
let (hs2,c2) = dest_thm th2 in
(list_eq aconv hs1 hs2) && (aconv c1 c2);;
(* shrink_rewrite_list *)
let shrink_rewrite_list (rewrite_fn:thm list -> 'a -> thm)
(ths:thm list) (arg:'a) : thm list =
shrink_arg_list (thm_eq) (fun ths -> rewrite_fn ths arg) ths;;
On 31/01/2018 15:56, Yaqing Jiang wrote:
Hi Mark,
Sure, you help me a lot early 2015. Time flies!
I think you'll incorporate dependency tracking in a systematic way, so
I'll just try the black box method myself (I won't be using this very
often and the accuracy is not quite important).
I saw a directory Proofrecording in the root directory of HOL Light.
There's also anther implementation of dependency tracking as part of
anther project here [1] These might be helpful, just in case you need.
Thanks for the advice.
Best,
Yaqing
On 31/01/18 15:38, Mark Adams wrote:
Hi Yaqing,
Good to know someone's been using it!
This has always been in my list of things to do, since Tactician is
about both refactoring and dependency.
I was going to treat REWRITE_CONV (or potentially some other
function) like a black box. I think tweaking the REWRITE_CONV code
could also be a valid technique, but would require a bit of
investment understanding the implementation (which is not trivial!).
Best,
Mark.
On 31/01/2018 15:25, Yaqing Jiang wrote:
Hi Mark,
Thanks for the quick reply. You (and Tactician) have really helped
me
a lot these years!
I wonder if this feature is in your update plan?If not, I think I
should do this myself.
Now I'm not sure which method should be considered. I saw most proof
recording methods using a way that hacks the fusion.ml, and they
don't
even touch any functions related to REWRITE_CONV. I found it very
low
efficient to figure out how these functions in kernel finally used
in
REWRITE_CONV.
I was also thinking to just use a direct way you mentioned. Now that
you think it's a solution, I'll try this.
I'd like to have the minimal subset of the theorems(lemmas) used by
REWRITE_CONV. With the idea you mentioned, there are still 2 levels:
1. Treat REWRITE_CONV as a black box and use another functions
to
minimise the lemma list
2. If there's a loop inside REWRITE_CONV, and the theorems are
passed in serial, maybe I can track the results each time, which
might
be faster.
Best wishes,
Yaqing
On 31/01/18 14:58, Mark Adams wrote:
Hi Yaqing,
I could enhance my Tactician tool to do this sort of thing. In
fact, a new release is long overdue, so I'll try to find the time to
do this soon (but am too busy in the next few weeks).
But you say you're looking for a quick patch. One approach would be
to apply the original conversion, and then try taking out members of
the theorem list and keeping the same result. I can probably knock
up the code for this tonight.
Note that this idea gives you something a slightly different from
removing unused theorems - it's a list that removes any unused
theorems plus potentially others that have no effect on the overall
result (whether the original rewrite used them or not). Which of
these two are you interested in (or does it make no difference to
you)?
Best,
Mark.
On 31/01/2018 12:49, Yaqing Jiang wrote:
Sometimes when I'm using REWRITE_CONV[th1;th2...] to rewrite a term,
not all the theorems in th1,th2,... are used.
Anyone knows if there is a simple way of finding out which theorems
were actually applied?
I know there are methods that tracking the entire dependencies of a
proven theorem, but a small patch of REWRITE_CONV would work for me.
By the way, I'm using HOL Light, so things might be different. I
should be able to adapt the idea to HOL Light.
Best regards,
Yaqing
Links:
------
[1] http://cl-informatik.uibk.ac.at/software/hh/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Hi Yaqing,
Good to know someone's been using it!
This has always been in my list of things to do, since Tactician is
about both refactoring and dependency.
I was going to treat REWRITE_CONV (or potentially some other function)
like a black box. I think tweaking the REWRITE_CONV code could also
be
a valid technique, but would require a bit of investment understanding
the implementation (which is not trivial!).
Best,
Mark.
On 31/01/2018 15:25, Yaqing Jiang wrote:
Hi Mark,
Thanks for the quick reply. You (and Tactician) have really helped
me
a lot these years!
I wonder if this feature is in your update plan?If not, I think I
should do this myself.
Now I'm not sure which method should be considered. I saw most proof
recording methods using a way that hacks the fusion.ml, and they
don't
even touch any functions related to REWRITE_CONV. I found it very
low
efficient to figure out how these functions in kernel finally used
in
REWRITE_CONV.
I was also thinking to just use a direct way you mentioned. Now that
you think it's a solution, I'll try this.
I'd like to have the minimal subset of the theorems(lemmas) used by
REWRITE_CONV. With the idea you mentioned, there are still 2 levels:
1. Treat REWRITE_CONV as a black box and use another functions
to
minimise the lemma list
2. If there's a loop inside REWRITE_CONV, and the theorems are
passed in serial, maybe I can track the results each time, which
might
be faster.
Best wishes,
Yaqing
On 31/01/18 14:58, Mark Adams wrote:
Hi Yaqing,
I could enhance my Tactician tool to do this sort of thing. In
fact,
a new release is long overdue, so I'll try to find the time to do
this
soon (but am too busy in the next few weeks).
But you say you're looking for a quick patch. One approach would
be
to apply the original conversion, and then try taking out members
of
the theorem list and keeping the same result. I can probably knock
up
the code for this tonight.
Note that this idea gives you something a slightly different from
removing unused theorems - it's a list that removes any unused
theorems plus potentially others that have no effect on the overall
result (whether the original rewrite used them or not). Which of
these
two are you interested in (or does it make no difference to you)?
Best,
Mark.
On 31/01/2018 12:49, Yaqing Jiang wrote:
Sometimes when I'm using REWRITE_CONV[th1;th2...] to rewrite a
term,
not all the theorems in th1,th2,... are used.
Anyone knows if there is a simple way of finding out which
theorems
were actually applied?
I know there are methods that tracking the entire dependencies of
a
proven theorem, but a small patch of REWRITE_CONV would work for
me.
By the way, I'm using HOL Light, so things might be different. I
should be able to adapt the idea to HOL Light.
Best regards,
Yaqing
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
------------------------------------------------------------------------------
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
