EvalML2における評価の一意性の証明

　前回、前々回は四則演算程度しか持たない導出システムについての証明でしたが、今回は変数束縛や環境を持つ導出システム、EvalML2における評価の一意性を証明しようと思います。例によって元ネタはプログラミング言語の基礎概念です。

　変数を扱うために式にletと変数参照が追加されています。値の定義は前回と変わりません。

Require Import Arith String.
Open Scope string_scope.

Inductive value : Type := 
  | VInt : nat -> value
  | VBool : bool -> value.

Inductive exp : Type :=
  | ExpInt : nat -> exp
  | ExpBool : bool -> exp
  | ExpVar : string -> exp
  | ExpPlus : exp -> exp -> exp
  | ExpTimes : exp -> exp -> exp
  | ExpLt : exp -> exp -> exp
  | ExpIf : exp -> exp -> exp -> exp
  | ExpLet : string -> exp -> exp -> exp.

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.

また、変数を扱うために新しく環境の定義が追加されています。

Inductive environment : Type :=
  | EnvEmpty : environment
  | EnvBind : environment -> string -> value -> environment.

見づらいのでいい感じの構文を追加したかったのですが、既存の構文と干渉するので断念しました。

　次に、ある環境でML2の式が値に評価される事を示す命題を定義します。

Inductive evalto : environment -> exp -> value -> Prop :=
  | EInt : forall (env : environment) (n : nat),
      evalto env (ExpInt n) (VInt n)
  | EBool : forall (env : environment) (b : bool),
      evalto env (ExpBool b) (VBool b)
  | EVar1 : forall (env : environment) (v : value) (x : string),
      evalto (EnvBind env x v) (ExpVar x) v
  | EVar2 : forall (env : environment) (v1 v2 : value) (x y : string),
      x <> y ->
      evalto env (ExpVar x) v2 ->
      evalto (EnvBind env y v1) (ExpVar x) v2
  | EIfT : forall (env : environment) (e1 e2 e3 : exp) (v : value), 
      evalto env e1 (VBool true) ->
      evalto env e2 v ->
      evalto env (ExpIf e1 e2 e3) v
  | EIfF : forall (env : environment) (e1 e2 e3 : exp) (v : value), 
      evalto env e1 (VBool false) ->
      evalto env e3 v ->
      evalto env (ExpIf e1 e2 e3) v
  | EPlus : forall (env : environment) (e1 e2 : exp) (n1 n2 n3 : nat),
      evalto env e1 (VInt n1) ->
      evalto env e2 (VInt n2) ->
      n1 + n2 = n3 ->
      evalto env (ExpPlus e1 e2) (VInt n3)
  | ETimes : forall (env : environment)  (e1 e2 : exp) (n1 n2 n3 : nat),
      evalto env e1 (VInt n1) ->
      evalto env e2 (VInt n2) ->
      n1 * n2 = n3 ->
      evalto env (ExpTimes e1 e2) (VInt n3)
  | ELt : forall (env : environment) (e1 e2 : exp) (n1 n2 : nat) (b : bool),
      evalto env e1 (VInt n1) ->
      evalto env e2 (VInt n2) ->
      blt_nat n1 n2 = b ->
      evalto env (ExpLt e1 e2) (VBool b)
  | ELet : forall (env : environment) (e1 e2 : exp) (v1 v : value) (x : string),
      evalto env e1 v1 ->
      evalto (EnvBind env x v1) e2 v ->
      evalto env (ExpLet x e1 e2) v.

Notation "E |- e 'evalto' v" := (evalto E e v) (at level 70).

今更ながら、environmentは長かったですね。

　評価の一意性を証明する前に、本に載っている非形式的な証明の流れに従って、変数参照の評価の一意性を補題として証明します。

Lemma var_evalto_unique :
  forall (env : environment) (x : string) (v v' : value),
    env |- ExpVar x evalto v ->
    env |- ExpVar x evalto v' ->
    v = v'.
Proof.
  intros env.
  induction env.
    intros x v v' E1.
    inversion E1.

    intros x v0 v' E1 E2.
    assert ({x = s} + {x <> s}).
      apply string_dec.
    destruct H.
      rewrite <- e in E1.
      rewrite <- e in E2.
      inversion E1.
        inversion E2.
          congruence.
          congruence.
        congruence.
        
      inversion E1.
        congruence.
        inversion E2.
          congruence.
          eauto.
Qed.

この文字列が等しいかどうかで場合分けするのが曲者でしたが、仮定にstring_decを導入してdestructすることで無事場合分けできました。関数を書く時には文字列の比較として使える上に証明でも使えるとは、string_dec優秀ですね。

　最後に評価の一意性を証明します。特に詰まった所はありませんでしたが、envを全称量化するとautoでサブゴールが証明できなくなったのでeautoを使っています。

Theorem evalto_unique :
  forall (env : environment) (e : exp) (v v' : value),
    env |- e evalto v -> env |- e evalto v' -> v = v'.
Proof.
  intros env e.
  generalize env.
  induction e.
    intros env0 v v' E1 E2.
    inversion E1.
    inversion E2.
    auto.

    intros env0 v v' E1 E2.
    inversion E1.
    inversion E2.
    auto.
    
    intros env0 v v'.
    apply var_evalto_unique.
    
    intros env0 v v' E1 E2.
    inversion E1.
    inversion E2.
    assert (VInt n1 = VInt n0).
      eauto.
    assert (VInt n2 = VInt n4).
      eauto.
    congruence.
    
    intros env0 v v' E1 E2.
    inversion E1.
    inversion E2.
    assert (VInt n1 = VInt n0).
      eauto.
    assert (VInt n2 = VInt n4).
      eauto.
    congruence.

    intros env0 v v' E1 E2.
    inversion E1.
    inversion E2.
    assert (VInt n1 = VInt n0).
      eauto.
    assert (VInt n2 = VInt n3).
      eauto.
    congruence.
    
    intros env0 v v' E1 E2.
    inversion E1.
      inversion E2.
        eauto.
        
        assert (VBool true = VBool false).
          eauto.
        congruence.
      inversion E2.
        assert (VBool false = VBool true).
          eauto.
        congruence.
        
        eauto.

    intros env0 v v' E1 E2.
    inversion E1.
    inversion E2.
    assert (v1 = v2).
      eauto.
    rewrite <- H13 in H12.
    eauto.
Qed.