Re: [Hol-info] New tactic: IMP_REWRITE_TAC

[Michael Norrish]

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] Learning HOL Light

[Bill Richter]

Thanks, John!  I'll read p 34 more carefully. Your example shows the behavior 
I'd want from REWRITE_TAC.  You theorem is 
# ADD_AC;;
val it : thm =
  |- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p

This is a good exercise for my right associativity skill.  and that's what it 
takes to prove your 

  `(x + 1) + y + z = z + (1 + y) + x`
 
I'd guess that REWRITE_TAC did 

(x + 1) + y + z = (y + z) + x + 1 = (z + y) + x + 1 = z + y + x + 1

= z + y + 1 + x = z + (y + 1) + x = z + (1 + y) + x 

using the 1st, 3rd, 2nd, 1st, 2nd  1st clauses of ADD_AC respectively.  That's 
a nice example of the power of REWRITE_TAC.  But my example was quite 
different, I think.  REWRITE_TAC[DIST_SYM] did exactly what I wanted, 
symmetrizing only the middle of three dist expressions
 `∀x e x'.
  dist (x,x')  e
  ⇒ (∃e'. 0  e' ∧ (∀x''. dist (x'',x')  e' ⇒ dist (x,x'')  e))`

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?

BTW I think there isn't an pdf available for Ursula Martin and Tobias Nipkow's 
paper, 
http://www21.in.tum.de/~nipkow/pubs/cade90.html
But it sounds pretty complicated. 

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. 

-- 
Best,
Bill 

--
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