Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Product_Type.split_beta fails


view this post on Zulip Email Gateway (Aug 19 2022 at 12:16):

From: Ognjen Maric <ognjen.maric@gmail.com>
Hi all,

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]]
apply(simp)

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.

Cheers,
Ognjen

view this post on Zulip Email Gateway (Aug 19 2022 at 13:47):

From: Makarius <makarius@sketis.net>
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).

Makarius


Last updated: Mar 28 2024 at 12:29 UTC