[isabelle] blast looping and backtracking · Mirror: Isabelle Users Mailing List

I like to tag unconditional facts (0 < 1, X ⊆ X, x ∈ {x}) as
[intro!] rules. In combination with a suitable elim rule and goal
statement, this lead to a looping behaviour of blast that I did not
expect. Here is a minimal, contrived example:

definition "P x ≡ True"

lemma [intro]: "P x"
  unfolding P_def ..

lemma [elim]:
  assumes "True"
  obtains "¬(P x)" | "P x"
  (*if we were to swap the order of the cases, blast does not loop*)
  (*obtains "P x" | "¬(P x)"*)
  by blast

lemma "True ⟹ False"
  by blast (*loops*)

Looking at the output of blast (

setup "Config.put_global Blast.trace
true"

), it seems to me that

If, as written in the comment above, we were to swap the order of the
cases in the elim-rule, blast will not loop. Is this the expected
behaviour of blast? I would have expected that the elim-rule will not be
applied again after backtracking occurs.

For the sake of completeness, here is a more realistic example of the
same problem:

declare insertI1[intro] (*"a ∈ insert a A"*)
(*subsetCE is already declared as [elim] in the distro*)
declare subsetCE[elim] (*A ⊆ B ⟹ (c ∉ A ⟹ Q) ⟹ (c ∈ B ⟹ Q) ⟹ Q*)

lemma "(∀X. X ⊆ X) ⟹ 1 + 1 = 2"
  by blast (*loops*)

Email Gateway (Nov 26 2021 at 10:58):

From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Kevin, thanks for an interesting email. In fact it turns out that

Blast doesn’t know anything about arithmetic, so it’s unable to prove 1 + 1 = 2. It will look at the assumptions and see that quantified formula, which it will try to use, creating instances of the form ?A ⊆ ?A, which are in effect other quantified formulas, giving blast lots of things to try. But of course, the assumption is equivalent to true and can’t prove anything.

Blast isn’t a decision procedure and you should kill it if it doesn’t succeed in a couple of seconds.

You should be cautious about tagging facts like the ones you list (0 < 1, X ⊆ X, x ∈ {x}), simply because they refer to built-in primitives where the existing setup has undergone years of tuning (the set primitives in particular). By all means tag facts related to constants that lie further from the core, if that makes sense. But in fact it is quite easy to get blast to loop.

Email Gateway (Nov 26 2021 at 11:08):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Thanks Larry - do you also happen to know why blast stops looping if we
were to swap the cases in the first example I posted? That would maybe
help me to tag lemmas in a way that makes auto and blast more predictable.

Email Gateway (Nov 26 2021 at 11:19):

From: Lawrence Paulson <lp15@cam.ac.uk>
I don’t think that there is a simple explanation. In general, blast is an instance of a sort of technology that will keep trying if there is anything it can do, and therefore can be expected to loop rather than to terminate with failure.

It would be more concerning to see examples that loop even though there is a proof (in logic, not something involving arithmetic say). And I am sure such examples also exist.

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] blast looping and backtracking

Email Gateway (Nov 26 2021 at 09:35):

Email Gateway (Nov 26 2021 at 10:58):

Email Gateway (Nov 26 2021 at 11:08):

Email Gateway (Nov 26 2021 at 11:19):