今日のCoq: Inversion of the typing relation補題

Coq

前回までで作った型付け規則を元に、Types and Programming Languages (The MIT Press)に載っている「Inversion of the typing relation補題」の証明にチャレンジしました。

Inversion of the typing relation補題は

Lemma LambdaRel :
  forall (x : string)
         (t r1 : type)
      	 (body : term)
         (tenv : list (string * type)),
  Some r1 = typing (Lambda x t body) tenv ->
      exists r2 : type,
      Some r2 = typing body ((x,t)::tenv) /\
      r1 = FunT t r2.

のようなやつです。直感的な意味は「あるtermが型を持つなら、そのsubtermも型を持つ」です。ちなみに、Types and Programming Languages (The MIT Press)によると「Immediate from the definithion」らしいですよ。

このような形をした補題が、VarとかBoolとかの各コンストラクタごとに定義されています。今回は、VarとLambdaのやつだけを証明しました。続きはまた明日です。

わかったこと

  • 場合分けはcaseタクティクスで行なう
  • existsはexistsタクティクスで具体的な値を与えるか、eapply ex_introで仮定を導入する

ソースコード

今回からGithubに置くようにしました。
http://github.com/mzp/lambda