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
<[email protected]
<mailto:[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]
<mailto:[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]
<mailto:[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]
<mailto:[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
<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=48808831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
<mailto:[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/
<http://users.encs.concordia.ca/%7Evincent/>
--
Dr Vincent Aravantinos
Analysis and Design of Dependable Systems
fortiss GmbH <www.fortiss.org/en <http://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 <http://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 list
[email protected] <mailto:[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 <http://www.fortiss.org/en>>
Guerickestrasse 25 | 80805 Munich | Germany
--
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=124407151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
