OK, my original example now works.
But I get exception Unchanged raised when I try IMP_REWRITE_TAC[] on the
goal ``p \/ q ==> q \/ p``.
I still would expect the tactic to be able to solve this goal, no?
And if it can't then would it not be better to leave the goal unchanged
rather than to raise an exception?
On Mon, Feb 10, 2014 at 10:31 PM, Vincent Aravantinos <
[email protected]> wrote:
> Solved. The new version is uploaded:
> https://github.com/aravantv/HOL4-impconv
>
> Thanks for the report! Was indeed a mistake in the translation from
> HOL-Light/Ocaml to HOL4/SML...
>
> V.
>
> Le 10/02/2014 21:00, Vincent Aravantinos a écrit :
>
> So indeed, the goal is solved immediatly in HOL Light... Gonna work on it
> :-/
>
> Le 10/02/2014 18:39, Vincent Aravantinos a écrit :
>
> Hi Ramana,
>
> - regarding your example: no, it is not the intended behavior. I'll have a
> look asap.
>
> - regarding the infinite loop: do you mean that it goes most of the time
> into an infinite loop? This is not normal either... Could you provide me
> with such examples?
>
> The examples provided in the manual are a good starting point to grasp a
> lil bit better the intended behaviour. Dunno if that helps though.
> Unfortunately, on a daily basis, I use only the HOL Light version of it
> and could not test on real-life use cases the HOL4 version :-(
>
> Cheers,
> V.
>
> On 10.02.2014 18:23, Ramana Kumar wrote:
>
> Hi Vincent,
>
> I have just now started trying to use your new tactic, and I am having
> some trouble. When I call IMP_REWRITE_TAC[] on some simple goal like ``p /\
> q ==> q /\ p``, it raises an exception (Unchanged). Is this the intended
> behaviour? That seems pretty annoying.
>
> Also, I have not yet found a non-trivial example on which it does not
> appear to go into an infinite loop. But I haven't looked far yet.
>
> Cheers,
> Ramana
>
>
> On Tue, Jul 30, 2013 at 1:33 PM, Vincent Aravantinos <
> [email protected]> wrote:
>
>> Hi Ramana,
>>
>> I will make a few performance improvements on the HOL Light version in
>> the coming weeks hopefully, and then I plan indeed to "translate" it to
>> HOL4.
>>
>> V.
>>
>>
>> 2013/7/30 Ramana Kumar <[email protected]>
>>
>>> This looks great, Vincent.
>>> Are you interested in working on a version for HOL4?
>>>
>>>
>>> On Thu, Jul 11, 2013 at 11:08 AM, Vincent Aravantinos <
>>> [email protected]> wrote:
>>>
>>>> Hi list,
>>>>
>>>> I developed a new tactic that takes a theorem of the form P ==> l = r
>>>> and replaces l by r in a goal adding whatever it needs to make it work
>>>> properly (typically conjunction with P; but can also be an implication or
>>>> even existentials).
>>>>
>>>> This is a follow-up of the discussion I started a few months ago (
>>>> http://sourceforge.net/mailarchive/message.php?msg_id=30133516), the
>>>> major difference being that it solves the problem raised by Michael Norrish
>>>> (i.e., it could not work under the scope of a quantifier) in a systematic
>>>> and (in my opinion) elegant way.
>>>>
>>>> This change entails that the tactic is much more modular and thus can
>>>> be chained very smoothly. Many preprocessing options also allows it to be a
>>>> (sometimes more powerful) replacement for REWRITE_TAC, SIMP_TAC and even
>>>> MATCH_MP_TAC. Please look at the (draft) manual for more info.
>>>>
>>>> The code is available at: https://github.com/aravantv/impconv (HOL
>>>> Light only for now)
>>>> To install, type:
>>>> # needs "target_rewrite.ml";;
>>>> The pdf manual is available in the directory "manual".
>>>>
>>>> The development of this tactic required quite some work that might be
>>>> useful in other context. This is undocumented for now but is described in a
>>>> paper which is currently under review.
>>>>
>>>> Regards,
>>>> --
>>>> Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University,
>>>> Hardware
>>>> Verification Group
>>>> http://users.encs.concordia.ca/~vincent/
>>>>
>>>>
>>>> ------------------------------------------------------------------------------
>>>> See everything from the browser to the database with AppDynamics
>>>> Get end-to-end visibility with application monitoring from AppDynamics
>>>> Isolate bottlenecks and diagnose root cause in seconds.
>>>> Start your free trial of AppDynamics Pro today!
>>>>
>>>> http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk
>>>> _______________________________________________
>>>> hol-info mailing list
>>>> [email protected]
>>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>>
>>>>
>>>
>>
>>
>> --
>> Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University,
>> Hardware
>> Verification Group
>> http://users.encs.concordia.ca/~vincent/
>>
>
>
>
> --
> Dr Vincent Aravantinos
> Analysis and Design of Dependable Systems
> fortiss GmbH <www.fortiss.org/en>
> T +49 (0)89 360 35 22 33 | Fx +49 (0)89 360 35 22 50
> Guerickestrasse 25 | 80805 Munich | Germany
>
>
> --
> Dr Vincent Aravantinos
> Analysis and Design of Dependable Systems
> fortiss GmbH <www.fortiss.org/en>
> Guerickestrasse 25 | 80805 Munich | Germany
>
>
>
>
> ------------------------------------------------------------------------------
> Androi apps run on BlackBerry 10
> Introducing the new BlackBerry 10.2.1 Runtime for Android apps.
> Now with support for Jelly Bean, Bluetooth, Mapview and more.
> Get your Android app in front of a whole new audience. Start
> now.http://pubads.g.doubleclick.net/gampad/clk?id=124407151&iu=/4140/ostg.clktrk
>
>
>
> _______________________________________________
> hol-info mailing
> [email protected]https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
> --
> Dr Vincent Aravantinos
> Analysis and Design of Dependable Systems
> fortiss GmbH <www.fortiss.org/en>
> Guerickestrasse 25 | 80805 Munich | Germany
>
>
>
------------------------------------------------------------------------------
Android apps run on BlackBerry 10
Introducing the new BlackBerry 10.2.1 Runtime for Android apps.
Now with support for Jelly Bean, Bluetooth, Mapview and more.
Get your Android app in front of a whole new audience. Start now.
http://pubads.g.doubleclick.net/gampad/clk?id=124407151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
