Re: [Hol-info] New tactic: IMP_REWRITE_TAC
On 14.02.2014 01:42, Michael Norrish wrote:
On 13/02/14 04:46, Vincent Aravantinos wrote:
Then considering leaving the goal unchanged, well it is a matter of taste...
I
know it is the standard to leave the goal unchanged. But I personally met
many
buggy situations that I hardly detected because HOL {4,Light} was just
allowing
a rewrite (in the middle of a big script) to leave a goal unchanged whereas a
rewrite should have happened. It was so hard to debug that I went to the
conclusion to raise an exception instead
Note that one can transform a tactic of one type into the other with
CHANGED_TAC (silently lets things not change -- exception)
and
TRY (exception -- silently lets things not change)
I know, and TRY is shorter to write than CHANGED_TAC :-)
Given this, I think it's probably better to have the primitives conform to the
default behaviour (if only because of the principle of least surprise).
But indeed, I should stick to the convention...
--
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
--
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=124407151iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
On 13/02/14 04:46, Vincent Aravantinos wrote:
Then considering leaving the goal unchanged, well it is a matter of taste... I
know it is the standard to leave the goal unchanged. But I personally met many
buggy situations that I hardly detected because HOL {4,Light} was just
allowing
a rewrite (in the middle of a big script) to leave a goal unchanged whereas a
rewrite should have happened. It was so hard to debug that I went to the
conclusion to raise an exception instead
Note that one can transform a tactic of one type into the other with
CHANGED_TAC (silently lets things not change -- exception)
and
TRY (exception -- silently lets things not change)
Given this, I think it's probably better to have the primitives conform to the
default behaviour (if only because of the principle of least surprise).
Michael
signature.asc
Description: OpenPGP digital signature
--
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=124407151iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
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 vincent.aravanti...@fortiss.org 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 vincent.aravanti...@gmail.com 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 ramana.ku...@cl.cam.ac.uk 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 vincent.aravanti...@gmail.com 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=48808831iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net 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
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
Hi Ramana,
this is intended: what makes the tactic solve p /\ q == q /\ p is
that it uses the context p /\ q when doing the rewriting. Therefore
the theorems used for the rewrite are p = T and q = T, which indeed
turns p /\ q into T /\ T.
However with p \/ q the context only brings (p \/ q) = T which does
not allow to turn q \/ p into T just by rewriting.
Possible solutions would be either to take commutativity of disjunction
into account in the basic rewrites but this is not really easy to deal
with in a proper way since this brings the usual non-termination problems.
Another solution would be to consider a branching in the way rewriting
is done: one branch where p holds and one where q holds. But then this
goes way beyond rewriting.
Note for instance that neither FULL_SIMP_TAC nor RW_TAC can solve this
goal either.
Then considering leaving the goal unchanged, well it is a matter of
taste... I know it is the standard to leave the goal unchanged. But I
personally met many buggy situations that I hardly detected because HOL
{4,Light} was just allowing a rewrite (in the middle of a big script) to
leave a goal unchanged whereas a rewrite should have happened. It was so
hard to debug that I went to the conclusion to raise an exception
instead
V.
On 12.02.2014 13:42, Ramana Kumar wrote:
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
vincent.aravanti...@fortiss.org
mailto:vincent.aravanti...@fortiss.org 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
vincent.aravanti...@gmail.com
mailto:vincent.aravanti...@gmail.com 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 ramana.ku...@cl.cam.ac.uk
mailto:ramana.ku...@cl.cam.ac.uk
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
vincent.aravanti...@gmail.com
mailto:vincent.aravanti...@gmail.com 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
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
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 vincent.aravanti...@gmail.com 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 ramana.ku...@cl.cam.ac.uk 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 vincent.aravanti...@gmail.com 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=48808831iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ -- Androidtrade; apps run on BlackBerryreg;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=124407151iu=/4140/ostg.clktrk___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
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 vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com 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 ramana.ku...@cl.cam.ac.uk mailto:ramana.ku...@cl.cam.ac.uk 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 vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com 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 http://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/ http://users.encs.concordia.ca/%7Evincent/ -- 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=48808831iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net mailto:hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ http://users.encs.concordia.ca/%7Evincent/ -- 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 -- Androidtrade; apps run on BlackBerryreg;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
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
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 vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com 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 ramana.ku...@cl.cam.ac.uk mailto:ramana.ku...@cl.cam.ac.uk 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 vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com 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 http://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/ http://users.encs.concordia.ca/%7Evincent/ -- 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=48808831iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net mailto:hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ http://users.encs.concordia.ca/%7Evincent/ -- 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
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
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 vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com 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 ramana.ku...@cl.cam.ac.uk mailto:ramana.ku...@cl.cam.ac.uk 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 vincent.aravanti...@gmail.com mailto:vincent.aravanti...@gmail.com 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 http://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/ http://users.encs.concordia.ca/%7Evincent/ -- 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=48808831iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net mailto:hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ http://users.encs.concordia.ca/%7Evincent/ -- Dr Vincent Aravantinos Analysis and Design of Dependable Systems fortiss GmbH www.fortiss.org/en T +49 (0)89
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
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 vincent.aravanti...@gmail.com 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=48808831iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Get your SQL database under version control now! Version control is standard for application code, but databases havent caught up. So what steps can you take to put your SQL databases under version control? Why should you start doing it? Read more to find out. http://pubads.g.doubleclick.net/gampad/clk?id=49501711iu=/4140/ostg.clktrk___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
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 ramana.ku...@cl.cam.ac.uk 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 vincent.aravanti...@gmail.com 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=48808831iu=/4140/ostg.clktrk ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ -- Get your SQL database under version control now! Version control is standard for application code, but databases havent caught up. So what steps can you take to put your SQL databases under version control? Why should you start doing it? Read more to find out. http://pubads.g.doubleclick.net/gampad/clk?id=49501711iu=/4140/ostg.clktrk___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
Hi Peter,
here is the difference:
(* The new hypotheses are added as conjuncts rather than as a *)
(* separate subgoal to reduce the user's burden of subgoal splits *)
(* when creating tactics to prove theorems. If a separate subgoal*)
(* is desired, simply use CONJ_TAC after the dependent rewriting to *)
(* split the goal into two, where the first contains the hypotheses *)
(* and the second contains the rewritten version of the original *)
(* goal. *)
In my tactic, the new hypotheses are added deeply, as close as possible to
the atom where the rewrite happens.
Consider the following examples:
- Consider the goal:
!x. x 0 == x / x = y
Then my tactic will replace it by:
!x. x 0 == x 0 /\ 1 = y
Whereas, from my tries, dep_rewrite could not apply because x is quantified.
- Without the quantification, you can consider the goal:
x 0 == x / x = y
where dep_rewrite would yield
x 0 /\ (x 0 == x / x = y)
which is not provable, whereas my tactic yields:
x 0 == x 0 /\ x / x = y
This looks like a small difference but it changes a lot of things in
practice because calls to dep_rewrite need to be interleaved by calls to
GEN_TAC or DISCH_TAC (in these examples), whereas with my tactic one call
to IMP_REWRITE_TAC (with several theorems) is enough.
This change is not just a simple change but required the development of a
new notion of conversion, hence it seemed better to me to start it from
scratch rather than patching dep_rewrite.
V.
2013/7/11 Peter Vincent Homeier palan...@trustworthytools.com
Vincent, how does this tactic compare to the dependent rewriting package
in src/1/dep_rewrite.{sig,sml}? It appears at first glance to address the
same problem you are working on. Here is part of the .sig header comment:
(* == *)
(* == *)
(* DEPENDENT REWRITING TACTICS*)
(* == *)
(* == *)
(**)
(* This file contains new tactics for dependent rewriting,*)
(* a generalization of the rewriting tactics of standard HOL. *)
(**)
(* The main tactics are named DEP_REWRITE_TAC[thm1,...], etc., with *)
(* the standard variations (PURE,ONCE,ASM). In addition, tactics *)
(* with LIST instead of ONCE are provided, making 12 tactics in all. *)
(**)
(* The argument theorems thm1,... are typically implications. *)
(* These tactics identify the consequents of the argument theorems, *)
(* and attempt to match these against the current goal. If a match *)
(* is found, the goal is rewritten according to the matched instance *)
(* of the consequent, after which the corresponding hypotheses of *)
(* the argument theorems are added to the goal as new conjuncts on*)
(* the left. *)
(**)
(* Care needs to be taken that the implications will match the goal *)
(* properly, that is, instances where the hypotheses in fact can be *)
(* proven. Also, even more commonly than with REWRITE_TAC, *)
(* the rewriting process may diverge. *)
(**)
(* Each implication theorem for rewriting may have a number of layers *)
(* of universal quantification and implications. At the bottom of*)
(* these layers is the base, which will either be an equality, a *)
(* negation, or a general term. The pattern for matching will be *)
(* the left-hand-side of an equality, the term negated of a negation, *)
(* or the term itself in the third case. The search is top-to-bottom,*)
(* left-to-right, depending on the quantifications of variables. *)
(**)
(* To assist in focusing the matching to useful cases, the goal is*)
(* searched for a subterm matching the pattern. The matching of the *)
(* pattern to subterms is performed by higher-order matching, so for *)
(* example, ``!x. P x`` will match the term ``!n. (n+m) 4*n``. *)
(**)
(* The argument theorems may each be either an implication or not.*)
(* For those which are implications, the hypotheses of the instance *)
(* of each theorem which matched the goal are added to the goal as*)
(* conjuncts on the left side. For
Re: [Hol-info] New tactic: IMP_REWRITE_TAC
Forgot: in the examples below, both tactics are used with the theorem |-
!x. x 0 == x / x = 1
2013/7/11 Vincent Aravantinos vincent.aravanti...@gmail.com
Hi Peter,
here is the difference:
(* The new hypotheses are added as conjuncts rather than as a *)
(* separate subgoal to reduce the user's burden of subgoal splits *)
(* when creating tactics to prove theorems. If a separate subgoal*)
(* is desired, simply use CONJ_TAC after the dependent rewriting to *)
(* split the goal into two, where the first contains the hypotheses *)
(* and the second contains the rewritten version of the original *)
(* goal. *)
In my tactic, the new hypotheses are added deeply, as close as possible to
the atom where the rewrite happens.
Consider the following examples:
- Consider the goal:
!x. x 0 == x / x = y
Then my tactic will replace it by:
!x. x 0 == x 0 /\ 1 = y
Whereas, from my tries, dep_rewrite could not apply because x is
quantified.
- Without the quantification, you can consider the goal:
x 0 == x / x = y
where dep_rewrite would yield
x 0 /\ (x 0 == x / x = y)
which is not provable, whereas my tactic yields:
x 0 == x 0 /\ x / x = y
This looks like a small difference but it changes a lot of things in
practice because calls to dep_rewrite need to be interleaved by calls to
GEN_TAC or DISCH_TAC (in these examples), whereas with my tactic one call
to IMP_REWRITE_TAC (with several theorems) is enough.
This change is not just a simple change but required the development of a
new notion of conversion, hence it seemed better to me to start it from
scratch rather than patching dep_rewrite.
V.
2013/7/11 Peter Vincent Homeier palan...@trustworthytools.com
Vincent, how does this tactic compare to the dependent rewriting package
in src/1/dep_rewrite.{sig,sml}? It appears at first glance to address the
same problem you are working on. Here is part of the .sig header comment:
(* == *)
(* == *)
(* DEPENDENT REWRITING TACTICS*)
(* == *)
(* == *)
(**)
(* This file contains new tactics for dependent rewriting,*)
(* a generalization of the rewriting tactics of standard HOL. *)
(**)
(* The main tactics are named DEP_REWRITE_TAC[thm1,...], etc., with *)
(* the standard variations (PURE,ONCE,ASM). In addition, tactics *)
(* with LIST instead of ONCE are provided, making 12 tactics in all. *)
(**)
(* The argument theorems thm1,... are typically implications. *)
(* These tactics identify the consequents of the argument theorems, *)
(* and attempt to match these against the current goal. If a match *)
(* is found, the goal is rewritten according to the matched instance *)
(* of the consequent, after which the corresponding hypotheses of *)
(* the argument theorems are added to the goal as new conjuncts on*)
(* the left. *)
(**)
(* Care needs to be taken that the implications will match the goal *)
(* properly, that is, instances where the hypotheses in fact can be *)
(* proven. Also, even more commonly than with REWRITE_TAC, *)
(* the rewriting process may diverge. *)
(**)
(* Each implication theorem for rewriting may have a number of layers *)
(* of universal quantification and implications. At the bottom of*)
(* these layers is the base, which will either be an equality, a *)
(* negation, or a general term. The pattern for matching will be *)
(* the left-hand-side of an equality, the term negated of a negation, *)
(* or the term itself in the third case. The search is top-to-bottom,*)
(* left-to-right, depending on the quantifications of variables. *)
(**)
(* To assist in focusing the matching to useful cases, the goal is*)
(* searched for a subterm matching the pattern. The matching of the *)
(* pattern to subterms is performed by higher-order matching, so for *)
(* example, ``!x. P x`` will match the term ``!n. (n+m) 4*n``. *)
(**)
(* The argument theorems may each be either an implication or not.
