Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.



I’m not aware of a change, but it’s possible.

There is a trade-off here: on the one hand, these constraints can accumulate excessively, causing performance problems and making the subgoals unreadable. But on the other hand, eliminating them in the obvious way (using constant functions) destroys information.

If you get these constraints in a proof, even if it currently works, it might be a good idea to look for a different proof (by explicitly instantiating a variable that is currently left uninstantiated) to get rid of them yourself.

Larry Paulson


On 8 Dec 2013, at 04:23, David Greenaway <David.Greenaway at nicta.com.au> wrote:

> Hi all,
> 
> While updating some large proofs to Isabelle2013-1, I discovered
> a change in the behaviour of "blast" in the presence of flex-flex pairs.
> In particular, in Isabelle2013-1, "apply blast" appears to eliminate
> flex-flex pairs, even if the particular goal blast is working on doesn't
> actually involve any schematics. This can make the larger theorem being
> worked on unprovable.
> 
> For example, consider the following snippet:
> 
>    (* Silly lemma to generate a flex-flex pair. *)
>    schematic_lemma "!!x y a b. (1 = 1) & f ((x = y) = (a = b)) = ?P x y a b"
>      apply (subst (1 3) eq_commute)
>      apply (rule conjI)
>       (* Two subgoals exist; only the second involves schematics. *)
>       apply blast
> 
> In Isabelle2013 the "apply blast" would leave the flex-flex constraints
> unchanged. In Isabelle2013-1 and Isabelle2013-2, the constraint
> disappears. In more complex proofs, this can make finishing the proof
> impossible.
> 
> Is this behaviour of Isabelle2013-1/2 expected, or is it a regression?
> 
> (I don't have a good grasp on the finer points of higher order
> unification and flex-flex constraints, so please forgive me if I am
> using incorrect terminology.)
> 
> Cheers,
> David
> 
> 
> 
> ________________________________
> 
> 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.
> 





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