## Stream: Coq users

### Topic: ✔ CPDT stackmachine example proof

#### Julin S (Dec 29 2021 at 07:22):

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?

#### Paolo Giarrusso (Dec 29 2021 at 08:16):

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.

#### Paolo Giarrusso (Dec 29 2021 at 08:21):

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`.

#### Julin S (Dec 29 2021 at 09:03):

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.

#### Julin S (Dec 29 2021 at 09:43):

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?

#### Guillaume Melquiond (Dec 29 2021 at 09:54):

Same thing. By evaluation of the definitions of `++`, `progDenote`, and `instrDenote`.

#### Julin S (Dec 29 2021 at 10:22):

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.

#### Paolo Giarrusso (Dec 29 2021 at 10:28):

"evaluate partially" is not wrong; `simpl` has pretty complex heuristic to choose what term to produce.

#### Guillaume Melquiond (Dec 29 2021 at 10:29):

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.

#### Guillaume Melquiond (Dec 29 2021 at 10:30):

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

#### Julin S (Dec 29 2021 at 14:04):

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

#### Notification Bot (Dec 29 2021 at 14:04):

Ju-sh has marked this topic as resolved.

Last updated: Feb 06 2023 at 12:04 UTC