Email Gateway (Aug 19 2022 at 17:12): Email Gateway (Aug 19 2022 at 17:12):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I have large subgoals with operators that bind variables like let, bind and integrals.
These operators are just higher-order functions which use the standard function
abstraction to implement the binding. Unfortunately, lemmas about these operators no
longer apply when the bound variable is a tuple which is split up into its components
using patterns (internally implemented via case_prod), because the case_prod destroys the
pattern. Here is an example to illustrate the problem (also attached as a theory file).
The bind operation on option commutes.
notation Option.bind (infixr "»=" 54)
lemma bind_commute: "x »= (λx. y »= (λy. f x y)) = y »= (λy. x »= (λx. f x y))"
by(cases "x = None ∨ y = None") auto
Now, I would like to apply this lemma in a situation where the "x" is a tupled option and
the "λx" splits the tuple into its components say "λ((b, c), d)". For example,
have "f x »= (λ((b, c), d). g x »= h b d) = foo"
apply(subst bind_commute)
Of course, the subst method fails here, because between the two binds there are the
case_prod functions, i.e., the pattern does not match. I have not been able to find a
satisfactory solution for this problem. I expect that others have the same problem and
hope that they share their solutions with me.
Here are my attempts so far:
apply(unfold split_def)
This works but the resulting subgoal is
"g x »= (λy. f x »= (λx. h (fst (fst x)) (snd x) y)) = foo
which is much harder to read than the desired
"g x »= (λy. f x »= (λ((b, c), d). h b d y)) = foo"
(Think of f, g, and h being huge terms with many occurrences of b and d.) Moreover, the
variable names b and d get lost,
lemma bind_commute_ss:
"x »= (λ((a, b), c). y »= h a b c) = y »= (λy. x »= (λ((a, b), c). h a b c y))"
unfolding split_def by(rule bind_commute)
Now, I can use apply(subst bind_commute_ss), but the variable names are still lost. The
new subgoal is
"g x »= (λy. f x »= (λ((a, b), c). h a c y)) = foo"
instead of
"g x »= (λy. f x »= (λ((b, c), d). h b d y)) = foo"
Moreover, I have to derive a new rule for each way in which the tuples are split up.
State the desired result as an intermediate step:
have "f x »= (λ((b, c), d). g x »= h b d) = g x »= (λy. f x »= (λ((b, c), d). h b d y))"
by(unfold split_def)(rule bind_commute)
also have "... = foo"
When f, g, and h are huge terms, this is very inconvenient, especially when I am in the
middle of an apply script.
Thanks in advance for any pointers and ideas,
Andreas
Split.thy
Email Gateway (Aug 19 2022 at 17:12):From: Michael Norrish <michael.norrish@nicta.com.au>
My experience with this sort of situation is that sometimes you are just doomed.
However, Konrad Slind and I did have a proof pearl in TPHOLs 2005
http://nicta.com.au/people/norrishm/attachments/bibliographies_and_papers/2005/tphols2005-pearl.pdf
where we presented a solution to a pretty similar problem.
I don't know if the Isabelle simplifier will preserve variable names when it
applies the relevant rules, but at least the approach doesn't require anything
more than standard h.o pattern rewriting.
Michael
signature.asc
Email Gateway (Aug 19 2022 at 17:12):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Michael,
I am aware of your approach with combinators and have been using it in Isabelle for a
while. Unfortunately, the simplifier does not preserve variable names as required, but I
was able to solve that by writing a simproc that takes care of that. Unfortunately, the
reasoning infrastructure sometimes spontaneously eta-expands (e.g., due to congruence
rules) or eta-contracts (in particular method subst) terms. Then, new variable names are
introduced or some of the combinators remain in the goal. So this does not work as
smoothly as in HOL.
Maybe I could make your system work to preserve the variable names in my approach no. 2,
but I don't see how I could avoid devising combinator rules for all combinations of splitting.
Cheers,
Andreas
Email Gateway (Aug 19 2022 at 17:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I have never tried to tackle that issue, but a rough idea comes to my
mind: an optional simproc which collapses (%x. … fst x … snd x) to (%(a,
b). … a … b …). No idea how this would work in practice.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 17:14):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Florian,
I am not sure that this would work in general, because "fst x" and "snd x" need not both
be in the remaining term. In my example, we would get "λ(a, d). h (fst a) d y" in the
first step. For a, there is only "fst a", but no "snd a", so should the simproc trigger
once more?
What is more severe is that I do not see how one can possibly get back the original
variable names. Once split_def has been unfolded, they seem to be gone forever.
Andreas
Last updated: Apr 25 2024 at 20:15 UTC