Re: [isabelle] Product_Type.split_beta fails

On Wed, 30 Oct 2013, Ognjen Maric wrote:

I'm getting exceptions from the split_beta simproc which propagate to
the "user-level" (Isabelle 2013). Here's a minimal example:

lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))"
 using [[simp_depth_limit=0]]

This results in:
*** Proof failed.
*** (case :000 of (x, y) \<Rightarrow> c) = c
***  1. (case :000 of (x, y) \<Rightarrow> c) = c
*** The error(s) above occurred for the goal statement:
*** (case :000 of (x, y) \<Rightarrow> c) = c

Setting the depth limit to 2 or higher makes the error go away. Glancing at the simproc, it seems that its local function "meta_eq" assumes that rewriting with just "cond_split_eta" will work, but this fails at low simp depths.

Thanks for working out a well-defined example for this incident.

This thread was left open over several months, because nobody felt responsible for a simproc that David von Oheimb made in 1998. But the problem here is not the simproc, it is the Simplifier context in Isabelle2013 (and Isabelle2013-2).

Reductionism is the great fallacy of modern science, and I almost fell on the nose myself by "fixing" the simproc, although it is not at fault. It is merely an indicator of a problem somewhere else --- there is no need to blame the messenger for a bad message.

The real problem behind the incident above is "localization" of the Simplifier, or rather lack thereof. That important and complex tool still had its own "simpset" over a long time, with unclear relation to the all-important Proof.context that is uniform for all tools (and allows tools to cooperate robustly in the first place, if done right).

The mistake above is due to the Simplifier "depth" field: it ended up semantically as part of the context, but seems to belong to the simpset instead. Thus nested tools like the split_eta and split_beta simprocs may provide a fresh environment for their own simplification business.

Just some weeks ago, I discovered some other incoherence in the "params" management of the Simplifier: that field belongs into the context, not the simpset.

Conclusion: it should work better again in the coming Isabelle2014 release (summer 2014).


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