Stream: Coq users

Topic: ✔ CPDT stackmachine example proof


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Guillaume Melquiond (Dec 29 2021 at 09:54):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 29 2021 at 10:28):

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

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Dec 29 2021 at 10:30):

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

view this post on Zulip Julin S (Dec 29 2021 at 14:04):

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

view this post on Zulip 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