Hi Freek,
2012/5/8 Freek Wiedijk <[email protected]>
> HOL_BY really needs to be modified in such a way that this
> thing doesn't happen. But how?
>
>
I would really like to understand HOL_BY better, in order to be able to
improve it. This understanding is some way off, however :)
That said, I have thought of a modification to miz3, as a workaround the
problem we were discussing. The basic idea is the following:
>From what I understand, the "trivial" tactics that get called when after
the tactic specified in by has been called are given at the end of
tactic_of_by, in this snippet:
let (_,_,just as gs) =
((fun g'' ->
let gs' = TIMED_TAC (!timeout) (tac thms) g'' in
if grow then raise (Grown (steps_of_goals g gs'))
else gs') THEN
REPEAT (fun (asl'',_ as g'') ->
if subset asl'' asl' then NO_TAC g''
else FIRST_ASSUM (UNDISCH_TAC o concl) g'') THEN
TRY (FIRST (map ACCEPT_TAC thms'')) THEN
REWRITE_TAC thms'' THEN NO_TAC) g' in
let th = just null_inst [] in
just_cache := (key |-> (0,th)) !just_cache;
gs
The problem now is that if the default prover is run because no tactic was
given explicitly after the "by", we never get to the part after the first
THEN in the above snippet. The reason is that the default prover takes too
long and a Timeout exception is raised. So my idea was simply to handle
Timeout exceptions differently. I defined
let TIMED_TRY_TAC n tac g =
let _ = Unix.alarm n in
try
let gs = tac g in
let _ = Unix.alarm 0 in
gs
with x ->
let _ = Unix.alarm 0 in
ALL_TAC g;;
and then modified tactic_of_by to read
let gs' = TIMED_TRY_TAC (!timeout) (tac thms) g'' in ...
With this modification, I can drop all references to tactics from my
example miz3 proof. The main drawback that I see is that "inference
timeouts" are now indistinguishable from "inference errors". I have no idea
how this workaround interacts with the "Grow" features of miz3.
A cleaner solution might be to have HOL_BY try the "trivial" tactics from
tactic_of_by first. Only if these fail should HOL_BY go on to do its usual
magic. But I don't see yet how to do this.
Cheers,
Felix
--
http://www.felixbreuer.net
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
