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

[Michael N. <mic...@ni...>]

On 09/09/14 15:07, Jiaqi Tan wrote:
> 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.

If you want to get rid of them all, you will need to do

  REPEAT (POP_ASSUM (K ALL_TAC))

I only suggested the non-repeated version so that you could pop them off one at
a time to see when METIS_TAC started to work.

> The current proof steps I have are (apologies for the verbosity): ...

> 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.

I guess you probably have found a bug in METIS_TAC.

Does PROVE_TAC solve the goal?

Michael

________________________________

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.