TaPL輪講/9章/9.3.9 定理の証明
Γ |- t : T かつ t -> t' ならば Γ |- t' : T
(証明)
Γ |- t : Tの導出(の深さ)に関する帰納法
t'は任意にとらないほうがいい気がする
(T-Var, T-True, T-False, T-Absの場合)
ありえない
tはすでに正規形なのでt -> t'という仮定に反する
(T-Appの場合)
t = t1 t2
H: t -> t'
Γ |- t1 : T11 -> T12
Γ |- t2 : T11
Γ |- t1 t2 : T12
IH: 任意のt'について (Γ |- t1 t2 : T12 かつ) t1 t2 -> t' ならば Γ |- t' : T12
Goal: Γ |- t' : T12
Hについて場合分け
(E-App1の場合)
t1 -> t1'
t1 t2 -> t1' t2
IHがそのまま使える
(E-App2の場合)
t1 = v1
t2 -> t2'
v1 t2 -> v1 t2'
IHがそのまま使える
(E-AppAbsの場合)
t1 = λx:T11. t12
t2 = v2
t1 t2 -> (x |-> v2) t12
Γ |- λx:T11. t12 : T11 -> T12 についてinversion lemmaを使う
Γ, x:T11 |- t12 : T12
Γ |- v2 : T11を思い出すとsubstitution lemmaからΓ |- (x |-> v2) t12 : T11
よって題意を得る
(T-True, T-Falseの場合)
ありえない
(T-Ifの場合)
t = if t1 then t2 else t3
H: Γ |- t : T
H1: Γ |- t1 : Bool
H2: Γ |- t2 : T
H3: Γ |- t3 : T
IH1: 任意のt1'について Γ |- t1 : Bool かつ t1 -> t1' ならば Γ |- t1' : Bool
IH2: 任意のt2'について Γ |- t2 : T かつ t2 -> t2' ならば Γ |- t2' : T
IH3: 任意のt3'について Γ |- t3 : T かつ t3 -> t3' ならば Γ |- t3' : T
Goal: Γ |- t' : T
t -> t'について場合分け
(E-IfTrueの場合)
t1 = true
このとき if t1 then t2 else t3 -> t2
H2よりOK
(E-IfFalseの場合)
同様にOK
(E-Ifの場合)
あるt1'があってt1 -> t1'
H1とIH1よりΓ |- t1' : Bool
これとH2, H3よりΓ |- if t1' then t2 else t3 : T
よってOK
以上よりT-Ifの場合に示された
以上よりOK