Re: [isabelle] My unforgivable soundness issue with a locale
Already years ago, I got used to always provide some model for any
locale that contains "final results" of my formalization, just to make
sure that I have not introduced inconsistent assumptions by mistake. And
this is, unfortunately, easier than one may think. E.g., a simple typo
is already enough:
definition P :: "nat => bool" [...]
locale foo = assumes A: "j>0 ==> p j" (* <-- note the lower-case typo
here, p is actually a free variable! *)
inside the locale, you can prove everything you expect with A (and much
more ;) ). Only when interpreting the locale you will realize the
On So, 2013-12-22 at 18:51 +0100, Yannick Duchêne (Hibou57) wrote:
> Hi guys'n gals,
> I feel ashamed now, while I feel it's so funny as much as useful enough to
> be narrated, I'm telling the story here.
> Say I had a local with “assumes A and B”. The most important stuff was in
> A, so I was mainly busy proving theorems derived from A. One of those was
> hard to me (I'm not a guru, and I'm as slow as a snail), and I multiple
> times requested the help of Try/Sledgehammer and others. I was never happy
> with the produced Isar proof, and to make it more clear, I wanted to
> understand one I picked, expecting to make it more readable.
> I was astonished to noticed one of the intermediate goal generated by
> Sledgehammer, should have been impossible to prove according to my intents
> and interpretations of A and B. I forked my investigations toward this new
> case, and discovered I could both prove this goal and disprove it. Yes, I
> could prove P and ¬ P! You guess I was rather frightened, while not
> willing to believe in an Isabelle bug.
> I finally understood: you could only prove ¬ P if you used A and B from
> the locale's premisses and you could only prove P if you used only A and
> don't bother about B; and as you could either bother or not about B, you
> could prove both P and ¬ P one next to the other. So I changed the
> locale's premisses into “assumes B and B ⟹ A” instead of “assumes A and
> B”. I also have to add “using B” in most proofs about A targeting that
> I was doing as if B was implicitly there everywhere; but it's not.
> Moral of the story: don't forget the premisses, it's not enough to have it
> in the locale's “assumes”, it probably also have to be there at the left
> of an ⟹, in some propositions of the “assumes” section.
> By the way, a question aside: is there a way to refer to a proposition
> from another proposition? I mean so that I would not have to copy/paste
> the premiss of “(text of B) ⟹ (text of A)” and just refer to B, as “B ⟹
> (text of A)” instead of the latter.
This archive was generated by a fusion of
Pipermail (Mailman edition) and