Re: [isabelle] blast looping and backtracking



Dear Kevin, thanks for an interesting email. In fact it turns out that

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

loops right out of the box. Why is this?

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.

Larry Paulson


> On 26 Nov 2021, at 09:34, Kevin Kappelmann <kevin.kappelmann at tum.de> wrote:
> 
> Dear 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:
> 
> ```isabelle
> 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
> 1. the elim rule is applied
> 2. the first subgoal closed by the intro rule
> 3. the second subgoal cannot be closed and backtracking occurs
> 4. repeat with 1.
> 
> 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:
> 
> ```isabelle
> 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*)
> ```






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.