Stream: General

Topic: ✔ Changes in match variables not considered when backtrac...

Wolfgang Jeltsch (Nov 08 2021 at 00:27):

I’ve found some odd behavior of match in connection with backtracking.

Consider the following complex approach of proving that True is true:

lemma triviality:
  shows True
  by (
    match TrueE FalseE in elimination: "P ⟹ _" for P ⇒ ‹
      match TrueI in P ⇒ ‹succeed›,
      insert elimination [OF TrueI TrueI]
    ›
  )

The outer match selects TrueE, resulting in elimination being True ⟹ ?P ⟹ ?P and P being True. The inner match succeeds, since P is True. Finally, elimination [OF TrueI TrueI] is inserted, which is True.

Now consider the following variant of the above code, which has an invocation of fail added:

lemma triviality:
  shows True
  by (
    match TrueE FalseE in elimination: "P ⟹ _" for P ⇒ ‹
      match TrueI in P ⇒ ‹succeed›,
      insert elimination [OF TrueI TrueI]
    ›,
    fail
  )

After the activities described above, fail triggers backtracking. The outer match selects FalseE, resulting in elimination being False ⟹ ?P and P being False. The inner match should now fail, causing the whole proof to fail.

However, that is not what happens. Instead, I get the following output:

exception THM 0 raised (line 309 of "drule.ML"):
  OF: no unifiers
  False ⟹ ?P7
  True
  True

Apparently, what happens is the following: After backtracking, the inner match is not re-executed, perhaps because it doesn’t depend on elimination and its dependence on P erroneously isn’t taken into account. As a result, Isabelle attempts to execute insert elimination [OF TrueI TrueI], which has to fail as elimination has False as its sole premise.

Is this really a bug or have I overlooked something?

Kevin Kappelmann (Nov 11 2021 at 11:10):

I am not an expert in that area, but it also seems strange to me. I think this is something that you should post on the mailing list

Wolfgang Jeltsch (Nov 21 2021 at 16:30):

I’ll report this as a bug to the developers.

Notification Bot (Nov 21 2021 at 16:30):

Wolfgang Jeltsch has marked this topic as unresolved.

Notification Bot (Nov 21 2021 at 16:30):

Wolfgang Jeltsch has marked this topic as resolved.

Last updated: Dec 21 2024 at 12:33 UTC