Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue

On Tue, 23 Oct 2012, Tobias Nipkow wrote:

"A conversion is any function that maps a term t to a theorem |-t==u."
LCP, 1983

up to beta-equivalence. Since conversions are low-level proof methods which are sensitive to the precise term structure, this is a wart that causes non-modularity. This non-modularity only shows up (to refine Brian's analysis) if the lhs of the rewrite rule has a free variable F in an applied position: F t. This does not happen very often, but if it does, rewr_conv should still behave nicely. It should do a non-normalizing instantiation followed by a beta-normalization.

Alternatively one could do the normalization before on the input term. Empirically, higher-order matching can produce surprises if applied to terms with beta redexes, it normally is never used like that in the existing tools. So it is better not to give non-normal stuff to the match operation.

Again, I don't expect too many fundamental problems in this rather small incident, but one has to approach it with the proper mindset about how the Isabelle code base (and its history) works.

(Next time I will tell a story how an efficient and fully verified merge-sort function included in the core sources caused several days of worries.)


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