The standard issue with problems like these is a difference in types. Have you
tried examining the goal with show_types on?
Do
show_types := true;
and reprint the goal? Do you really have an instance of A ==> A?
You can also do the following:
match_term ``A ==> A`` (#2 (top_goal());
that will fail (unhelpfully) if the goal isn't an instance of A ==> A, but will
succeed with an instantiation for A if it is. If it is, then METIS_TAC is
presumably being confused by one of your assumptions. If so, try deleting
assumptions (use POP_ASSUM (K ALL_TAC)) until METIS_TAC does manage to prove it.
I hope this helps.
Feel free to report back if you still have trouble tracking down the problem.
It is also quite possible that there is a bug in METIS_TAC of course.
Michael
On 08/09/14 16:20, Jiaqi Tan wrote:
> Hi,
>
> I have the following goal (using the theorems in examples/machine-code) in
> HOL4
> which I am trying to prove:
>
> val mw2 =
> ([([``SEP_IMP (aPC offset'' * r) (aPC offset'' * s')``,
> ``(s = aPC offset'' * s') ∧ SEP_IMP (aPC offset'' * r) s ⇒
> SPEC2 x (aPC offset' * q) c2 (aPC offset'' * s')``,
> ``(q' = aPC offset' * q) ∧ SEP_IMP (aPC offset' * q) q' ⇒
> SPEC2 x (aPC offset * p) c1 (aPC offset' * q)``,
> ``SEP_IMP (aPC offset'' * r) s``,
> ``s = aPC offset'' * s'``,
> ``SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * r)``,
> ``q' = aPC offset' * q``],
> ``SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s') ⇒
> SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s')``)],
> fn): goal list * validation
>
> The goal is "SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s') ⇒
> SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s')", which appears to be
> true (by one of the conjuncts in boolTheory.IMP_CLAUSES), but I am unable to
> prove it.
>
> When I run "METIS_TAC []" on this goal interactively (by typing it in) from
> the
> HOL shell, I get "[.....] |- SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' *
> s') ⇒ SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s')", and when I run
> "METIS_TAC []" by pasting it into the shell (as the last tactic in my list of
> THEN'ed tactics), I get the error:
> "Exception-
> HOL_ERR
> {message = "", origin_function = "CHOOSE", origin_structure = "Thm"} raised
> "
>
> Two of my tactics before reaching the above state are:
>
> (Q.PAT_ASSUM `! aaa . ?bbb ccc . ddd /\ SEP_IMP (aPC offset' * q) s ==> eee`
> ((Q.X_CHOOSE_THEN `q` (Q.X_CHOOSE_TAC `offset'`)) o (Q.SPECL [`q'`])))
>
> and
>
> (Q.PAT_ASSUM `! aaa . ?bbb ccc . ddd /\ SEP_IMP (aPC offset'' * r) s ==> eee`
> ((Q.X_CHOOSE_THEN `s'` (Q.X_CHOOSE_TAC `offset''`)) o (Q.SPECL [`s`])))
>
> Could the Q.PAT_ASSUM (or X_CHOOSE_TAC) be causing problems? When I call
> Q.PAT_ASSUM and I use X_CHOOSE_TAC to instantiate existentially quantified
> variables with some variable, does that add extra assumptions to the theorem
> being selected from the assumptions before adding it to the goals?
>
> 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
>
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
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
