https://coq.discourse.group/t/reasoning-about-higher-order-program-transformation/1240/3

eval_subst.v

Set Implicit Arguments.

(* Source *)
Inductive exp :=
| CONST : nat -> exp
| IFV : exp -> exp -> exp -> exp
| ADD : exp -> exp -> exp.

Definition ifnat {R} (n : nat) (x1 x2 : R) : R :=
  match n with
  | S _ => x1
  | O => x2
  end.

Fixpoint eval (e : exp) : nat :=
  match e with
  | CONST n => n
  | IFV e1 e2 e3 => ifnat (eval e1) (eval e2) (eval e3)
  | ADD e1 e2 => eval e1 + eval e2
  end.

(* Target *)
Inductive aexp : Type :=
| AAdd : aexp -> aexp -> aexp
| AConst : nat -> aexp
.

Inductive bexp (A : Type) : Type :=
| If : aexp -> bexp A -> bexp A -> bexp A
| Const : A -> bexp A
.

(* [bind] of the monad [bexp] *)
Fixpoint subst {A B} (e : bexp A) (k : A -> bexp B) : bexp B :=
  match e with
  | If e1 e2 e3 => If e1 (subst e2 k) (subst e3 k)
  | Const a => k a
  end.

Fixpoint fold {A R} (f : aexp -> R -> R -> R) (g : A -> R) (e : bexp A) : R :=
  match e with
  | If e1 e2 e3 => f e1 (fold f g e2) (fold f g e3)
  | Const a => g a
  end.

Fixpoint eval_aexp (e : aexp) : nat :=
  match e with
  | AConst n => n
  | AAdd e1 e2 => eval_aexp e1 + eval_aexp e2
  end.

Definition evalb : bexp aexp -> nat :=
  fold (fun a => ifnat (eval_aexp a)) eval_aexp.

Lemma fold_mor {A R R'} (f : aexp -> R -> R -> R) (f' : aexp -> R' -> R' -> R') (g : A -> R) (g' : A -> R') (h : R -> R') (e : bexp A)
  : (forall a x1 x2, f' a (h x1) (h x2) = h (f a x1 x2)) ->
    (forall x, g' x = h (g x)) ->
    fold f' g' e = h (fold f g e).
Proof.
  intros H1 H2; induction e; cbn; congruence.
Qed.

(* If you defined [subst] using [fold] this would be a corollary of [fold_mor]. *)
Lemma fold_subst {A B R} (f : aexp -> R -> R -> R) (g : B -> R) (k : A -> bexp B) (e : bexp A)
  : fold f g (subst e k) = fold f (fun x => fold f g (k x)) e.
Proof.
  induction e; cbn; congruence.
Qed.

(* Source-to-target *)
Fixpoint phik (e : exp) : bexp aexp :=
  match e with
  | CONST n => Const (AConst n)
  | IFV e1 e2 e3 => subst (phik e1) (fun e1 => If e1 (phik e2) (phik e3))
  | ADD e1 e2 =>
    subst (phik e1) (fun e1 =>
    subst (phik e2) (fun e2 =>
    Const (AAdd e1 e2)))
  end.

Lemma eval_phik : forall e, evalb (phik e) = eval e.
Proof.
  induction e; cbn.
  - auto. 
  - unfold evalb; rewrite fold_subst; cbn.
    rewrite <- IHe1, <- IHe2, <- IHe3.
    apply fold_mor with (h := fun x => ifnat x _ _) (e := (phik e1)).
    + clear; intros; destruct (eval_aexp a); cbn; auto.
    + intros; reflexivity.
  - unfold evalb; rewrite fold_subst.
    rewrite <- IHe1, <- IHe2.
    apply fold_mor with (h := fun x => x + _) (e := phik e1).
    + intros a; destruct (eval_aexp a); auto.
    + intros x. rewrite fold_subst.
      apply fold_mor.
      * intros a; destruct (eval_aexp a); auto.
      * cbn. auto.
Qed.