To turn simplifier tracking on, just set the reference:
val _ = simpLib.track_rewrites := true
Then after some simplification, you can see what rewrites were used by
looking at
val result = !simpLib.used_rewrites
Alternatively, wrap your call to RW_TAC with simpLib.track, i.e. use
simpLib.track (RW_TAC [...]) [...]. Then examine the contents of
simpLib.used_rewrites as before.
P.S. Thanks Konrad, I didn't know about these before :)
On Mon, Oct 28, 2013 at 3:09 PM, Andrea <ag...@leicester.ac.uk> wrote:
> Hi,
>
> mmm.. I have not really understood how could I modify the flag.
> The trial and error approach seems more feasible at my hol level.
> However thank you both.
> Bye,
>
> Andrea
>
> P.S: how do you understand which theorems helped in proofing your goals
> when you use the RW_TAC reasoner?
>
>
> On 25/10/13 23:45, Konrad Slind wrote:
>
> There is a flag implemented so that the simplifier
> tracks which rules are successfully applied. See
>
> simpLib.{track,track_rewrites,used_rewrites}
>
> Konrad.
>
>
>
> On Fri, Oct 25, 2013 at 3:47 PM, Ramana Kumar <ram...@member.fsf.org>wrote:
>
>> There's no easy way to do this, that I know of, but there are several
>> difficult ways.
>>
>> The simplest is: try removing the theorem from the list you give to
>> METIS_TAC (or RW_TAC) and see if the proof still goes through or not.
>> This is a trial and error approach, so is a bit tedious, but is at least
>> simple.
>>
>> The other approaches I can think of would involve proof recording of
>> some kind: possibly using the OpenTheory logging kernel, or some
>> custom-made proof-logging code, then inspecting the proof of the theorem to
>> see which other theorems it references.
>>
>>
>> On Fri, Oct 25, 2013 at 3:25 PM, Andrea <ag...@leicester.ac.uk> wrote:
>>
>>> Hi everyone,
>>>
>>> I am advancing step by step in the tutorial, and now I am interactively
>>> following the example of the Euclid's theorem proofing.
>>> In this example it is made an heavy usage of the MATIS_TAC reasoner, and
>>> here my question: is it possible to see which theorem the reasoner
>>> chooses among those given in the list?
>>> I think it would help me in understanding how the proof is built.
>>> Thank you anyway,
>>>
>>> Andrea
>>>
>>>
>>> ------------------------------------------------------------------------------
>>> October Webinars: Code for Performance
>>> Free Intel webinars can help you accelerate application performance.
>>> Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most
>>> from
>>> the latest Intel processors and coprocessors. See abstracts and register
>>> >
>>>
>>> http://pubads.g.doubleclick.net/gampad/clk?id=60135991&iu=/4140/ostg.clktrk
>>> _______________________________________________
>>> hol-info mailing list
>>> hol-info@lists.sourceforge.net
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>
>>
>>
>> ------------------------------------------------------------------------------
>> October Webinars: Code for Performance
>> Free Intel webinars can help you accelerate application performance.
>> Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most
>> from
>> the latest Intel processors and coprocessors. See abstracts and register >
>>
>> http://pubads.g.doubleclick.net/gampad/clk?id=60135991&iu=/4140/ostg.clktrk
>> _______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>
>
------------------------------------------------------------------------------
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from
the latest Intel processors and coprocessors. See abstracts and register >
http://pubads.g.doubleclick.net/gampad/clk?id=60135991&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
