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. Tobias
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. AndreasOn 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 https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00277.html. 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 becomes 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) becomes 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)) Best, Andreas
Description: S/MIME Cryptographic Signature