Re: [isabelle] Let and commutative rewrite rules

On 08/05/2015 15:29, Andreas Lochbihler wrote:
Hi Tobias,

On 08/05/15 13:41, Tobias Nipkow wrote:
I like the elimination of atomic let bindings (and the elimination if there
are <= 1
occurrences of the bound variable), but not the rest of the current let_simp.
If possible,
I would relegate that to a special simproc that can be activated on demand.
These cases I like, too, but they are not part of Norbert's special case.

That is my point, I would like to separate out the rest of his code.


A mechanism to make let-bindings in a goal available as assumptions (as in
HOL4) would be
nice, but that only seems to sense in combination with a structured proof that
can access
these assumption by some name.
I would already be very happy to float lets consistently outwards - if the
classical reasoner also knows what to do with them. At least, they would no
longer intervene with other rewrite rules as in "map f (let g = h a in map g
ys)", where the let prevents the simp rule "map f (map g xs) = map (f o g) xs"
from triggering.

I find these intervening control operators (let, if, case, ...) pretty annoying
- especially if the occur under lambdas where the splitter cannot extract them
automatically. But that's a different story.


On 08/05/2015 09:46, Andreas Lochbihler wrote:
Dear Tobias,

An informal explanation of the code is in the NEWS file (for Isabelle2005). It
explains pretty well what is going on.

   Simplifier: new simproc for "let x = a in f x".  If a is a free or
   bound variable or a constant then the let is unfolded.  Otherwise
   first a is simplified to b, and then f b is simplified to g. If
   possible we abstract b from g arriving at "let x = b in h x",
   otherwise we unfold the let and arrive at g.

Unfortunately, this does not help much in understanding the motivation and
indented use cases for the simproc. From a proving perspective, Norbert's case
looks quite pragmatic to me: let's inline and see what happens - maybe one can
regain the abstraction afterwards. Thus, the simproc breaks the abstraction of
the binding - if more can be done, then it will be done.

This is in line with my experience. Let bindings help to make definitions more
readable, but for proving, I usually just get rid of them by unfolding Let_def,
because the classical reasoner does not deal with them at all and the simplifier
does these funny transformations.

I am not really happy with this behaviour. I'd prefer something (maybe a
different let) that respects the abstraction. What are your and others'
experience with this?

Below are my thoughts on respecting the abstraction:

 From a conceptual point of view, the let binding should respect the
abstraction. That is, the new variable should be treated like a fresh constant -
this is presently the case without the simproc. Unfortunately, proving then
becomes a nightmare because no properties of the variable are known to the
provers. It would be good to have some mechanism that automatically transfers
the required properties from the bound term to the variable, but it is not clear
what these properties should be. In fact, being equal to the bound term is also
a property. So the simproc let_simp just goes all the way of transferring the
properties by inlining.

Still, I wonder whether let_simp is doing to much. Essentially, it tries to
guess when the binding should be unfolded (by trying out all possibilities). The
other abstraction facilities in Isabelle such as definition and function have
well-defined rules for when to break the abstraction automatically: definition
only explicitly when the user unfolds the defining equation, and function when
the argument matches the pattern. This seems to work rather well in practice.
With let_simp, it does not work for bindings.

Unfortunately, I do not a good understanding of how such on-the-fly abstractions
(let bindings) should be handled in general. I just have a few data points.
Norrish and Slind (TPHOLs 2005 proof pearl) argue that it is important in some
cases to keep the abstraction of let bindings (and the names of the bound
variables). Their approach extracts let bindings from proof goals and makes them
available as assumptions. Thus, the user can manually derive the required
properties for the bound variables and---equally importantly---the let bindings
are out of the way in the proof term.

Urban mentioned a similar problem in

What I like about let_simp is that it eliminates duplicate let bindings, i.e.,
the term

   let x = f a b in let y = f a b in P x x y y


   let x = f a b in P x x x x

It also folds the abstraction if the bound term occurs in the body:

   let x = f a b in P x x (f a b)


   let x = f a b in P x x x

Unfortunately, the current simproc does not get the let out of the way. For
example, to prove the following, I have to unfold the binding.

   1 + (let x = f a in x + x) = (let x = f a in 1 + (x + x))


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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