[isabelle] My unforgivable soundness issue with a locale



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 locale.

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.

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





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