*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] blast looping and backtracking*From*: Kevin Kappelmann <kevin.kappelmann at tum.de>*Date*: Fri, 26 Nov 2021 12:07:38 +0100*Authentication-results*: cam.ac.uk; iprev=pass (postout1.mail.lrz.de) smtp.remote-ip=129.187.255.137; spf=pass smtp.mailfrom=tum.de; dkim=pass header.d=tum.de header.s=postout header.a=rsa-sha256; arc=none*Authentication-results*: postout.lrz.de (amavisd-new); dkim=pass (2048-bit key) reason="pass (just generated, assumed good)" header.d=tum.de*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4A5519F8-082C-4563-AEA7-6AEFD3FF7662@cam.ac.uk>*References*: <8cc47c10-5323-c4d4-d68a-5a6f109d804a@tum.de> <4A5519F8-082C-4563-AEA7-6AEFD3FF7662@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.14.0

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. Kevin On 26.11.21 11:57, Lawrence Paulson wrote: > 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*) >> ``` > > > >

**Follow-Ups**:**Re: [isabelle] blast looping and backtracking***From:*Lawrence Paulson

**References**:**[isabelle] blast looping and backtracking***From:*Kevin Kappelmann

**Re: [isabelle] blast looping and backtracking***From:*Lawrence Paulson

- Previous by Date: [isabelle] New in the AFP: Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL
- Next by Date: Re: [isabelle] blast looping and backtracking
- Previous by Thread: Re: [isabelle] blast looping and backtracking
- Next by Thread: Re: [isabelle] blast looping and backtracking
- Cl-isabelle-users November 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list