Coqの練習にプログラミング言語の基礎概念に出てくる、EvalML1における評価の一意性について証明したので公開したいと思います。
最初に、ML1における式を表す型を定義します。
int型はnatではなくてZあたりで表現したかったのですが、使い方が分からなかった ので断念しました。int型をnatで表現したのに伴って減算が省略されていますが、両者ともあまり本質的ではないので目をつぶってください。
Require Import Arith. 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.
別に比較関数が正しく実装されていなくても目的の性質は示せますが、念のために証明しておきます。
Lemma blt_nat_true : forall (n1 n2 : nat),
blt_nat n1 n2 = true <-> n1 < n2.
Proof.
intros n1.
induction n1 as [| n1'].
intros n2.
split.
intros H.
destruct n2 as [| n2'].
inversion H.
apply lt_0_Sn.
intros H.
destruct n2 as [| n2'].
inversion H.
reflexivity.
intros n2.
split.
intros H.
destruct n2 as [| n2'].
inversion H.
apply -> NPeano.Nat.succ_lt_mono.
apply IHn1'.
apply H.
intros H.
destruct n2 as [| n2'].
inversion H.
simpl.
apply IHn1'.
apply <- NPeano.Nat.succ_lt_mono.
apply H.
Qed.
Lemma blt_nat_false : forall (n1 n2 : nat),
blt_nat n1 n2 = false <-> ~(n1 < n2).
Proof.
intros n1.
induction n1 as [| n1'].
intros n2.
split.
intros H.
destruct n2 as [| n2'].
intros H0.
inversion H0.
inversion H.
intros H.
destruct n2 as [| n2'].
reflexivity.
exfalso.
apply H.
apply lt_0_Sn.
intros n2.
split.
intros H.
destruct n2 as [| n2'].
intros H0.
inversion H0.
simpl in H.
apply IHn1' in H.
rewrite <- NPeano.Nat.succ_lt_mono.
apply H.
intros H.
destruct n2 as [| n2'].
reflexivity.
simpl.
apply IHn1'.
rewrite -> NPeano.Nat.succ_lt_mono.
apply H.
Qed.最後に、ML1の式が値に評価されることを表す命題を定義します。
Inductive evalto : exp -> value -> Prop :=
| EInt : forall (n : nat), evalto (ExpInt n) (VInt n)
| EBool : forall (b : bool), evalto (ExpBool b) (VBool b)
| EIfT : forall (e1 e2 e3 : exp) (v : value),
evalto e1 (VBool true) ->
evalto e2 v ->
evalto (ExpIf e1 e2 e3) v
| EIfF : forall (e1 e2 e3 : exp) (v : value),
evalto e1 (VBool false) ->
evalto e3 v ->
evalto (ExpIf e1 e2 e3) v
| EPlus : forall (e1 e2 : exp) (n1 n2 n3 : nat),
evalto e1 (VInt n1) ->
evalto e2 (VInt n2) ->
n1 + n2 = n3 ->
evalto (ExpPlus e1 e2) (VInt n3)
| ETimes : forall (e1 e2 : exp) (n1 n2 n3 : nat),
evalto e1 (VInt n1) ->
evalto e2 (VInt n2) ->
n1 * n2 = n3 ->
evalto (ExpTimes e1 e2) (VInt n3)
| ELt : forall (e1 e2 : exp) (n1 n2 : nat) (b : bool),
evalto e1 (VInt n1) ->
evalto e2 (VInt n2) ->
blt_nat n1 n2 = b ->
evalto (ExpLt e1 e2) (VBool b).
Infix "evalto" := evalto (at level 70, no associativity).以上の定義によって準備が整いました。問題の評価の一意性を証明します。
肝心の証明はとにかく場合分けの数が多い上単調なので、極力自動証明に頼ることにします。
Theorem evalto_unique : forall (e : exp) (v1 v2 : 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 (VInt n1 = VInt n0).
auto.
assert (VInt n2 = VInt n4).
auto.
congruence.
intros v1 v2 H H0.
inversion H.
inversion H0.
assert (VInt n1 = VInt n0).
auto.
assert (VInt n2 = VInt n4).
auto.
congruence.
intros v1 v2 H H0.
inversion H.
inversion H0.
assert (VInt n1 = VInt n0).
auto.
assert (VInt n2 = VInt n3).
auto.
congruence.
intros v1 v2 H H0.
inversion H.
inversion H0.
auto.
assert (VBool true = VBool false).
auto.
congruence.
inversion H0.
assert (VBool true = VBool false).
auto.
congruence.
auto.
Qed.
