Search code examples
isabelle

Using prefer_tac correctly

I'm currently failing to figure out how to use prefer_tac correctly. (Isabelle2019 Linux)

I'm doing the following (minimum working example):

theory MWE
imports
  Main
begin

lemma "False ∧ True ∧ A"
  apply (intro conjI)
    apply (tactic ‹prefer_tac 2›) (* Exception *)
    apply (tactic ‹SELECT_GOAL all_tac 2 THEN prefer_tac 2›) (* Works *)
  oops

end

I get a exception for the first prefer_tac call (state at first call):

proof (prove)
goal (3 subgoals):
 1. False
 2. True
 3. A 
exception Subscript raised (line 75 of "./basis/List.sml")

while I would expect it to just work. Why does it not? I'm sorry if this has some trivial reason. I'm really not an expert with Isabelle's internals.

The second call works. State at second call:

proof (prove)
goal (3 subgoals):
 1. True
 2. False
 3. A

I'm asking myself why this works. Which invisible effect does the SELECT_GOAL call have so that prefer_tac then works? I thought that SELECT_GOAL selects the second goal solely for the invocation of all_tac?

As a side note (I should probably write this to the mailing list) in the function permute_prems (thm.ML) List.take has an exception handler, but List.drop doesn't. This looks odd to me. This shouldn't have anything to do with my problem, because then I would just get a nicer error message.

Solution

  • I did not investigate the problem in detail. However, upon the first call from apply (tactic ‹...›), the tactic is called on a dummy pattern (see this post on the mailing list for details). Upon receiving the dummy pattern, Thm.permute_prems throws an exception which is not handled by prefer_tac. Usually (but not always), tactics are expected to return an empty result sequence upon failure (see section 4.2 in the Isabelle/Isar implementation manual). Upon the first call of SELECT_GOAL all_tac 2... the dummy pattern that all_tac receives does not result in an exception and it passes only the valid goals to the prefer_tac.

    It is difficult for me to say whether there was a reason for admitting an unhandled exception in the prefer_tac. However, you can easily modify the original specification of the tactic prefer_tac to ensure that it does not throw an exception and returns an empty result sequence in the case of a failure:

    ML‹
fun prefer_tac' i thm = thm
  |> PRIMITIVE (Thm.permute_prems (i - 1) 1 #> Thm.permute_prems 0 ~1)
  handle Subscript => Seq.empty;
  (* of course, you can add other exceptions if necessary *)
›

lemma "False ∧ True ∧ A"
  apply (intro conjI)
  apply (tactic ‹prefer_tac' 2›) (* Works *)
  oops

    Remarks:

    As a side note (I should probably write this to the mailing list) in the function permute_prems (thm.ML) List.take has an exception handler, but List.drop doesn't. This looks odd to me. This shouldn't have anything to do with my problem, because then I would just get a nicer error message.

    Indeed, this seems slightly odd and may be worth mentioning on the mailing list. However, I am also far from being knowledgeable about the implementation details of Isabelle.

    Isabelle version: Isabelle2020