coqのいい感じの情報少ないし、頑張って書いたけどしばらく放置すると忘れてしまうので、詳しめにコメント書いて残しておきます。改善点は多分に残されているので注意しつつ読むこと。

解説

Require Import Arith.
Require Import NArith.
Require Import Vector.
Require Import List.
Require Import Ascii.
Require Import String.
  • Arith
    • OSからなる自然数
  • NArith
    • binaryで保持される自然数
  • List
    • 単方向連結list
    • lisp, haskellのそれと同じ
  • Vector
    • 固定長
  • Ascii
    • boolの8-tupleで表される文字
    • uint8_tや$\mathbb{Z}/256\mathbb{Z}$を表す型が欲しかったけど見つけられなかった
    • 参考にした: mzp/magpack-ocaml
  • String
    • list asciiと同型な文字列
  • Require Importの順は意味を持つらしい
Inductive Brainfuck : Type :=
  | Incr : Brainfuck
  | Decr : Brainfuck
  | Next : Brainfuck
  | Prev : Brainfuck
  | Read : Brainfuck
  | Write : Brainfuck
  | While : list Brainfuck -> Brainfuck.
  • 素直な定義
Definition byte := ascii.

Function byte_succ (n : byte) := ascii_of_N (N.succ (N_of_ascii n)).
Function byte_pred (n : byte) := ascii_of_N (N.add 255 (N_of_ascii n)).
  • ascii ~ (bool, bool, ..., bool)byteとして使う
  • byte_succ (byte_pred n) = nのような定理が証明できない
    • ただし256通りの場合分けを行なえば可能
    • 定義が悪いと思われる
Definition Len : nat := 3000.
Inductive State : Type :=
  | Memory : Vector.t byte Len -> Fin.t Len -> string -> string -> State.
  • 処理系の状態
    • memory, program pointer, input, output
  • Lenは確保する配列の長さ
    • 30000とすると型が巨大すぎて関数の定義が終わらないので少し小さめにしておく
Function state_incr (s : State) : State ...
Function state_decr (s : State) : State ...
Function state_next (s : State) : option State ...
Function state_prev (s : State) : option State ...
Function state_read (s : State) : option State ...
Function state_write (s : State) : State ...
Function state_zerob (s : State) : bool ...
  • 外部でStateの処理を定義しておく
  • optionはhaskellのMaybe
Function state_prev (s : State) : option State :=
  state_update_pointer s (fun mem ptr =>
    match Fin.to_nat ptr with
    | exist i p =>
      match zerop i with
      | left  _ => None
      | right q => Some (Fin.of_nat_lt (lt_trans (Peano.pred i) i Len (lt_pred_n_n i q) p) : Fin.t Len)
      end
    end).
  • 上で挙げたstate_prev
  • state_update_pointerは自明な補助関数
  • Fin.to_nat ptr : {i | i < m}
    • Fin.t n[1,n]の範囲を持つ型
    • 条件を満たす値i : natと条件を満たしていることの証明p : i < Lenから構成されているので分解
  • zerop i : { 0 = i } + { 0 < i }
    • 証明0 = iあるいは証明0 < iのどちらかから構成されているので場合分け
  • Fin.of_nat_lt ...
    • その型に合うように推移律で証明を合成
Inductive EvalResult : Type :=
  | Success
  | Interrupted
  | LeftIndexExceeded
  | RightIndexExceeded
  | EndOfInput.
  • 実行の結果の分類
Fixpoint eval (n : nat) (s : State) (tss : list (list Brainfuck)) : EvalResult * nat * State * list (list Brainfuck) :=
  let failure e := (e, n, s, tss) in
  match n with
  | O => failure Interrupted
  | S n' =>
    match tss with
    | nil => failure Success
    | nil :: tss' => eval n' s tss'
    | (t :: ts) :: tss' =>
      let success s' := eval n' s' (ts :: tss') in
      let try x e :=
        match x with
        | None => failure e
        | Some s' => success s'
        end in
      match t with
      | Incr => success (state_incr s)
      | Decr => success (state_decr s)
      | Next => try (state_next s) RightIndexExceeded
      | Prev => try (state_prev s)  LeftIndexExceeded
      | Read => try (state_read s) EndOfInput
      | Write => success (state_write s)
      | While ts' => eval n' s (if state_zerob s then ts :: tss' else ts' :: tss)
      end
    end
  end.
  • 本体
  • 停止性を保証するために、step数n : natを取りその数だけ実行する
    • coqはturing完全でない
  • step数が0となり中断されても再び再開できるように、次に実行すべき命令をlist (list Brainfuck)として受け渡す
Function execute' (n : nat) (code : list Brainfuck) (input : string)
    : EvalResult * nat * State * list (list Brainfuck) ...
Function execute (n : nat) (code : list Brainfuck) (input : string) : option string ...
  • wrapper
Fixpoint parse' (code : string) (top : list Brainfuck) (stack : list (list Brainfuck)) : option (list Brainfuck) :=
  match code with
  | EmptyString =>
    match stack with
    | nil => Some top
    | _ => None
    end
  | String "+" code' => parse' code' (top ++ Incr  :: nil) stack
  | String "-" code' => parse' code' (top ++ Decr  :: nil) stack
  | String ">" code' => parse' code' (top ++ Next  :: nil) stack
  | String "<" code' => parse' code' (top ++ Prev  :: nil) stack
  | String "," code' => parse' code' (top ++ Read  :: nil) stack
  | String "." code' => parse' code' (top ++ Write :: nil) stack
  | String "[" code' => parse' code' nil (top :: stack)
  | String "]" code' =>
    match stack with
    | nil => None
    | x :: xs => parse' code' (x ++ While top :: nil) xs
    end
  | String _ code' => parse' code' top stack
  end.

Fixpoint parse (code : string) : option (list Brainfuck) := parse' code nil nil.
  • 本体と同じくらい面倒だった
  • coqにとって停止性が明らかであるように、stackに積みながら1度のみ舐める
  • rose tree様の構造であるBrainfuckを停止性を認識させつつ逆にする関数の定義を諦めた
Function execute_string (n : nat) (code : string) (input : string) : option string := option_bind (parse code) (fun code => execute n code input).

Definition A_code := "++++++++[>++++++++<-]>+."%string.
Theorem test_A : execute_string 1000 A_code EmptyString = Some "A"%string.
Proof. compute. trivial. Qed.

Definition helloworld_code := "++++[>++++[>++++>++++++>++<<<-]>++>+<<<-]>>.>+.+++++++..+++.>.<<-<++++[>++++<-]>.>.+++.------.--------.>+."%string.
Theorem test_helloworld : execute_string 10000 helloworld_code EmptyString = Some "Hello World!"%string.
Proof. compute. trivial. Qed.
  • unittest
    • 証明ではない
  • この単純な処理系に関しては、証明の余地はほぼなかったように思う
    • 標準libraryにあるべきだが欠落している汎用関数のそれは別とする
  • helloworldのcodeは短さのためBrainFuck <[+-.,]> »197から拝借

version

$ coqc -v
The Coq Proof Assistant, version 8.4pl5 (January 2015)
compiled on Jan 27 2015 19:49:36 with OCaml 4.02.1