EvalML1Errにおける評価の全域性の証明でML1*1のすべての式に評価される値が存在することが分かったので、式を評価する関数書いてみたいと思います。また、せっかくCoqで書いたので関数が妥当であるかの証明とOCamlソースコードの出力も行おうと思います。
まずは式を評価する関数を書きます。普通に書くとパターンマッチが大量に出てきて煩わしいので、Maybeモナド風に書いてみました。
Notation "'perform' x <-- e1 ;; e2" :=
(match e1 with
| None => None
| Some x => e2
end)
(right associativity, at level 60).
Fixpoint eval_ml1exp (e : exp) : option value :=
match e with
| ExpInt n => Some (VInt n)
| ExpBool b => Some (VBool b)
| ExpPlus e1 e2 =>
perform v1 <-- eval_ml1exp e1;;
perform v2 <-- eval_ml1exp e2;;
match v1, v2 with
| VBool _, _ => None
| _, VBool _ => None
| VInt n1, VInt n2 =>
Some (VInt (n1 + n2))
end
| ExpTimes e1 e2 =>
perform v1 <-- eval_ml1exp e1;;
perform v2 <-- eval_ml1exp e2;;
match v1, v2 with
| VBool _, _ => None
| _, VBool _ => None
| VInt n1, VInt n2 =>
Some (VInt (n1 * n2))
end
| ExpLt e1 e2 =>
perform v1 <-- eval_ml1exp e1;;
perform v2 <-- eval_ml1exp e2;;
match v1, v2 with
| VBool _, _ => None
| _, VBool _ => None
| VInt n1, VInt n2 =>
Some (VBool (blt_nat n1 n2))
end
| ExpIf e1 e2 e3 =>
perform v1 <-- eval_ml1exp e1;;
match v1 with
| VInt _ => None
| VBool true => eval_ml1exp e2
| VBool false => eval_ml1exp e3
end
end.このHaskellにおけるdoの様な構文はソフトウェアの基礎から拝借しています。
Coqにも型クラスはある様なのでMaybeモナドに限定しない汎用的な構文にできそうですが、本題から逸れるので今回は手を付けません。
次に、全ての式がこの関数の戻り値に評価されることを証明します。証明は長いですが適当に場合分けして該当する評価規則に当てはめるだけなので難しくはないです。
Theorem eval_evaled : forall (e : exp), e evalto (eval_ml1exp e).
Proof.
intros e.
induction e.
apply EInt.
apply EBool.
remember (eval_ml1exp e1).
destruct o.
remember (eval_ml1exp e2).
destruct o.
destruct v.
destruct v0.
simpl.
rewrite <- Heqo.
rewrite <- Heqo0.
apply EPlus with (n1 := n) (n2 := n0).
eauto.
eauto.
eauto.
simpl.
rewrite <- Heqo.
rewrite <- Heqo0.
apply EPlusBoolR with (b := b).
auto.
simpl.
rewrite <- Heqo.
destruct (eval_ml1exp e2).
apply EPlusBoolL with (b := b).
auto.
apply EPlusBoolL with (b := b).
auto.
simpl.
rewrite <- Heqo.
rewrite <- Heqo0.
apply EPlusErrorR.
eauto.
simpl.
rewrite <- Heqo.
apply EPlusErrorL.
eauto.
remember (eval_ml1exp e1).
destruct o.
remember (eval_ml1exp e2).
destruct o.
destruct v.
destruct v0.
simpl.
rewrite <- Heqo.
rewrite <- Heqo0.
apply ETimes with (n1 := n) (n2 := n0).
eauto.
eauto.
eauto.
simpl.
rewrite <- Heqo.
rewrite <- Heqo0.
apply ETimesBoolR with (b := b).
auto.
simpl.
rewrite <- Heqo.
destruct (eval_ml1exp e2).
apply ETimesBoolL with (b := b).
auto.
apply ETimesBoolL with (b := b).
auto.
simpl.
rewrite <- Heqo.
rewrite <- Heqo0.
apply ETimesErrorR.
eauto.
simpl.
rewrite <- Heqo.
apply ETimesErrorL.
eauto.
remember (eval_ml1exp e1).
destruct o.
remember (eval_ml1exp e2).
destruct o.
destruct v.
destruct v0.
simpl.
rewrite <- Heqo.
rewrite <- Heqo0.
apply ELt with (n1 := n) (n2 := n0).
eauto.
eauto.
eauto.
simpl.
rewrite <- Heqo.
rewrite <- Heqo0.
apply ELtBoolR with (b := b).
auto.
simpl.
rewrite <- Heqo.
destruct (eval_ml1exp e2).
apply ELtBoolL with (b := b).
auto.
apply ELtBoolL with (b := b).
auto.
simpl.
rewrite <- Heqo.
rewrite <- Heqo0.
apply ELtErrorR.
eauto.
simpl.
rewrite <- Heqo.
apply ELtErrorL.
eauto.
remember (eval_ml1exp e1).
destruct o.
remember v.
destruct v0.
simpl.
rewrite <- Heqo.
apply EIfInt with (n := n).
auto.
remember b.
destruct b0.
simpl.
rewrite <- Heqo.
remember (eval_ml1exp e2).
destruct o.
apply EIfT.
auto.
auto.
apply EIfTError.
auto.
auto.
simpl.
rewrite <- Heqo.
remember (eval_ml1exp e3).
destruct o.
apply EIfF.
auto.
auto.
apply EIfFError.
auto.
auto.
simpl.
rewrite <- Heqo.
apply EIfError.
auto.
Qed.もっと格好良い名前にしたかったのですが、センスが足りませんでした。
この定理を使えば、関数の戻り値がvであることと式がvに評価されることが等価であると簡単に証明できます。
Theorem eval_evalto_equiv : forall (e : exp) (v : option value),
e evalto v <-> eval_ml1exp e = v.
Proof.
intros e v.
split.
intros H.
apply evalto_unique with (e := e).
apply eval_evaled.
apply H.
intros H.
rewrite <- H.
apply eval_evaled.
Qed.最後に、OCamlソースコードの出力を行います。詳しいことは分かりませんがプログラミングCoqの手順に従えば出力できました。
Extract Constant plus => "( + )". Extract Constant mult => "( * )". Extract Constant blt_nat => "( < )". Extract Inductive nat => int ["0" "succ"] "(fun fO fS n -> if n = 0 then fO () else fS (n-1))". Extract Inductive bool => bool ["true" "false"]. Extract Inductive option => option ["Some" "None"]. Extraction "evalML1Err.ml" eval_ml1exp.
これにより、Coqで仕様を満たすことが証明されたOCamlの関数が得られました。
(** val plus : int -> int -> int **) let rec plus = ( + ) (** val mult : int -> int -> int **) let rec mult = ( * ) type exp = | ExpInt of int | ExpBool of bool | ExpPlus of exp * exp | ExpTimes of exp * exp | ExpLt of exp * exp | ExpIf of exp * exp * exp type value = | VInt of int | VBool of bool (** val blt_nat : int -> int -> bool **) let rec blt_nat = ( < ) (** val eval_ml1exp : exp -> value option **) let rec eval_ml1exp = function | ExpInt n -> Some (VInt n) | ExpBool b -> Some (VBool b) | ExpPlus (e1, e2) -> (match eval_ml1exp e1 with | Some v1 -> (match eval_ml1exp e2 with | Some v2 -> (match v1 with | VInt n1 -> (match v2 with | VInt n2 -> Some (VInt (plus n1 n2)) | VBool b -> None) | VBool b -> None) | None -> None) | None -> None) | ExpTimes (e1, e2) -> (match eval_ml1exp e1 with | Some v1 -> (match eval_ml1exp e2 with | Some v2 -> (match v1 with | VInt n1 -> (match v2 with | VInt n2 -> Some (VInt (mult n1 n2)) | VBool b -> None) | VBool b -> None) | None -> None) | None -> None) | ExpLt (e1, e2) -> (match eval_ml1exp e1 with | Some v1 -> (match eval_ml1exp e2 with | Some v2 -> (match v1 with | VInt n1 -> (match v2 with | VInt n2 -> Some (VBool (blt_nat n1 n2)) | VBool b -> None) | VBool b -> None) | None -> None) | None -> None) | ExpIf (e1, e2, e3) -> (match eval_ml1exp e1 with | Some v1 -> (match v1 with | VInt n -> None | VBool b -> if b then eval_ml1exp e2 else eval_ml1exp e3) | None -> None)
