Re: [Hol-info] Problem trying to prove "A ==> A": Error from CHOOSE

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

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 <
mic...@ni...> 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...@li...
> > 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.
>