Re: [isabelle] Strange eta-expansion on induction



On Fri, 2 Mar 2012, Peter Lammich wrote:

As Tobias points out, the Pure Isabelle system conceptually works modulo
eta (and beta and alpha) conversion -- although there are well known
traps.  So to continue the thread, I would also like to see the other part
-- the proof tool by Peter that fails here.

It's no custom "proof tool" involved here. My setting is roughly like
this:

I have assertions of type "heap => addr set => bool", and hoare-tripels
of type "assertion => program => assertion => bool" (syntax: {P} S {Q})

I defined the assertion
 definition [simp]: "false h as == False"

Moreover, I have a rule
 lemma [simp]: "{false} S {Q}"

The proof that fails has the form:
 lemma "{is_list xs p} S Q" proof (induct xs arbitrary: p)
   case Nil show ?case by (cases p, simp_all)
   ...

Here, depending on the case for p, "is_list [] p" simplifies to false, which is then simplified to \lambda _ _. False, before the rule for {false} S {Q} is applied.

This is the normal order of things. Combinations of simplification with rule applications of the resolution family (intro/elim/dest) can lead to eta-expansion and thus more reductions than first anticipated.

The above simpset is a bit fragile in that sense, as you have observed already. If you do not want to add more rules, but want to retain control of lambda equivalences, you can try to wrap up some App or Abs nodes in auxiliary operators; similar to Collect/member for 'a set in HOL.


	Makarius





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