*To*: Kevin Kappelmann <kevin.kappelmann at tum.de>*Subject*: Re: [isabelle] blast looping and backtracking*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 26 Nov 2021 10:57:48 +0000*Accept-language*: en-GB, en-US*Arc-authentication-results*: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=cam.ac.uk; dmarc=pass action=none header.from=cam.ac.uk; dkim=pass header.d=cam.ac.uk; arc=none*Arc-message-signature*: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=4JtsgNM4kUYLcS47TSGgpQ377fDNsGzNsuZxhTiqExw=; b=g5rL2vvbo5jpPSTm8eyk1mJAeu9HC8+SWny8ZvYPi6xa0HpW7rChH8ysSQSGQyjE0v/Q8D4SOWdR8xo+70eJHq1o5a3CtXpgALdPih9Q0QkKi7J03ZBmHzaTtgaX4s4Xy40vhtxOrfihVGYgGwNwkTmsaOqJ8bR/wF2CGuL1MRiMrZIMui+8DEJyXTEhm9+mCRZ1jicclSvkTzBuDBalUlh3kuJRrDEkuSYFEZCB/IbcCjkL1pC3OGB6YEWiPB04Htk6gK7ypb/kmquCbaKGIqIn8X03OYkKHt3GH1KXiu4Fzm3MmqFd8KtmSP6YXvQ481h8A4agUymp5ZN77l8T4g==*Arc-seal*: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=WKaILgFEwTI/fmaoFENKrSJ6mIiHIdKx/AghbDNkZy3/ITXKUof1QAbbkaXERvhQc7/uOBNlrgAVGB1ZkNySPk412kZfcwACp5FgVy2rpNGDs8cWxlD9aJI25MIAycryj97Zh3FRpkfwC1UVBrmx+6QN7bjf9LDuPtOmWgKZAX2C0RzHVZmHZvGCw8DmSSq36+tr+4N1YslHsQqxisNZiLN/XR+6uh2L9QVw71GSPJ9PvgHRWUgv+KNROyZOR6w4JXyNs/BZO1c4NnV2Fv0B+FHaUs0yewKLYc1NKVHUTbahUUVbP9NIkAiIpqPx84LkEOzKGnwf2+xg8+zXdMRSFw==*Authentication-results*: cam.ac.uk; iprev=pass (mail-cwlgbr01lp2054.outbound.protection.outlook.com) smtp.remote-ip=104.47.20.54; spf=pass smtp.mailfrom=cam.ac.uk; dkim=pass header.d=UniversityOfCambridgeCloud.onmicrosoft.com header.s=selector2-UniversityOfCambridgeCloud-onmicrosoft-com header.a=rsa-sha256; arc=pass (i=1) header.s=arcselector9901 arc.oldest-pass=1 smtp.remote-ip=104.47.20.54*Authentication-results*: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=cam.ac.uk;*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <8cc47c10-5323-c4d4-d68a-5a6f109d804a@tum.de>*References*: <8cc47c10-5323-c4d4-d68a-5a6f109d804a@tum.de>*Thread-index*: AQHX4qmdVU0VMV5jQk2UQe6vrWoqU6wVo5IA*Thread-topic*: [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*) > ```

**Follow-Ups**:**Re: [isabelle] blast looping and backtracking***From:*Kevin Kappelmann

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

- Previous by Date: [isabelle] New in the AFP: van Emde Boas Trees
- Next by Date: [isabelle] New in the AFP: Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL
- Previous by Thread: [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