Re: [isabelle] My unforgivable soundness issue with a locale



Hi.

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


Best,
  Peter


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






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