On 14.02.2014 04:39, Bill Richter wrote:
> I guess I understood that REWRITE_TAC used a complicated algorithm in order
> to avoid infinite looping. So I think I didn't express my question very
> well. I tend to think that it's not good coding on my part to rely on
> features that I don't even understand. I would think that the only sensible
> way to handle my code above was to find a different way of solving the
> problem, such as your solution of using ONCE_REWRITE_TAC to symmetry all
> three dist expressions. Any thoughts? For instance, isn't it possible that
> you would change the REWRITE_TAC algorithm?
> In any case, thanks, as you answered my question: this behavior of
> REWRITE_TAC that I didn't understand is caused by REWRITE_TAC being quite
> ingenious and complicated! That's a perfectly acceptable answer to me right
> now.
Hi Bill,
I would say what is bad coding is not to rely on features you don't
understand but on features that are actually undocumented/unintended.
Here, the ordering chosen is indeed ingenious to prevent some often-met
looping situations.
However, as John pointed out it is also completely arbitrary (in your
case it just applies the rewrite you wanted because Ocaml orders symbols
as follows: x < x' < x'').
So the fact that you obtained what you wanted is completely random and
not actually based on the ingenuity of the tactic.
In particular, if the Ocaml implementors decide randomly to change the
order of strings then the script does not work anymore.
So ONCE_REWRITE_TAC is indeed better here. But I personally still don't
like it so much since it does not really reflect your intention:
your intention is to rewrite the middle "dist", not to rewrite "once".
So a better solution would be to use GEN_REWRITE_TAC as you know, or
PATH_CONV.
However I still don't like these ones so much since they force you to
give precise information about the location of the rewrite.
This is, first, annoying, and second, can break easily if ever you
change later on some definitions (the sequence of xxx_CONV given to
GEN_REWRITE_TAC could slightly change).
So actually, the best version in my opinion is just to give DIST_SYM to
MESON_TAC:
let OPEN_BALL = prove
(`!x e. open(ball(x,e))`,
REWRITE_TAC[open_def; ball; IN_ELIM_THM] THEN
MESON_TAC[DIST_SYM; REAL_SUB_LT; REAL_LT_SUB_LADD; REAL_ADD_SYM;
REAL_LET_TRANS; DIST_TRIANGLE_ALT]);;
Then you don't even have to care about technical details like the number
or the position of rewrites.
Note that - sorry to insist on it again... - the library that I've been
advertising a couple of times, https://github.com/aravantv/impconv,
provides a tactic specially intended to provide a nice solution to this
sort of problem: TARGET_REWRITE_TAC.
It is an attempt and does not claim to solve everything (and, in
particular, is inefficient as soon as you give it too many theorems) but
it gives an idea of a possible direction to go to obtain a solution
that, for me, would be perfect.
"TARGET_REWRITE_TAC ths th" tries all possible rewrites on every
possible path using the theorems in the list ths, and picks the first
rewrite which allows to obtain a goal where we can apply th.
If that's not clear I refer to the manual of the library, which also
contains examples.
The overall idea is to change from the question "Where do I want my
rewrite to apply?" or "How many times do I want my rewrite to apply?" to
"For which purpose do I want my rewrite to apply?".
To the former questions you answer informally by "in the middle dist
term" or by "1 time", whereas for the latter you answer "in order to
rewrite using the theorem th".
It follows better the intention of the human behind the proof and does
not require that you give technical information like the position or the
number of rewrites.
In your example, the purpose of the rewrite is to apply the triangular
inequality, i.e., DIST_TRIANGLE, so one would ideally write
TARGET_REWRITE_TAC [DIST_SYM] DIST_TRIANGLE
(which means informally "try every single rewrite with DIST_SYM - in
first position, in the middle, in the last position - and pick the one
that allows to make use of DIST_TRIANGLE").
In your example this is not enough actually since rewriting with
DIST_SYM does not allow to rewrite immediately with DIST_TRIANGLE: you
also need quite a bunch of intermediate theorems like REAL_SUB_LT,
REAL_LET_TRANS, etc.
So you should give these theorems to TARGET_REWRITE_TAC as follows:
TARGET_REWRITE_TAC [DIST_SYM; REAL_SUB_LT; REAL_LET_TRANS; ...]
DIST_TRIANGLE
Unfortunately this particular case is way too complex that
TARGET_REWRITE_TAC can handle... :-(
But it still demonstrates the motivation behind TARGET_REWRITE_TAC.
Cheers,
V.
--
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
