On 17.02.2014 12:49, Bill Richter wrote: > Vince, this is very interesting: > > 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''). > > Ah, that's why it worked! I was really puzzled. But doesn't that mean you > won't ever use REWRITE_TAC or SIMP_TAC, as John's actual algorithm (or > Tobias's) might be published but isn't explained in the documentation? Mhh, no. What is bad is to rely on some particular feature which is undocumented. The fact is that the actual specification is pretty loose: REWRITE_TAC claims it will rewrite some things according to the theorems you give it. But this is extremely vague: it does not actually tell you which strategy it is going to use. And there can be several. Most of the time, the strategy choice actually yields the same result. But, from time to time, it actually makes a difference like in your example. In such a case - if aware of it - it is better to avoid relying on such "features" in my opinion.
> I mean, I use REWRITE_TAC, MESON_TAC and SIMP_TAC all the time, rarely > knowing in advance which one will work. Mff. That's bad! :-) Do you mean you don't know the technical differences between them? or that you know them but don't necessarily know which impact it has on their behaviour? Or that you are really trying them completely randomly? > Two quick notes: > > The ONCE_REWRITE_TAC approach was John's original code, and it did what John > intended. Oh you mean he really wanted to switch *all* the dist? Then ok I did not check the proof carefully. Often people use ONCE_REWRITE_TAC because they actually just want one position to change but don't care that the tactic also changes the other positions. > That's really cool, that you discovered that DIST_SYM can be moved to the > MESON_TAC theorem list (how did I miss that???), and that works for my > readable.ml code (and thanks again for helping me write it) > > let OPEN_BALL = theorem `; > ∀x e. open (ball (x,e)) > > proof > rewrite open_def ball IN_ELIM_THM; > fol DIST_SYM REAL_SUB_LT REAL_LT_SUB_LADD REAL_ADD_SYM REAL_LET_TRANS > DIST_TRIANGLE; > qed; > `;; > > Note that my version runs about as long as yours > > 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]);; > > and that John's original version is about 160 times faster :) > > let OPEN_BALL = prove > (`!x e. open(ball(x,e))`, > REWRITE_TAC[open_def; ball; IN_ELIM_THM] THEN ONCE_REWRITE_TAC[DIST_SYM] > THEN > MESON_TAC[REAL_SUB_LT; REAL_LT_SUB_LADD; REAL_ADD_SYM; REAL_LET_TRANS; > DIST_TRIANGLE_ALT]);; > Yes that is its disadvantage: that's the price you pay for getting more intelligence from HOL Light :-) -- 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 ------------------------------------------------------------------------------ Managing the Performance of Cloud-Based Applications Take advantage of what the Cloud has to offer - Avoid Common Pitfalls. Read the Whitepaper. http://pubads.g.doubleclick.net/gampad/clk?id=121054471&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
