Hi,
I have a question about the internals of METIS_TAC, whether my proof
succeeded, and whether there might be problems with trying to prove my
theorem with METIS_TAC.
I set the trace for METIS_TAC to 5, and in the trace feedback, the last
line of the proof from the METIS feedback was:
(11) |- F
[Resolve
{res = ~set_sep.SEP_IMP (set_sep.STAR (prog_arm.aPC offset'') r) s,
pos = (9), neg = (10)}]
END OF PROOF
Does this mean that my proof succeeded?
At the same time, I also got the following error at the end of METIS_TAC:
metis: proof translation time: 0.233517
Exception-
HOL_ERR
{message = "", origin_function = "CHOOSE", origin_structure = "Thm"}
raised
Is the error occurring during the proof process, or is the error occurring
during the post-processing to generate the theorem after the proof was
completed?
I also get the same problem when, instead of METIS_TAC, I use REWRITE_TAC
or SIMP_TAC using the same theorem list passed to METIS_TAC, although I
also received the same trace/feedback messages from METIS_TAC when I used
REWRITE_TAC/SIMP_TAC so presumably it was because REWRITE_TAC/SIMP_TAC were
also using METIS_TAC internally?
Thank you!
Regards,
Jiaqi
------------------------------------------------------------------------------
Want excitement?
Manually upgrade your production database.
When you want reliability, choose Perforce.
Perforce version control. Predictably reliable.
http://pubads.g.doubleclick.net/gampad/clk?id=157508191&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
