I was trying out the first example (untyped) from chapter 2 of the CPDT book under the section Arithmetic Expressions Over Natural Numbers and did

```
(** * Source language **)
Inductive binop : Set := Plus | Mult.
Inductive exp : Set :=
| Const : nat -> exp
| Binop : binop -> exp -> exp -> exp.
Definition binopDenote (op : binop) : nat -> nat -> nat :=
match op with
| Plus => plus (* Same as Nat.add *)
| Mult => mult (* Same as Nat.mul *)
end.
Fixpoint expDenote (e : exp) : nat :=
match e with
| Const n => n
| Binop op e1 e2 => (binopDenote op) (expDenote e1) (expDenote e2)
end.
(** * Target language **)
Inductive instr : Set :=
| iConst : nat -> instr
| iBinop : binop -> instr.
Definition stack : Set := list nat.
Definition instrDenote (i : instr) (s : stack) : option stack :=
match i with
| iConst n => Some (n :: s)
| iBinop b =>
match s with
| (s2 :: s1 :: ss) => (* Was changed from (s1::s2::ss) here *)
let nval := ((binopDenote b) s1 s2) in
Some (nval :: ss)
| _ => None (* Stack prematurely empty! *)
end
end.
Definition prog : Set := list instr.
Fixpoint progDenote (p : prog) (s : stack) : option stack :=
match p with
| (px::pxs) =>
match (instrDenote px s) with
| Some s' => progDenote pxs s'
| None => None
end
| _ => Some s
end.
(** * Translation *)
Fixpoint compile (e : exp) : list instr :=
match e with
| Const n => [iConst n]%list
| Binop op e1 e2 => (compile e2) ++ (compile e1) ++ [iBinop op]%list
end.
```

I had made a change in the definition of `instrDenote`

in the match case of `iBinop`

from something like

```
| iBinop b =>
match s with
| (s1 :: s2 :: ss) =>
let nval := ((binopDenote b) s1 s2) in
Some (nval :: ss)
| _ => None
end
```

to

```
| iBinop b =>
match s with
| (s2 :: s1 :: ss) =>
let nval := ((binopDenote b) s1 s2) in
Some (nval :: ss)
| _ => None
end
```

ie, the order in which elements are taken from the stack was reversed.

But with this change, I couldn't prove the 'translation correctness' proof:

```
Theorem foobar : forall (e : exp) (p : prog) (s : stack),
progDenote ((compile e) ++ p) s = progDenote p ((expDenote e)::s).
Proof.
induction e.
- intros.
unfold compile.
reflexivity.
- intros.
unfold compile.
fold compile.
unfold expDenote.
fold expDenote.
rewrite app_assoc_reverse.
rewrite IHe2.
rewrite app_assoc_reverse.
rewrite IHe1.
unfold progDenote at 1.
simpl.
fold progDenote.
```

the goal at this point would be

```
1 subgoal
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
p : prog
s : stack
========================= (1 / 1)
progDenote p (binopDenote b (expDenote e2) (expDenote e1) :: s) =
progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)
```

and the error was

```
In environment
b : binop
e1, e2 : exp
IHe1 : forall (p : prog) (s : stack),
progDenote (compile e1 ++ p) s = progDenote p (expDenote e1 :: s)
IHe2 : forall (p : prog) (s : stack),
progDenote (compile e2 ++ p) s = progDenote p (expDenote e2 :: s)
p : prog
s : stack
Unable to unify
"progDenote p (binopDenote b (expDenote e1) (expDenote e2) :: s)"
with "progDenote p (binopDenote b (expDenote e2) (expDenote e1) :: s)".
```

But if the change was not made and the order of elements taken from the stack wasn't changed in `instrDenote`

, the proof would end all right.

Was the change that I made erroneous? Or is all I need some change in the proof steps?

I’d say the change is erroneous. In your snippet, the proof can be completed despite your change by proving that `binopDenote b`

is commutative. However, that seems an accident: once you extend the language with subtraction, that will stop being the case. At that point, `instrDenote`

will have to fetch the elements in the correct order.

The reason is that the output of `compile (Binop op e1 e2)`

evaluates and pushes `e2`

to `s2`

, then it evaluates `e1`

to `s1`

and pushes that on top, so the produced stack will have `s1`

on top, then `s2`

.

Okay. So changing the order of 'compilation' of expressions to make it

```
Fixpoint compile (e : exp) : list instr :=
match e with
| Const n => [iConst n]%list
| Binop op e1 e2 => (compile e1) ++ (compile e2) ++ [iBinop op]%list
(* changed from
| Binop op e1 e2 => (compile e2) ++ (compile e1) ++ [iBinop op]%list
*)
end.
```

would set it right? The proof was able to finish after that second change.

I had another small doubt related to this. Could help me with this as well?

Right after the `unfold compile.`

in the first subgoal of the induction, when the goal was

```
1 Subgoal
(1 unfocused at this level)
n : nat
p : prog
s : stack
========================= (1 / 1)
progDenote ([iConst n] ++ p) s = progDenote p (expDenote (Const n) :: s)
```

I did `simpl.`

after which the goal became

```
1 subgoal
(1 unfocused at this level)
n : nat
p : prog
s : stack
========================= (1 / 1)
progDenote p (n :: s) = progDenote p (n :: s)
```

Both `progDenote ([iConst n] ++ p) s`

and `progDenote p (expDenote (Const n) :: s)`

became `progDenote p (n :: s)`

.

`simpl.`

does some evaluations, right?

I understand `progDenote p (expDenote (Const n) :: s)`

becoming `progDenote p (n :: s)`

as `expDenote (Const n)`

gives `n`

.

But how did `progDenote ([iConst n] ++ p) s`

become `progDenote p (n :: s)`

as well?

Same thing. By evaluation of the definitions of `++`

, `progDenote`

, and `instrDenote`

.

Is it that `simpl.`

evaluates `progDenote`

partially or something? I mean, `progDenote`

is still there whereas in the other case with `expDenote`

, `expDenote`

disappeared once its definition was used.

"evaluate partially" is not wrong; `simpl`

has pretty complex heuristic to choose what term to produce.

Yes, it is partial evaluation. But in fact, it is more like weak normalization. Coq's evaluation rules only unfold a fixpoint function if the argument has a constructor in head position. Since `p`

does not, `progDenote`

stays around.

(The so-called "iota-reduction" rule.)

Had heard of iota rule. But had never really looked it up. Thanks guys!

Ju-sh has marked this topic as resolved.

Last updated: Jun 17 2024 at 22:01 UTC