✔ CPDT stackmachine example proof · Coq users

(** * 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

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

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.

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)

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):

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.

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

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)

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

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.

Stream: Coq users

Topic: ✔ CPDT stackmachine example proof

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