型システムで推論プログラムを書くようにcoqコードを書き、coqで証明をやってみる

背景

prologサンプルコードをふと書いてみる - ラシウラで書かれたコードのように、普通の(関数型)プログラミングだと戻り値に結果を返すようなコードになるところは、

  • 戻り値となる変数をパラメータの最後に置く
  • その戻り値パラメータが、結果としてどのようなパターンになるかを書く
  • サブ関数を呼び出すばあいは、本体部分に並べる(戻り値は最後の変数に入る感じのアナロジーで)
  • 引数パターンごとにルールを定義する

というように対応付けて書き換えることで、Prologプログラムが書けます。

eval(Env, ref(Var), Result) :-
        get(Env, Var, Result).

はHaskellの

eval env (Ref var) = result
  where
     result = get env var

という感じのコードに対応したものになるでしょう。

さらにPrologコードをHaskellの型システムで書く - ラシウラでは、Prologで書いた形無しラムダ計算のevaluatorをと同等のものを、prolog同様推論システムになっているHaskell(GHCの拡張)型システムの推論で行うように書きました。

Prologのコードにあたる部分を、Haskellのclassとinstanceを使って、型のところにパターンで書くことで、型システムの型推論によって計算されて結果が出ました。

上記のPrologコードに当たる部分は、型システム推論コードでは前後が逆になり

class Eval env term value | env term -> value where
  ...
instance (Get env var result) => Eval env (Ref var) result

のようになります。

やること

このパターンの流れで、証明補助機coqで形無しラムダ式の(環境を用いたタイプの)evaluatorを定義し、いくつかの証明を行ってみます。プログラムは以下のようになります:

  • データ型(にあたるもの)も関数(にあたるもの)は、すべてParameterとInductive(Haskellでいうとdataやclass)で定義する
    • すなわち前述の型システムによるコードと同じスタイル
  • 証明はevalの証明、すなわち想定される入力と想定される結果を並べた論理式を証明する
    • autoでは証明が終わらないが、intro(s),apply,exactだけで証明される

前述のevalの部分関数は、coqコードで以下のように定義することになります:

Inductive Eval : Env -> Term -> Value -> Prop :=
...
| EvalRef: forall env name result,
    Get env name result ->
    Eval env (Ref name) result
...

各パターンに名前が付きいろいろ量が増えていることを無視すれば、前述のコードと対応付けされていることがわかるでしょう。

証明は具体例として、(\x->x) v => vになることを証明したり、もっと一般的に(\x->x)自体を証明したりする。前者は、coqでかくと

Theorem example1: forall x v,
    Eval ENil (Apply (Lambda x (Ref x)) (Literal v)) (Const v).

という感じになり、これをcoqの証明戦略intros、apply等で証明することになります。

本来は、さらに一般化して正規形とか、チャーチロッサー定理とかを証明したりするのだが、今回は省略しました。



coqでevaluatorを定義する方法はほかにもいくつかあるが、今回のやり方はCoqIntroを読む - ラシウラで用いているPOPL08チュートリアルでとられたスタイルに似たようになってます。ただし、POPL08チュートリアルでは環境は使わずtermの置換(substitution)による評価を使っています。

以下coqでのプログラミングを順に説明します。コード全体は最後に載せました。ツールであるcoqcやcoqtop等のコマンドの使い方は証明補助coqを使ってみる - ラシウラなどに書いてます。

各種データの定義

まずデータ型に当たるものを定義していきます。coqは対話型でもあるので、ソースファイル(eval.v)にはふつう必要なものは上から順に書いてくことになります。

変数名、数字データ

まずはじめに、変数名につかう名前と値を定義する。データのうち構造を持たない場合はParameterでラベルだけ定義する。データ型の型はふつうSetを使います。

(* name and direct value *)
Parameter Name : Set.
Parameter Int : Set.

ちなみに(*と*)でかこまれるのはcoqのコメントです。
さらにParameter X: Name. とか Parameter Ten : Int.とかやれば定数のようなものも定義できる。が、今回でもここまでやる必要はないでしょう。

式データ

いわゆる形無しラムダ式の項 Term = Literal value | Ref name | Lambda arg body | Apply operator operand の定義。

(* terms *)
Inductive Term : Set :=
| Literal (value : Int)
| Ref (name : Name)
| Lambda (arg : Name) (body : Term)
| Apply (operator operand : Term).

データ型なのでSet、各データのパラメータには変数名と型を指定します。

POPL08チュートリアルでは、変数名を使わず、各データのコンストラクタの型を->を使って書いてます。以下はそのように書いた場合です。

Inductive Term : Set :=
| Literal : Int -> Term
| Ref : Name -> Term
| Lambda : Name -> Term -> Term
| Apply : Term -> Term -> Term.

これも基本的に同じです。

環境データと値データ

環境と値は相互に参照しあうデータです。環境は値を保持し、クロージャ値は環境を保持します。
このような場合はInductive ... with ... with ...で並べて書きます。

(* env and value *)
Inductive Env : Set :=
| ENil
| ECell (name: Name) (value: Value) (next : Env)
with Value : Set :=
| NotFound
| Const (value : Int)
| Closure (env : Env) (arg : Name) (body : Term).

環境用関数の定義

環境から値を取得するGetと、環境に変数名:値ペアを追加するExtを定義します。

Getと、coqでの関数の作り方

関数(にあたるもの)もInductiveで書きます。ただし関数の型は、引数1 -> 引数2 ... -> 結果 -> Propというように最後に->Propが付いた型になります。PropというのはTrueかFalseのいわゆるBooleanの型です。

以下は環境と名前から値を引き出すGet関数の定義です。

Inductive Get : Env -> Name -> Value -> Prop :=
| GetNotFound : forall name,
    Get ENil name NotFound
| GetMatch : forall name value next,
    Get (ECell name value next) name value
| GetNotMatch: forall name value next pname result,
    name <> pname ->
    Get next pname result ->
    Get (ECell name value next) pname result.

関数(にあたるもの)をつくっていく手順は以下のようになります。

  • Inductive 関数名 : 関数型 := ... を書く
  • (引数の)各パターンごとに書き分ける
    • パターンにはそれぞれ名前をつける
    • 関数を呼び出したときの引数と結果のパターンを書く: 関数名 引数1パターン ... 結果パターン
    • ダイレクトにパターンが欠けない場合は、サブパターンや条件を ->をつけ前側においていく
    • 最後にパターン変数にあたるものは、宣言するようにforallで頭に並べる
  • 最後にピリオドを忘れないように

Get関数の場合、まず、Getの引数はEnvとNameであり、戻り値はValueなので、

Inductive Get : Env -> Name -> Value -> Prop :=

次にGetのパターンはEnvがENiとECellのとき、さらにECellのときはそのname部分がGetの引数と同じときと違うとき、の3パターンになるので、名前をつけ並べます:

Inductive Get : Env -> Name -> Value -> Prop :=
| GetNotFound :
| GetMatch :
| GetNotMatch :

GetNotFoundのときはEnvがENilのとき、NotFound値を返すので、Get関数の呼び出しと結果のパターンで書きます:

Inductive Get : Env -> Name -> Value -> Prop :=
| GetNotFound :
    Get ENil name NotFound
| GetMatch :
| GetNotMatch :

そして変数であるnameを頭にforallで並べます。つまりNotFoundのとき、引数nameはなんでもいいという条件になっています:

Inductive Get : Env -> Name -> Value -> Prop :=
| GetNotFound : forall name,
    Get ENil name NotFound
| GetMatch :
| GetNotMatch :

GetMatchも同様にパターンで書けます:

Inductive Get : Env -> Name -> Value -> Prop :=
| GetNotFound : forall name,
    Get ENil name NotFound
| GetMatch : forall name value next,
    Get (ECell name value next) name value
| GetNotMatch :

Getの引数pnameとECell中のnameが違う場合だし、resultのパターンもnextから取り出したものになるので、GetNotMatchは単純にGet呼び出しのパターンでは書けません。
こういう場合はまず呼び出しパターンをわかるところだけ書き、すぐパターンで書けないところはばらばらの仮の変数で全部埋めます:

| GetNotMatch : 
    Get (ECell name value next) pname result

そして、このresultはnextに対してGetを問い合わせた結果になるので->をつけ前に書きます:

| GetNotMatch : 
    Get next pname result ->
    Get (ECell name value next) pname result

またnameとpnameは違うものであるので、それも->をつけて前に書きます。A != Bはcoqでは A <> Bです。not (A = B)でも、not (eq A B)でもいいでしょう:

| GetNotMatch : 
    name <> pname ->
    Get next pname result ->
    Get (ECell name value next) pname result

最後にforallで使った変数を並べて完成です: 

| GetNotMatch : forall name value next pname result 
    name <> pname ->
    Get next pname result ->
    Get (ECell name value next) pname result

ちなみに、今回は使いませんが、Booleanを返す関数(にあたるもの)を書きたい場合は戻り値を変数にするのではなく、引数1 -> ... -> Propという型にします。また、False = not Trueとみなします(notはProp -> Propの関数)。関数の本体にあたる部分にはTrueになるパターンを書くことになります。

Ext

eval中のパターンで書けるので、coqでもExtはわざわざ定義する必要はないです。が、Haskell型システムで書いたときのコードとの対応付けのため、あえて同じように定義しておきます。

Inductive Ext : Env -> Name -> Value -> Env -> Prop :=
| ExtENil: forall name value,
    Ext ENil name value (ECell name value ENil)
| ExtECell: forall env name value,
    Ext env name value (ECell name value env).

上下とも同じパターンなので、coqでは場合わけの必要もありません。

eval関数の定義

EvalもGetと同様に作れます。

(* eval *)
Inductive Eval : Env -> Term -> Value -> Prop :=
| EvalLiteral: forall env value,
    Eval env (Literal value) (Const value)
| EvalRef: forall env name result,
    Get env name result ->
    Eval env (Ref name) result
| EvalLambda: forall env arg body,
    Eval env (Lambda arg body) (Closure env arg body)
| EvalApply: forall env operator cenv arg body operand value extenv result,
    Eval env operator (Closure cenv arg body) ->
    Eval env operand value ->
    Ext cenv arg value extenv ->
    Eval extenv body result ->
    Eval env (Apply operator operand) result.

各部分を、Prolog版やHaskell型システム版のevalコードとの対応付けもできると思います。

証明: evalパターンごと

まず、証明練習としてevalの各パターンが正しいかを証明してみます。どの証明式もInductiveからの定義とまったく同じなので、人間的には明らかなのですが、coqではauto(自動)でやってくれないようです(別に自動戦略があるのかな？)。ただほかの証明もこの証明と似たようになるようなので、証明のよい練習にはなります。

coqtopを使う場合は、いままでのInductiveをeval.vに並べて書き、coqcでコンパイルするとeval.voができ、coqtopでそれを-requireすると、対話的に証明ができるようになります

$ coqc eval.v
$ ledit coqtop -I . -require eval
Welcome to Coq 8.1pl3 (Dec. 2007)

Coq <
EvalLiteralの証明

Lemmaは補題で、証明対象はほかにもTheoremなどがありますが、処理的にはどれも一緒の別名に過ぎません。
補題名はevalLiteralとしました。論理式はEvalLiteralとまったく同じです。以下が証明対象の補題です:

Lemma evalLiteral: forall env value,
    Eval env (Literal value) (Const value).

coqtopにこの補題を入力します:

Coq < Lemma evalLiteral: forall env value,
    Eval env (Literal value) (Const value).
Coq < 1 subgoal

  ============================
   forall (env : Env) (value : Int), Eval env (Literal value) (Const value)

evalLiteral <

型が明示されて、式が表示されます。

証明でまず行うことはintro戦略を使ってforallをはずすことです。intro自体は仮定をforallの変数や->の右辺として移すルールのことです。つまりforallや->を導入(introduce)するルールです。「-> - intro」ルールは、仮定Aのもとで、Bが成り立つ(A├ B) => 仮定なしで、AならばBが成り立つ(├ A->B)、に変換するルールです。ただ証明の場合にはそのルールの逆適用によって外していくので、変な感じはするかもしれません。
はずすのは左から行います:

evalLiteral < intro env.
1 subgoal

  env : Env
  ============================
   forall value : Int, Eval env (Literal value) (Const value)

evalLiteral <

変数名は省略もできます:

evalLiteral < intro.
1 subgoal

  env : Env
  value : Int
  ============================
   Eval env (Literal value) (Const value)

evalLiteral <


コマンドUndoでアンドゥできます。また戦略introsはこのintroを一気に行うものです。

evalLiteral < Undo.
1 subgoal

  ============================
   forall (env : Env) (value : Int), Eval env (Literal value) (Const value)

evalLiteral < intros env value.
1 subgoal

  env : Env
  value : Int
  ============================
   Eval env (Literal value) (Const value)

evalLiteral <

introsでも名前はつけなくても実行されます。名前を書かないと、forallは同じ変数名をつけますが、->の左辺は適当な変数(H，H0，H1など、hypothesisの頭文字か)をつけてしまいます。introsはforallも->も一緒に一気に仮定部に移してしまうため、コードに書くとわかりにくくなるので、自分はあえて名前をつけるようにしています。

forallが外れたら、次はEvalをパターン展開します。この場合apply戦略を使います。この場合EvalLiteralと同じものなので、EvalLiteralを(逆)applyします:

evalLiteral < apply EvalLiteral.
Proof completed.

evalLiteral <

論理式がなくなったので、証明が終わりました。

証明モードから抜けるにはQedコマンドを使います。Qedコマンドによってこの補題は保存されます。保存された補題は以降の証明のapply戦略に用いることができるようになります:

evalLiteral < Qed.
intros env value.
apply EvalLiteral.
evalLiteral is defined

Coq <

coqソースに補題とこの出力された結果を埋め込んでおけば、requireした時点でこの補題を使えるようすることができます。今回の証明のcoqコードは以下のようになります:

Lemma evalLiteral: forall env value,
    Eval env (Literal value) (Const value).
  intros env value.
  apply EvalLiteral.
Qed.

インデントは、証明部分を区別しやすくするようにつけてるだけです。

EvalRefの証明

次は、->のあるEvalRefを証明します。補題は以下:

Lemma evalRef: forall env name result,
    Get env name result ->
    Eval env (Ref name) result.

coqtopにこれを入力し、まずはintros:

Coq < Lemma evalRef: forall env name result,
    Get env name result ->
    Eval env (Ref name) result.
Coq < Coq < 1 subgoal

  ============================
   forall (env : Env) (name : Name) (result : Value),
   Get env name result -> Eval env (Ref name) result

evalRef < intros env name result HGET.
1 subgoal

  env : Env
  name : Name
  result : Value
  HGET : Get env name result
  ============================
   Eval env (Ref name) result

evalRef <

introsでは->まではずします。左辺部はHGETという名前にしてあります。次はEvalのうち項がRefのパターンのものであるので、apply EvalRefをします:

evalRef < apply EvalRef.
1 subgoal

  env : Env
  name : Name
  result : Value
  HGET : Get env name result
  ============================
   Get env name result

evalRef <

目標の論理式は、HGETと同じものです。つまり仮定にあるものそのものである場合は、exact戦略を使って目標達成ができます:

evalRef < exact HGET.
Proof completed.

evalRef <

証明終了し保存します:

evalRef < Qed.
intros env name result HGET.
apply EvalRef.
exact HGET.
evalRef is defined

Coq <
EvalApplyの証明

Evalのパターンのうち一番複雑なEvalApplyを証明してみます。補題は:

Lemma evalApply: forall env operator cenv arg body operand value extenv result,
    Eval env operator (Closure cenv arg body) ->
    Eval env operand value ->
    Ext cenv arg value extenv ->
    Eval extenv body result ->
    Eval env (Apply operator operand) result.

まず、intros:

evalApply < intros env operator cenv arg body operand value extenv result
     HOPR HOPD HEXT HRES.
evalApply < 1 subgoal

  env : Env
  operator : Term
  cenv : Env
  arg : Name
  body : Term
  operand : Term
  value : Value
  extenv : Env
  result : Value
  HOPR : Eval env operator (Closure cenv arg body)
  HOPD : Eval env operand value
  HEXT : Ext cenv arg value extenv
  HRES : Eval extenv body result
  ============================
   Eval env (Apply operator operand) result

evalApply <

次にapply EvalApplyをしてみますが:

evalApply < apply EvalApply.
Toplevel input, characters 0-15
> apply EvalApply.
> ^^^^^^^^^^^^^^^
Error: generated subgoal "Eval env operator (Closure ?22 ?23 ?24)"
has metavariables in it

evalApply <

エラーが出ます。これはパターン展開したあとで?22 ?23 ?24の部分が解決できないというエラーです。
これはつまり、EvalApplyの定義

| EvalApply: forall env operator cenv arg body operand value extenv result,
    Eval env operator (Closure cenv arg body) ->
    Eval env operand value ->
    Ext cenv arg value extenv ->
    Eval extenv body result ->
    Eval env (Apply operator operand) result.

のうち、cenv、arg、bodyがどうなるのかわからないといっています。これを証明の仮定部分の式を使って与えてやる必要があります。以下のように書きます:

apply EvalApply with (cenv := cenv) (arg := arg) (body := body).

cenv := cenvと同じものを書いてるように見えますが、左辺のほうのcenvはEvalApply定義での変数のcenvであり、右辺のほうのcenvはこの証明の仮定部のcenvを指しています。

これをcoqtopに食わせてみます:

evalApply < apply EvalApply with (cenv := cenv) (arg := arg) (body := body).
Toplevel input, characters 0-63
> apply EvalApply with (cenv := cenv) (arg := arg) (body := body).
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: generated subgoal "Eval env operand ?52" has metavariables in it

evalApply <

またエラーが出ました。今度はEvalApply中のvalueがわからないといっています。これも(value := value)で与えます。このようにエラーが出る部分をつぶしていくと、以下の引数で証明が進みました:

evalApply < apply EvalApply with (cenv := cenv) (arg := arg) (body := body) (value := value) (extenv := extenv).
4 subgoals

  env : Env
  operator : Term
  cenv : Env
  arg : Name
  body : Term
  operand : Term
  value : Value
  extenv : Env
  result : Value
  HOPR : Eval env operator (Closure cenv arg body)
  HOPD : Eval env operand value
  HEXT : Ext cenv arg value extenv
  HRES : Eval extenv body result
  ============================
   Eval env operator (Closure cenv arg body)

subgoal 2 is:
 Eval env operand value
subgoal 3 is:
 Ext cenv arg value extenv
subgoal 4 is:
 Eval extenv body result

evalApply <

証明すべき論理式が4つに増えました。これはちょうどEvalApplyの定義のうちの->の数にあたります。つまりA->B->Cのとき、AとBと両方それぞれ証明する必要があるということです。coqの場合はひとつづつ証明してつぶしていくことになります。

この場合は、4つの論理式とも仮定部に同じものがすべてあるので順にexactしていけばいいです:

evalApply < exact HOPR.
3 subgoals

  env : Env
  operator : Term
  cenv : Env
  arg : Name
  body : Term
  operand : Term
  value : Value
  extenv : Env
  result : Value
  HOPR : Eval env operator (Closure cenv arg body)
  HOPD : Eval env operand value
  HEXT : Ext cenv arg value extenv
  HRES : Eval extenv body result
  ============================
   Eval env operand value

subgoal 2 is:
 Ext cenv arg value extenv
subgoal 3 is:
 Eval extenv body result

evalApply <

3つに減りました。次々exactをやります:

evalApply < exact HOPD.
...
evalApply < exact HEXT.
...
evalApply < exact HRES.
Proof completed.

evalApply <

QED

evalApply < Qed.
intros env operator cenv arg body operand value extenv result HOPR HOPD HEXT
 HRES.
apply
 EvalApply
  with
    (cenv := cenv)
    (arg := arg)
    (body := body)
    (value := value)
    (extenv := extenv).
 exact HOPR.
exact HOPD.
exact HEXT.
exact HRES.
evalApply is defined

Coq <

例題: (\x->x) n = nの証明

今度は、すこし複雑なものとして、「プログラム((\x->x) n) を評価すると値が n になる」ことを証明します。
まずこれを論理式の定理として定義します。

Theorem example1: forall x n,
    Eval ENil (Apply (Lambda x (Ref x)) (Literal n)) (Const n).

TheoremもLemmaも別名でありcoq上での意味的には同じです。これにexample1という名前をつけました。

本体には「プログラム((\x->x) n) を評価すると値が n になる」を、論理式にした物を入れます。

  • コード中で使う変数や数値はforallで束縛しておく
  • 環境にはENilを置く
  • evalする項には、プログラム(\x->x) nのAST表現を置く
  • 結果のところには、nの値表現を置く

証明は以下のようになります:

Theorem example1: forall x n,
    Eval ENil (Apply (Lambda x (Ref x)) (Literal n)) (Const n).
  intros x n.
  apply EvalApply with
    (cenv := ENil) (arg := x) (body := Ref x)
    (value := Const n) (extenv := ECell x (Const n) ENil).
  apply EvalLambda.
  apply EvalLiteral.
  apply ExtENil.
  apply EvalRef.
  apply GetMatch.
Qed.

EvalApplyのパターンは複雑になります。証明する論理式が具体的になるほど、applyのパターンにも具体的なものを入れることになるために、複雑化することになる関係があります。

例題: id関数の証明

先の証明対象を少し一般化して、id関数自体の証明をします。つまり、任意の環境、任意のオペランドでも、そのオペランド値を返す、というように一般化することです。

証明対象は以下のようになります:

Theorem idFunc: forall env x term result,
    Eval env term result ->
    Eval env (Apply (Lambda x (Ref x)) term) result.

もっと愚直にかくと、

Theorem idFunc: forall env x term result value,
    Eval env term value ->
    result = value ->
    Eval env (Apply (Lambda x (Ref x)) term) result.

証明は、以下のとおり:

Theorem idFunc: forall env x term result,
    Eval env term result ->
    Eval env (Apply (Lambda x (Ref x)) term) result.
  intros env x term result HARG.
  apply EvalApply with
    (cenv := env)
    (arg := x)
    (body := Ref x)
    (value := result)
    (extenv := ECell x result env).
  apply EvalLambda.
  exact HARG.
  apply ExtECell.
  apply EvalRef.
  apply GetMatch.
Qed.

証明する論理式を一般化したため、applyのパターンもシンプルになっていきました。

まとめ

逆説的に考えると、記述対象の構造や関数を、Inductiveで各パターンごとに帰納的に別々の型として定義するということは、つまりそれらのパターンを構築ルールとみなして、それを元にして構築されたものについての証明をしたい、ということになります。

このようなスタイルでルールを構築するための型システムの機能は、LFというシステムの機能になるようです:

このLFに基づくTwelfという証明システムは、このようなルール記述やそれを使用する証明を行ないやすくした言語や機能を持っています:

Twelfの型システムのエンジンはprologベースになっているようです。また、ベータ簡約のようなルールを作るときcoqではアルファリネーミングが難しくそれを回避するために項をdeBruijn Indexにしたりするのですが、Twelfは自動でアルファリネーミングされる変数が組み込まれていたり、命名規則でforallのようなものを書かなくてよかったりとかあるようです。

言語の特性の証明可能性の点を考えるのであれば、Twelfで言語を定義するのもいいのかもしれません。

全コードeval.v

(*
  $ coqc eval.v
  $ ledit coqtop -I . -require eval
*)


(* name and direct value *)
Parameter Name : Set.
Parameter Int : Set.

(* terms *)
Inductive Term : Set :=
| Literal (value : Int)
| Ref (name : Name)
| Lambda (arg : Name) (body : Term)
| Apply (operator operand : Term).

(* env and value *)
Inductive Env : Set :=
| ENil
| ECell (name: Name) (value: Value) (next : Env)
with Value : Set :=
| NotFound
| Const (value : Int)
| Closure (env : Env) (arg : Name) (body : Term).

(* operators for env *)
Inductive Get : Env -> Name -> Value -> Prop :=
| GetNotFound : forall name,
    Get ENil name NotFound
| GetMatch : forall name value next,
    Get (ECell name value next) name value
| GetNotMatch: forall name value next pname result,
    name <> pname ->
    Get next pname result ->
    Get (ECell name value next) pname result.

Inductive Ext : Env -> Name -> Value -> Env -> Prop :=
| ExtENil: forall name value,
    Ext ENil name value (ECell name value ENil)
| ExtECell: forall env name value,
    Ext env name value (ECell name value env).

(* eval *)
Inductive Eval : Env -> Term -> Value -> Prop :=
| EvalLiteral: forall env value,
    Eval env (Literal value) (Const value)
| EvalRef: forall env name result,
    Get env name result ->
    Eval env (Ref name) result
| EvalLambda: forall env arg body,
    Eval env (Lambda arg body) (Closure env arg body)
| EvalApply: forall env operator cenv arg body operand value extenv result,
    Eval env operator (Closure cenv arg body) ->
    Eval env operand value ->
    Ext cenv arg value extenv ->
    Eval extenv body result ->
    Eval env (Apply operator operand) result.

(* lemmas *)
Lemma evalLiteral: forall env value,
    Eval env (Literal value) (Const value).
  intros.
  apply EvalLiteral.
Qed.
Lemma evalRef: forall env name result,
    Get env name result ->
    Eval env (Ref name) result.
  intros env name result H.
  apply EvalRef.
  exact H.
Qed.
Lemma evalLambda: forall env arg body,
    Eval env (Lambda arg body) (Closure env arg body).
  intros.
  apply EvalLambda.
Qed.
Lemma evalApply: forall env operator cenv arg body operand value extenv result,
    Eval env operator (Closure cenv arg body) ->
    Eval env operand value ->
    Ext cenv arg value extenv ->
    Eval extenv body result ->
    Eval env (Apply operator operand) result.
  intros env operator cenv arg body operand value extenv result
     HOPR HOPD HEXT HRES.
  apply (EvalApply env operator cenv arg body operand value extenv result).
  exact HOPR.
  exact HOPD.
  exact HEXT.
  exact HRES.
Qed.

(* examples *)
Theorem example1: forall x v,
    Eval ENil (Apply (Lambda x (Ref x)) (Literal v)) (Const v).
  intros x v.
  apply EvalApply with
    (cenv := ENil) (arg := x) (body := Ref x)
    (value := Const v) (extenv := ECell x (Const v) ENil).
  apply EvalLambda.
  apply EvalLiteral.
  apply ExtENil.
  apply EvalRef.
  apply GetMatch.
Qed.

Theorem idFunc: forall env x term result,
    Eval env term result ->
    Eval env (Apply (Lambda x (Ref x)) term) result.
  intros env x term result HARG.
  apply EvalApply with
    (cenv := env)
    (arg := x)
    (body := Ref x)
    (value := result)
    (extenv := ECell x result env).
  apply EvalLambda.
  exact HARG.
  apply ExtECell.
  apply EvalRef.
  apply GetMatch.
Qed.