I might need to forward the solution I got from Mark here as well:
-------- Forwarded Message --------
Subject: Re: [Hol-info] Tracking lemmas used by REWRITE_CONV
Date: Wed, 31 Jan 2018 15:38:46 +0000
From: Mark Adams <m...@proof-technologies.com>
To: Yaqing Jiang <s1318...@sms.ed.ac.uk>
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
