[isabelle-dev] [isabelle] safe for boolean equality

[Lawrence Paulson]

This is quite an interesting example.

The reason for discarding the equality is that these simple tactics work by repetition. if the equality is retained, then the procedure will loop. One could imagine a more refined procedure that maintained a list of variables that had undergone substitutions, and perhaps this option could be investigated. But I suspect that such a fundamental change in such a commonly used tactic would have widespread effects.

Altering the behaviour of the safe method on locale constants might be feasible, because it would affect only a few proofs. Can anybody tell me whether there is an easy way to identify whether a free variable is actually a locale constant?

Larry

On 14 Jun 2010, at 16:36, Thomas Sewell wrote:

> The variable elimination code is not only unsafe in the presence of context-wide variables (variables from locales, fixed in structured proofs, or mentioned in named assumptions). Variable elimination of local variables in the presence of schematic variables (?P etc) can also transform provable goals into unprovable ones.
> 
> lemma "EX x. x = fst y"
>  apply (rule exI)
>  (* goal still provable *)
>  apply (cases y)
>  (* goal still provable *)
>  apply safe
>  (* goal not provable *)
>  oops
> 
> Could we fix the problem by simply not discarding the equality after rewriting the constant? I can't see any general reason why keeping the expression "X = ..." in the assumptions should impact the proof much once X is mentioned nowhere else. It might clutter the assumptions, but it would also supply genuinely helpful information - I've sometimes spent more than ten minutes staring at a goal trying to figure out how it relates to the input problem I supplied before realising that I'm looking at the case where X = Y.
> 
> Yours,
>    Thomas.
> 
> ___________________________________
> From: isabelle-dev-bounces at mailbroy.informatik.tu-muenchen.de [isabelle-dev-bounces at mailbroy.informatik.tu-muenchen.de] On Behalf Of Lawrence Paulson [lp15 at cam.ac.uk]
> Sent: Tuesday, June 15, 2010 1:12 AM
> To: Brian Huffman
> Cc: isabelle-users; isabelle-dev Isabelle; Viorel Preoteasa
> Subject: Re: [isabelle-dev] [isabelle] safe for boolean equality
> 
> Equalities involving constants have never been eliminated in this way. The equality must involve a variable, free or bound. The method has no way of knowing about constraints on the variable that are not part of the goal. In the case of a structured proof, it would be appropriate and natural to insert relevant inequalities with an appropriate “using” clause.
> 
> The problem with locale constants is that they look like free variables to this 15 year old code. We need to look at whether there is a way for this code to identify locale constants and to treat them as such.
> 
> Larry Paulson
> 
> 
> On 14 Jun 2010, at 15:24, Brian Huffman wrote:
> 
>> The problem is that safe tries to be helpful by eliminating equalities
>> from the assumptions, unfolding them in the rest of the subgoal. In
>> this case the assumption "(op l-> ) = (op r->)" in goal 2 is
>> eliminated; since "op |->" does not appear in the rest of the subgoal,
>> the equality just goes away. This is often a reasonable behavior for
>> free variables, but it is NOT generally safe for variables fixed in
>> locales or structured proofs, and it is certainly not generally safe
>> for constants. This undesirable behavior has been noted before on the
>> list, and I would consider it a bug.
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.