Email Gateway (Aug 22 2022 at 09:42): Email Gateway (Aug 22 2022 at 09:42):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Andreas,
I am certainly open to changes. Here are two that I would welcome: simplifying
the code or adding informal explanations. In the case of your proposed change I
did notice that it would increase the running time and was also a bit concerned
about that.
I am afraid I cannot remember what situations prompted Norbert to write the more
elaborate simproc.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 09:42):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 09:43):From: Tobias Nipkow <nipkow@in.tum.de>
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.
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.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 09:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.
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.
Andreas
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
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 termlet 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
Email Gateway (Aug 22 2022 at 09:44):From: Tobias Nipkow <nipkow@in.tum.de>
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.Andreas
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
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 termlet 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
Email Gateway (Aug 22 2022 at 09:45):From: Thomas Sewell <thomas.sewell@nicta.com.au>
While the let-simp simproc is being discussed, I might mention the
problem I ran into with it.
Note that the body of the let is simplified twice, once by the normal
bottom-up algorithm of the simplifier, and again with the let-expression
unfolded as part of let-simp.
Now suppose that you start with a largish program which uses the let
construct for structuring:
"let a = 1;
(b, s) = f a s;
(c, s) = g b s;
d = a + b;
... etc"
Running the regular simplifier on this is exponential in the nesting
level of the lets. The innermost expression will be simplified with each
possible combination of folding and unfolding of all the let expressions
it is in.
There's also a secondary problem in my case, which is that the let
expression was folded in the first place to avoid an exponential blowup.
I tried working around this, but the long story is that I gave up on
using Isabelle for handling this problem.
Nonetheless, you might want to think about avoiding the exponential issue.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:46):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks for the data point, it looks like we should really separate out that
exponential blowup because it happens in practice.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 09:48):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I like the elimination of atomic let bindings (and the elimination if
^^^^^^^^^^^^^^^^^^^^^^
there are <= 1 occurrences of the bound variable)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
This in fact has been introduced by me.
(Just a remark. I have little ideas what proof support we actually
would need for let-bindings).
Florian
signature.asc
Email Gateway (Aug 22 2022 at 10:05):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts on rewriting,
I have a problem with let bindings and commutative rewrite rules. Here is an example and
my understanding of what is happening.
lemma "(let pb = foobar b in f pb (λpad. g (pb * pad :: int))) = bar"
apply(simp add: mult.commute)
mult.commute rewrites pb * pad into pad * pb, because pad seems to be smaller than pb
in the term order that the simplifier uses.
The let simproc determines that pb occurs more than once in the body, so it does not
inline the let binding. Instead, it simplifies the body with knowledge pb = foobar b.
Thus, the simplifier now sees pad * foobar b. Since "foobar b" is smaller than pad in the
term order, commutativity kicks in again and we get foobar b * pad. Now, the simproc
abstracts the simplified body over foobar b again and replaces it with pb. So we are back
to pb * pad. Thus, the simplifier goes over the whole term again and we are back at step 1.
In my understanding so far, commutative rewrite rules are safe (in the sense of
termination) to add to the simplifier, but the let simproc interferes with this. Is this a
known problem? Can the let simproc be somehow changed to avoid this?
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:05):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Andreas,
I was not aware of this interaction but it does not surprise me - the let
simproc is magic - but you can switch it off. I have no idea if it can be
modified to avoid this interaction in the first place. That sounds like a time sink.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 10:05):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Tobias,
I had another look at the implementation of let_simp. I guess that one might be able to
change the let simproc fairly easily. The idea is as follows. For non-trivial lets (at
least two occurrences of the bound variable and the bound term is not atomic), the let
simproc inlines the bound term in the body, normalises the result with the simplifier and
the current simpset, and then replaces all the remaining occurrences of the bound term in
the normalised term with the bound variable.
There is already a check whether the new body is alpha-beta-eta-equivalent to the old
body. In that case, the simproc aborts with NONE. Now, the interaction can occur only if
the abstracted body is no longer in normal form (although it is with the bound term
inlined)*. Thus, it would make sense to normalise the abstracted body again and check for
equivalence with the original body.
When I add this additional check, the looping in my example disappears. What do you think?
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:07):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Andreas,
Thank you for your thoughts, but I would rather not change the current setup. I
don't really understand Norbert's code and I don't want to add further bits to
it. Moreover, the problem seems to crop up very rarely. If we were to modify the
code, I would expect one of two results: it hardly has any effect or it breaks a
lot of proofs. In both cases I would want to leave well alone.
Tobias
PS I have recently made some similar change also in HOL and am thinking about
undoing it for some of the reasons above.
smime.p7s
Email Gateway (Aug 22 2022 at 10:08):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Tobias,
I do not like the situation "We do not fully understand what is going on, so better not
change anything", because this effectively freezes the code as it currently is with no way
to ever improve it. I am pretty sure that my change would have hardly any effect on the
existing proofs (although I would have to test this hypothesis). Still, I agree with your
decision for another reason. The let_simp simproc is already fairly inefficient when there
are nested let expressions such as
let x = foo a b c in
let y = bar a b c in
let z = fbr a b c in
f x x y y z z
because when the simproc triggers on the let for x (i.e., it has already looked at the
lets for y and z), it inlines the x in the body and invokes the simplifier on the body
let y = bar a b c in
let z = fbr a b c in
f (foo a b c) (foo a b c) y y z z
Thus, the simplifier goes over the whole body again, which triggers the let_simp for the y
once more (it has already triggered for this let binding before it triggered for the outer
let). In summary, let_simp's runtime is exponential in the depth of let nestings.
Now, if we were to add another normalisation check for the abstracted body, this would
increase the base of the exponential by one. The non-termination problem occurs rarely
(the main reason is probably that commutativity rules are not in the simpset by default),
so it probably does not justify slowing the simplifier down (although it took me a while
to understand where the non-termination came from).
I consider the exponential running time more of a problem. (Note that this term remains
linear in size if everything is inlined, so there is no exponential blow-up in term size
due to the inlining.) I digged a bit through the history of the simproc, but I was not
able to find any more information on what Norbert's case really is. Is there anyone who
remembers?
Andreas
PS: For completeness, here's the changed simproc with the additional normalisation test
for Isabelle2015-RC3.
lemma Let_folded2: "⟦ f x ≡ g x; g ≡ g' ⟧ ⟹ Let x f ≡ Let x g'"
by (simp add: Let_def)
simproc_setup let_simp ("Let x f") = {*
let
val (f_Let_unfold, x_Let_unfold) =
let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
in apply2 (Thm.cterm_of @{context}) (f, x) end
val (f_Let_folded2, x_Let_folded2) =
let val [(_ $ (f $ x) $ _), _] = Thm.prems_of @{thm Let_folded2}
in apply2 (Thm.cterm_of @{context}) (f, x) end;
val (g_Let_folded2, g'_Let_folded2) =
let val [_, (_ $ g $ g')] = Thm.prems_of @{thm Let_folded2}
in apply2 (Thm.cterm_of @{context}) (g, g') end;
fun count_loose (Bound i) k = if i >= k then 1 else 0
| count_loose (s $ t) k = count_loose s k + count_loose t k
| count_loose (Abs (_, _, t)) k = count_loose t (k + 1)
| count_loose _ _ = 0;
fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
(case t of
Abs (_, _, t') => count_loose t' 0 <= 1
| _ => true);
in
fn _ => fn ctxt => fn ct =>
if is_trivial_let (Thm.term_of ct)
then SOME @{thm Let_def} (no or one ocurrence of bound variable)
else
let (Norbert Schirmer's case)
val t = Thm.term_of ct;
val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
in
Option.map (hd o Variable.export ctxt' ctxt o single)
(case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in
normal form *)
if is_Free x orelse is_Bound x orelse is_Const x
then SOME @{thm Let_def}
else
let
val n = case f of (Abs (x, _, _)) => x | _ => "x";
val cx = Thm.cterm_of ctxt x;
val xT = Thm.typ_of_cterm cx;
val cf = Thm.cterm_of ctxt f;
val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
val (_ $ _ $ g) = Thm.prop_of fx_g;
val g' = abstract_over (x, g);
val abs_g'= Abs (n, xT, g');
in
if g aconv g' then
let
val rl =
cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm
Let_unfold};
in SOME (rl OF [fx_g]) end
else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract
abs_g') then
NONE (avoid identity conversion)
else
(* normalise the abstracted body, as the abstraction might have
un-normalised the body, e.g., ordered rewriting,
simprocs with syntactic checks, ... *)
let
val g'_normal = Simplifier.rewrite ctxt (Thm.cterm_of ctxt abs_g');
val (_ $ _ $ g'_normalised) = Thm.prop_of g'_normal;
in
if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract
g'_normalised) then
NONE
else
let
val g'x = abs_g' $ x;
val g_g'x = Thm.symmetric (Thm.beta_conversion false
(Thm.cterm_of ctxt g'x));
val rl =
@{thm Let_folded2} |> cterm_instantiate
[(f_Let_folded2, Thm.cterm_of ctxt f),
(x_Let_folded2, cx),
(g_Let_folded2, Thm.cterm_of ctxt abs_g'),
(g'_Let_folded2, Thm.cterm_of ctxt g'_normalised)];
in SOME (rl OF [Thm.transitive fx_g g_g'x, g'_normal])
end
end
end
| _ => NONE)
end
end
*}
Last updated: Nov 21 2024 at 12:39 UTC