前回はプログラミング言語の基礎概念に出てくるEvalML1についての定理を証明したので、ついでに実行時エラーも扱うEvalML1Errにおける評価の一意性を証明したいと思います。
式や値の定義などは前回と変わりません。
Require Import Arith. (* ML1の式 *) Inductive exp : Type := | ExpInt : nat -> exp | ExpBool : bool -> exp | ExpPlus : exp -> exp -> exp | ExpTimes : exp -> exp -> exp | ExpLt : exp -> exp -> exp | ExpIf : exp -> exp -> exp -> exp. (* ML1の値 *) Inductive value : Type := | VInt : nat -> value | VBool : bool -> value. (* boolを返す比較関数 *) Fixpoint blt_nat (n1 n2 : nat) : bool := match n1, n2 with | _, O => false | O, S _ => true | S n1', S n2' => blt_nat n1' n2' end.
本では実行時エラーをerrorに評価することで表現していますが、いい感じの表現が見つからなかったのでオプション型を使って評価が成功したかどうかを表現しています。少なくともerrorは値ではないとは書いてありました。
Inductive evalto : exp -> option value -> Prop :=
| EInt : forall (n : nat), evalto (ExpInt n) (Some (VInt n))
| EBool : forall (b : bool), evalto (ExpBool b) (Some (VBool b))
| EIfT : forall (e1 e2 e3 : exp) (v : value),
evalto e1 (Some (VBool true)) ->
evalto e2 (Some v) ->
evalto (ExpIf e1 e2 e3) (Some v)
| EIfF : forall (e1 e2 e3 : exp) (v : value),
evalto e1 (Some (VBool false)) ->
evalto e3 (Some v) ->
evalto (ExpIf e1 e2 e3) (Some v)
| EPlus : forall (e1 e2 : exp) (n1 n2 n3 : nat),
evalto e1 (Some (VInt n1)) ->
evalto e2 (Some (VInt n2)) ->
n1 + n2 = n3 ->
evalto (ExpPlus e1 e2) (Some (VInt n3))
| ETimes : forall (e1 e2 : exp) (n1 n2 n3 : nat),
evalto e1 (Some (VInt n1)) ->
evalto e2 (Some (VInt n2)) ->
n1 * n2 = n3 ->
evalto (ExpTimes e1 e2) (Some (VInt n3))
| ELt : forall (e1 e2 : exp) (n1 n2 : nat) (b : bool),
evalto e1 (Some (VInt n1)) ->
evalto e2 (Some (VInt n2)) ->
blt_nat n1 n2 = b ->
evalto (ExpLt e1 e2) (Some (VBool b))
| EIfInt : forall (e1 e2 e3 : exp) (n : nat),
evalto e1 (Some (VInt n)) ->
evalto (ExpIf e1 e2 e3) None
| EPlusBoolL : forall (e1 e2 : exp) (b : bool),
evalto e1 (Some (VBool b)) ->
evalto (ExpPlus e1 e2) None
| EPlusBoolR : forall (e1 e2 : exp) (b : bool),
evalto e2 (Some (VBool b)) ->
evalto (ExpPlus e1 e2) None
| ETimesBoolL : forall (e1 e2 : exp) (b : bool),
evalto e1 (Some (VBool b)) ->
evalto (ExpTimes e1 e2) None
| ETimesBoolR : forall (e1 e2 : exp) (b : bool),
evalto e2 (Some (VBool b)) ->
evalto (ExpTimes e1 e2) None
| ELtBoolL : forall (e1 e2 : exp) (b : bool),
evalto e1 (Some (VBool b)) ->
evalto (ExpLt e1 e2) None
| ELtBoolR : forall (e1 e2 : exp) (b : bool),
evalto e2 (Some (VBool b)) ->
evalto (ExpLt e1 e2) None
| EIfError : forall (e1 e2 e3 : exp),
evalto e1 None ->
evalto (ExpIf e1 e2 e3) None
| EIfTError : forall (e1 e2 e3 : exp),
evalto e1 (Some (VBool true)) ->
evalto e2 None ->
evalto (ExpIf e1 e2 e3) None
| EIfFError : forall (e1 e2 e3 : exp),
evalto e1 (Some (VBool false)) ->
evalto e3 None ->
evalto (ExpIf e1 e2 e3) None
| EPlusErrorL : forall (e1 e2 : exp),
evalto e1 None ->
evalto (ExpPlus e1 e2) None
| EPlusErrorR : forall (e1 e2 : exp),
evalto e2 None ->
evalto (ExpPlus e1 e2) None
| ETimesErrorL : forall (e1 e2 : exp),
evalto e1 None ->
evalto (ExpTimes e1 e2) None
| ETimesErrorR : forall (e1 e2 : exp),
evalto e2 None ->
evalto (ExpTimes e1 e2) None
| ELtErrorL : forall (e1 e2 : exp),
evalto e1 None ->
evalto (ExpLt e1 e2) None
| ELtErrorR : forall (e1 e2 : exp),
evalto e2 None ->
evalto (ExpLt e1 e2) None.
Infix "evalto" := evalto (at level 70, no associativity).まずは評価の一意性について証明しておきます。
推論規則が非常に多くなったことで証明も非常に長くなっていますが、ひたすら場合分けを使って力づくで証明しているだけなのでそれほど難しくはありません。
Theorem evalto_unique : forall (e : exp) (v1 v2 : option value),
e evalto v1 -> e evalto v2 -> v1 = v2.
Proof.
intros e.
induction e.
intros v1 v2 H H0.
inversion H.
inversion H0.
reflexivity.
intros v1 v2 H H0.
inversion H.
inversion H0.
reflexivity.
intros v1 v2 H H0.
inversion H.
inversion H0.
assert (Some (VInt n1) = Some (VInt n0)).
auto.
assert (Some (VInt n2) = Some (VInt n4)).
auto.
congruence.
assert (Some (VInt n1) = Some (VBool b)).
auto.
congruence.
assert (Some (VInt n2) = Some (VBool b)).
auto.
congruence.
assert (Some (VInt n1) = None).
auto.
congruence.
assert (Some (VInt n2) = None).
auto.
congruence.
inversion H0.
assert (Some (VBool b) = Some (VInt n1)).
auto.
inversion H11.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (Some (VBool b) = Some (VInt n2)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (None = Some (VInt n1)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (None = Some (VInt n2)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
intros v1 v2 H H0.
inversion H.
inversion H0.
assert (Some (VInt n1) = Some (VInt n0)).
auto.
assert (Some (VInt n2) = Some (VInt n4)).
auto.
congruence.
assert (Some (VInt n1) = Some (VBool b)).
auto.
congruence.
assert (Some (VInt n2) = Some (VBool b)).
auto.
congruence.
assert (Some (VInt n1) = None).
auto.
congruence.
assert (Some (VInt n2) = None).
auto.
congruence.
inversion H0.
assert (Some (VBool b) = Some (VInt n1)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (Some (VBool b) = Some (VInt n2)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (None = Some (VInt n1)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (None = Some (VInt n2)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
intros v1 v2 H H0.
inversion H.
inversion H0.
assert (Some (VInt n1) = Some (VInt n0)).
auto.
assert (Some (VInt n2) = Some (VInt n3)).
auto.
congruence.
assert (Some (VInt n1) = Some (VBool b0)).
auto.
congruence.
assert (Some (VInt n2) = Some (VBool b0)).
auto.
congruence.
assert (Some (VInt n1) = None).
auto.
congruence.
assert (Some (VInt n2) = None).
auto.
congruence.
inversion H0.
assert (Some (VBool b) = Some (VInt n1)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (Some (VBool b) = Some (VInt n2)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (None = Some (VInt n1)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (None = Some (VInt n2)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
intros v1 v2 H H0.
inversion H.
inversion H0.
auto.
assert (Some (VBool true) = Some (VBool false)).
auto.
congruence.
assert (Some (VBool true) = Some (VInt n)).
auto.
congruence.
assert (Some (VBool true) = None).
auto.
congruence.
assert(Some v = None).
auto.
congruence.
assert(Some (VBool true) = Some (VBool false)).
auto.
congruence.
inversion H0.
assert (Some (VBool false) = Some (VBool true)).
auto.
congruence.
auto.
assert (Some (VBool false) = Some (VInt n)).
auto.
congruence.
assert (Some (VBool false) = None).
auto.
congruence.
assert (Some (VBool false) = Some (VBool true)).
auto.
congruence.
assert (Some v = None).
auto.
congruence.
inversion H0.
assert (Some (VInt n) = Some (VBool true)).
auto.
congruence.
assert (Some (VInt n) = Some (VBool false)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (None = Some (VBool true)).
auto.
congruence.
assert (None = Some (VBool false)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (None = Some v).
auto.
congruence.
assert (Some (VBool true) = Some (VBool false)).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
inversion H0.
assert (Some (VBool false) = Some (VBool true)).
auto.
congruence.
assert (None = Some v).
auto.
congruence.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
Qed.最後に、目的の全域性について証明します。
これもひたすら場合分けをして推論規則を適用していくだけですね。
Theorem evalto_whole : forall (e : exp),
exists (v : option value), e evalto v.
Proof.
intros e.
induction e.
exists (Some (VInt n)).
apply EInt.
exists (Some (VBool b)).
apply EBool.
inversion IHe1.
inversion IHe2.
destruct x.
destruct v.
destruct x0.
destruct v.
exists (Some (VInt (n + n0))).
apply EPlus with (n1 := n) (n2 := n0).
auto.
auto.
auto.
exists None.
apply EPlusBoolR with (b := b).
auto.
exists None.
apply EPlusErrorR.
auto.
exists None.
apply EPlusBoolL with (b := b).
auto.
exists None.
apply EPlusErrorL.
auto.
inversion IHe1.
inversion IHe2.
destruct x.
destruct v.
destruct x0.
destruct v.
exists (Some (VInt (n * n0))).
apply ETimes with (n1 := n) (n2 := n0).
auto.
auto.
auto.
exists None.
apply ETimesBoolR with (b := b).
auto.
exists None.
apply ETimesErrorR.
auto.
exists None.
apply ETimesBoolL with (b := b).
auto.
exists None.
apply ETimesErrorL.
auto.
inversion IHe1.
inversion IHe2.
destruct x.
destruct v.
destruct x0.
destruct v.
exists (Some (VBool (blt_nat n n0))).
apply ELt with (n1 := n) (n2 := n0).
auto.
auto.
auto.
exists None.
apply ELtBoolR with (b := b).
auto.
exists None.
apply ELtErrorR.
auto.
exists None.
apply ELtBoolL with (b := b).
auto.
exists None.
apply ELtErrorL.
auto.
inversion IHe1.
destruct x.
destruct v.
exists None.
apply EIfInt with (n := n).
auto.
destruct b.
inversion IHe2.
destruct x.
exists (Some v).
apply EIfT.
auto.
auto.
exists None.
apply EIfTError.
auto.
auto.
inversion IHe3.
destruct x.
exists (Some v).
apply EIfF.
auto.
auto.
exists None.
apply EIfFError.
auto.
auto.
exists None.
apply EIfError.
auto.
Qed.今回の導出システムは単純な式のみを扱うものなので帰納法と場合分けで簡単に解くことができましたが、次は変数束縛と環境を扱う事になりそうなので楽しみです。
最終的にはHindley-Milnerな型推論器が正しく型付けできているかをCoqで証明できたらいいなぁとか考えてます。
