今日のCoq: Inversion of the typing relation補題とUniqueness of types定理
今日もTypes and Programming Languages (The MIT Press)に載っている定理の証明です。
type_dec
補題を定義する際に、以下のような定義が必要になりました。
Definition type_dec : forall t1 t2 : type, {t1 = t2} + {t1 <> t2}.
で、これを証明するために、2時間ほどがんばってました。
結局、decide equalityタクティクスで一発でした。ちぇー。
Proof. decide equality. Qed.
Inversion of the typing relation補題
昨日の続きです。
補題の直感的な意味は「ある項tが型を持つなら、そのsubtermも型を持つ」で、その証明は「Immediate from the definithion」らしいです。
証明する戦略は、
- 条件分岐が登場したらcaseタクティクスで場合分け
- 仮定が真ならintroで取り出して、inversionを適用し、reflexivityで証明する
- 仮定が偽ならintroで取り出して、discriminateで証明する
です。
Lemma VarRel : forall (tenv : list (string * type)) (x : string) (r : type), Some r = typing (Var x) tenv -> In (x,r) tenv. 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. Lemma ApplyRel: forall (r : type) (f x : term) (tenv : list (string * type)), Some r = typing (Apply f x) tenv -> exists t : type, Some (FunT t r) = typing f tenv /\ Some t = typing x tenv. Lemma TrueRel: forall (tenv : list (string * type)) (r : type), Some r = typing (Bool true) tenv -> r = BoolT. Lemma FalseRel: forall (tenv : list (string * type)) (r : type), Some r = typing (Bool false) tenv -> r = BoolT. Lemma IfRel: forall (tenv : list (string * type)) (r : type) (t1 t2 t3 : term), Some r = typing (If t1 t2 t3) tenv -> Some BoolT = typing t1 tenv /\ Some r = typing t2 tenv /\ Some r = typing t3 tenv.
lambda/TypeInv.v at 07ff6f65abbd8a3301fe256edbe1deef92bfc898 · mzp/lambda · GitHub
Uniqueness of types定理
初の定理(Theorem)です。
直感的な意味は「ある項tが型を持つらなら、その型は唯一(unique)である」で、その証明は「Exercise」らしいです。
簡単に見えるけれども、けっこう大変でした。tについて場合分けをし、それぞれについてひたすら証明しました。
Theorem type_uniq : forall (tenv : list (string * type)) (r1 r2 : type) (t : term), Some r1 = typing t tenv /\ Some r2 = typing t tenv -> r1 = r2.
lambda/TypeUniq.v at d479c0933ac7aef3ed687cec6a09553f49ac973d · mzp/lambda · GitHub
