Hi Michael,
Thank you for the pointers.
I tried match_term on the goal, and it succeeds. With show_types := true,
the goal I get is:
``SPEC (x :(arm_state, arm_el, FullAddress # FullAddress) processor)
(aPC (offset :FullAddress) * (p :arm_set -> bool))
((c1 :FullAddress reln) ∪ (c2 :FullAddress reln))
(aPC (offset'' :FullAddress) * (s' :arm_set -> bool)) ⇒
SPEC x (aPC offset * p) (c1 ∪ c2) (aPC offset'' * s')``
so it looks like the types are correct from the printed types as well.
I tried to clear the assumption list by appending "THEN (POP_ASSUM (K
ALL_TAC))" to my current list of tactics, but it doesn't clear any of the
assumptions. I tried using "THEN (POP_ASSUM MP_TAC)" (in place of "K
ALL_TAC") as well, and it only adds one of the 6 assumptions as an
antecedent to the goal.
The current proof steps I have are (apologies for the verbosity):
(ONCE_REWRITE_TAC [ind_cases])
THEN (REPEAT STRIP_TAC)
THEN etac21 THEN (REPEAT STRIP_TAC) THEN DISJ2_TAC THEN DISJ1_TAC
THEN etac22 THEN (REWRITE_TAC [STAR_ASSOC])
THEN (ONCE_ASM_REWRITE_TAC []) THEN (ONCE_ASM_REWRITE_TAC [])
THEN (SIMP_TAC std_ss [SEP_IMP_REFL])
THEN (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'`])))
THEN (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`])))
THEN (FULL_SIMP_TAC std_ss [SEP_IMP_REFL, SPEC_WEAKEN])
THEN (ASSUME_TAC sw_thm)
THEN (`SEP_IMP (aPC offset'' * r) (aPC offset'' * s')` by (METIS_TAC
[]))
THEN (Q.PAT_ASSUM `aaa ==> bbb ==> ccc` MP_TAC)
THEN (ONCE_ASM_REWRITE_TAC [])
THEN (ONCE_ASM_REWRITE_TAC [])
THEN (ONCE_ASM_REWRITE_TAC [])
THEN (POP_ASSUM (K ALL_TAC))
This goal is part of a larger proof on an inductively defined relation, so
the two Q.PAT_ASSUM's in the middle instantiate the inductive hypothesis so
that I can prove some of the goals. I'm not sure if the calls to
Q.PAT_ASSUM followed by the simplification using FULL_SIMP_TAC, and then
the subsequent ASSUME_TAC followed by the rewrites, are causing any issues
(or are logically incorrect/unsound). After (show_types := true), the
instantiated inductive hypotheses have the correct types and I am able to
discharge the relevant conjuncts in the goal.
sw_thm in the ASSUME_TAC is the exact statement of the ``A ==> A`` theorem
specialized from another theorem.
Thank you again!
Regards,
Jiaqi
P.S. Apologies for the somewhat repeated post to hol-info ("Problems with
METIS_TAC: Crashing with exception raised in CHOOSE"), it is the same issue
as this, I had found some extra information from increasing the trace level
for metis.
On Tue, Sep 9, 2014 at 12:04 AM, Michael Norrish <
michael.norr...@nicta.com.au> wrote:
> 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
