Email Gateway (Aug 18 2022 at 13:27): Email Gateway (Aug 18 2022 at 13:27):From: Ewaryst Schulz <ewaryst.schulz@dfki.de>
Hi,
I have a question regarding let environments in formulas. I'd like to
push them to the top of the formula and ideally declare them by
def-statements in the isar-proof.
Consider e.g. a context with variables x1, ..., xn:
My goal is of the form Psi(s1(X), ... , sm(X)), where X = x1, ..., xn, and
s1(X) of the form
let y1 = t1(X);
y2 = t2(X,y1);
...
yk = tk(X,Y)
in Phi(X,Y,yk)
Now I'd like to move the let-environment to the outside (theoretically
this is possible, if no variable capturing occurs, by some beta/eta
reduction and expansion):
Psi(s1(X), ... , sm(X))
--->
let y1 = t1(X);
y2 = t2(X,y1);
...
yk = tk(X,Y)
in Psi(Phi(X,Y,yk), s2(X), ... , sm(X))
And then put the let-env to the isar context by def:
--->
def y1 == t1(X)
def y2 == t2(X,y1)
...
def yk == tk(X,Y)
goal:
Psi(Phi(X,Y,yk), s2(X), ... , sm(X))
I'm not a really advanced user so I'd prefer to use an existing
procedure to do that automatically. Is there a tactic which does exactly
this job?
Of course then I won't have the defs visible in my isar proof, and I'd
need a labeling convention for this knowledge (to access the equalities
yi == t1(...)).
The method should also fail if the Y,yk and X intersect in the variable
names (variable capturing).
I don't think there is already something which does that exactly, but
perhaps there is a better way to deal with let environments deep inside
formulas
(I don't want to expand/unfold the let environment!) ?
Thanks for your help in advance,
cheers,
Ewaryst
Email Gateway (Aug 18 2022 at 13:27):From: Konrad Slind <slind@cs.utah.edu>
Hi,
Michael Norrish and I tackled exactly this sort of thing in
http://www.cs.utah.edu/~slind/papers/tphols05.pearl.pdf
The ideas in the paper are worked out in HOL4, and may
need to be modified a bit for Isabelle/HOL.
Cheers,
Konrad.
Email Gateway (Aug 18 2022 at 13:27):From: Brian Huffman <brianh@cs.pdx.edu>
I just tried out the rules from the paper in Isabelle/HOL. Indeed, the
unmodified rules don't work quite the same in Isabelle. Here's what I tried:
definition flip_def [simp]: "flip f x y = f y x"
definition compose_def [simp]: "compose f g x = f (g x)"
lemma Let_simps:
"!!f m g. f (Let m g) = Let m (compose f g)"
"!!m f n. (Let m f) n = Let m (flip f n)"
"!!f g. compose f (%x. g x) = (%x. f (g x))"
"!!f y. flip (%x. f x) y = (%x. f x y)"
"!!f g. compose f (split g) = split (compose (compose f) g)"
"!!f x. flip (split f) x = split (flip (compose flip f) x)"
unfolding Let_def expand_fun_eq by simp_all
Next I applied these as rewrites to the example term from the paper:
lemma "perm (h # t)
(let (l1, l2) = part (%y. ord y h) t in qsort ord l1 @ [h] @ qsort ord
l2)"
apply (simp only: Let_simps)
Here's the resulting term I hoped to get:
let (l1, l2) = part (%y. ord y h) t
in perm (h # t) (qsort ord l1 @ [h] @ qsort ord l2)"
But here's what I got:
goal (1 subgoal):
It sort of worked. At least the let binding was lifted to the outside of the
term. But the tuple binding was replaced with a single variable binding.
Also, the simplifier invented a new bound variable name, while the rules in
the paper are specifically designed to preserve bound variable names.
It appears that the Isabelle's simplifier behaves differently than HOL4. In
HOL4, the LHS patterns of the following two rules are non-overlapping:
"compose f (%x. g x) = (%x. f (g x))"
"compose f (split g) = split (compose (compose f) g)"
In Isabelle, I think the simplifier treats the first rule as equivalent to
the eta-contracted form:
"compose f g = (%x. f (g x))"
So it matches more often than the same rule in HOL4.
As a workaround, you could call the simplifier twice, using the
split-specific rules first, and the more general rules afterward:
lemma "perm (h # t)
(let (l1, l2) = part (%y. ord y h) t in qsort ord l1 @ [h] @ qsort ord
l2)"
apply (simp only: Let_simps(1,2,5,6), simp only: Let_simps(3,4))
goal (1 subgoal):
This at least gets the tuple binding in the right place, but the variable
names are still wrong. It just seems that the preservation of bound variable
names is a feature of the HOL4 simplifier that was never implemented in
Isabelle. Instead, Isabelle's simplifier replaces the old bound variable
name for whatever name was used on the RHS of the original rewrite rule. For
example:
lemma foo: "!!f g. compose f (%a. (g a, h a)) = (%a. f (g a, h a))"
unfolding expand_fun_eq by simp
lemma "P (compose f (%y. (y, y)))"
apply (simp only: foo)
goal (1 subgoal):
Anyway, I guess my conclusion is that to lift let-bindings in Isabelle, we
will need more than just a set of rewrite rules. A special proof tactic that
preserves variable names probably wouldn't be too hard to implement though.
Last updated: May 03 2024 at 08:18 UTC