Hello !

I am trying to formalize a program transformation which consists of lifting

“ifs” to the top-level of the term. The natural way to express this

transformation is to use a higher-order function taking a continuation as a

second argument (see function `phi`

below).

However, this definition is hard to reason about due to the higher-order argument.

For example, I would like to prove Lemma A and Lemma B below.

I tried “defunctionalizing” the transformation, defining an inductive type for the different

continuations. However, I cannot get around the structural recursion check in Coq.

I feel this kind of problem must have a standard solution, but I’m stuck so far.

Any help or pointers to possible approaches would be appreciated!

Thanks!

Nicolas

```
Inductive exp :=
| CONST : nat -> exp
| IFV : exp -> exp -> exp -> exp
| ADD : exp -> exp -> exp.
(* Semantics *)
Fixpoint eval (e : exp) : nat :=
match e with
| CONST n => n
| IFV e1 e2 e3 =>
match eval e1 with
| S _ => eval e2
| O => eval e3
end
| ADD e1 e2 =>
eval e1 + eval e2
end.
(* Lift IFV to the top-level, duplicating the continuation *)
Fixpoint phi e k {struct e} :=
match e with
| CONST n => k (CONST n)
| IFV e1 e2 e3 =>
phi e1 (fun e1 => IFV e1 (phi e2 k) (phi e3 k))
| ADD e1 e2 =>
phi e1 (fun e1 => phi e2 (fun e2 => k (ADD e1 e2)))
end.
(* The program transformation [phi] should preserve the semantics. *)
Lemma A: forall e, eval (phi e (fun x => x)) = eval e.
Abort.
(* The above is not general enough for induction on [e], so instead I try to
prove [Lemma B] below. As stated, [B] is false because [k]
can "inspect" its argument and do something different depending on its shape. *)
Lemma B: forall e k, eval (phi e k) = eval (k e).
Abort.
(* "Defunctionalization" : a datatype for the possible continuations *)
Inductive cont :=
| Kid : cont
| Kifv : exp -> exp -> cont
| Kadd1 : exp (* "suspended" e2 *) -> cont -> cont
| Kadd2 : exp (* "lifted" e1 *) -> cont -> cont.
(* The following does not work *)
Fixpoint apply k e :=
match k with
| Kid => e
| Kifv e2 e3 => IFV e e2 e3
| Kadd1 e2 k => phik e2 (Kadd2 e k)
| Kadd2 e1 k => apply k (ADD e1 e)
end
with phik e (k : cont) :=
match e with
| CONST n => apply k (CONST n)
| IFV e1 e2 e3 => phik e1 (Kifv (phik e2 k) (phik e3 k))
| ADD e1 e2 => phik e1 (Kadd1 e2 k)
end.
```