ソフトウェアの基礎，Imp_J.vの練習問題stack_compilerを解いた

stack_machine.v

(* ソフトウェアの基礎より *)
Require Import List Arith.

Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y) 
                     (at level 60, right associativity).

(* 変数の識別子 *)
Inductive id : Type :=
  Id : nat -> id.
Definition beq_id X1 X2 :=
  match (X1, X2) with
    (Id n1, Id n2) => beq_nat n1 n2
  end.
Definition X : id := Id 0.
Definition Y : id := Id 1.
Definition Z : id := Id 2.

(* 環境（？） *)
Definition state := id -> nat.
Definition empty_state : state :=
  fun _ => 0.

Definition update (st : state) (X:id) (n : nat) : state :=
  fun X' => if beq_id X X' then n else st X'.

(* 算術式 *)
Inductive aexp : Type :=
  | ANum : nat -> aexp
  | AId : id -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

(* 算術式の評価 *)
Fixpoint aeval (st : state) (e : aexp) : nat :=
  match e with
  | ANum n => n
  | AId X => st X
  | APlus a1 a2 => (aeval st a1) + (aeval st a2)
  | AMinus a1 a2  => (aeval st a1) - (aeval st a2)
  | AMult a1 a2 => (aeval st a1) * (aeval st a2)
  end.

(* スタック指向言語の命令 *)
Inductive sinstr : Type :=
| SPush : nat -> sinstr
| SLoad : id -> sinstr
| SPlus : sinstr
| SMinus : sinstr
| SMult : sinstr.

(* スタック指向言語で書かれたプログラムの評価 *)
Fixpoint s_execute (st : state) (stack : list nat)
                   (prog : list sinstr)
                 : list nat :=
  match prog with
  | [] => stack
  | SPush n :: prog' => s_execute st (n :: stack) prog'
  | SLoad x :: prog' => s_execute st (st x :: stack) prog'
  | SPlus :: prog' =>
      match stack with
      | y :: x :: stack' => s_execute st (x + y :: stack') prog'
      | _ => s_execute st stack prog'
      end
  | SMinus :: prog' =>
      match stack with
      | y :: x :: stack' => s_execute st (x - y :: stack') prog'
      | _ => s_execute st stack prog'
      end
  | SMult :: prog' =>
      match stack with
      | y :: x :: stack' => s_execute st (x * y :: stack') prog'
      | _ => s_execute st stack prog'
      end
  end.

Example s_execute1 :
     s_execute empty_state []
       [SPush 5, SPush 3, SPush 1, SMinus]
   = [2, 5].
Proof. reflexivity. Qed.

Example s_execute2 :
     s_execute (update empty_state X 3) [3,4]
       [SPush 4, SLoad X, SMult, SPlus]
   = [15, 4].
Proof. reflexivity. Qed.

(* 算術式をスタック指向言語にコンパイル *)
Fixpoint s_compile (e : aexp) : list sinstr :=
  match e with
  | ANum n => [SPush n]
  | AId x => [SLoad x]
  | APlus e1 e2 => s_compile e1 ++ s_compile e2 ++ [SPlus]
  | AMinus e1 e2 => s_compile e1 ++ s_compile e2 ++ [SMinus]
  | AMult e1 e2 => s_compile e1 ++ s_compile e2 ++ [SMult]
  end.

Example s_compile1 :
    s_compile (AMinus (AId X) (AMult (ANum 2) (AId Y)))
  = [SLoad X, SPush 2, SLoad Y, SMult, SMinus].
Proof. reflexivity. Qed.

Theorem s_execute_app : forall st prog1 prog2 stack,
  s_execute st stack (prog1 ++ prog2) = s_execute st (s_execute st stack prog1) prog2.
Proof.
  (* 逆ポーランド電卓がfoldで書けるんだから当たり前だよなぁ？ *)
  intros st prog1 prog2.
  induction prog1 as [| inst prog1']; intros stack.
    reflexivity.

    destruct inst; 
    destruct stack; 
    try destruct stack;
    apply IHprog1'.
Qed.

Theorem s_compile_correct_aux : forall st stack e,
  s_execute st stack (s_compile e) = aeval st e :: stack.
Proof.
  intros st stack e.
  generalize dependent stack.
  induction e; intros stack;
    try reflexivity;
    simpl;
    repeat rewrite -> s_execute_app;
    rewrite -> IHe1;
    rewrite -> IHe2;
    reflexivity.
Qed.  

(* コンパイルが正しく行われている *)
Theorem s_compile_correct : forall (st : state) (e : aexp),
  s_execute st [] (s_compile e) = [ aeval st e ].
Proof.
  intros st e.
  apply s_compile_correct_aux.
Qed.