Re: [isabelle] pushing let environments to the top level



On Sat, Apr 25, 2009 at 4:43 PM, Konrad Slind <slind at cs.utah.edu> wrote:

> Michael Norrish and I tackled exactly this sort of thing in
>
>   http://www.cs.utah.edu/~slind/papers/tphols05.pearl.pdf<http://www.cs.utah.edu/%7Eslind/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.
>

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):
 1. let x = part (%y. ord y h) t
    in perm (h # t) ((%(l1, l2). qsort ord l1 @ [h] @ qsort ord l2) x)

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):
 1. let (xa, x) = part (%y. ord y h) t
    in perm (h # t) (qsort ord xa @ [h] @ qsort ord x)

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):
 1. P (%a. f (a, a))

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.

- Brian




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