Records_J: STLCにレコードを追加する
MoreStlc_J.vで、レコードを、直積のネストされた使用の構文糖衣として扱う方法を見ました。
これは簡単な例にはよいです。しかし、エンコードは非形式的です。
(現実的に、もしこの方法でレコードを本当に扱うならパーサ内で実行されることになりますが、
パーサはここでは省いています。)
そしていずれにしろ、あまり効率的ではありません。
これから、
レコードを言語の第一級(first-class)のメンバーとしてはどのように扱えるのか見るのも興味があるところです。
前の非形式的定義を思い出してみましょう:
前の非形式的定義を思い出してみましょう:
構文:
ti ⇒ ti' (ST_Rcd)
--------------------------------------------------------------------
{i1=v1, ..., im=vm, in=tn, ...} ⇒ {i1=v1, ..., im=vm, in=tn', ...}
t1 ⇒ t1'
-------------- (ST_Proj1)
t1.i ⇒ t1'.i
------------------------- (ST_ProjRcd)
{..., i=vi, ...}.i ⇒ vi
型付け:
Γ ⊢ t1 : T1 ... Γ ⊢ tn : Tn
-------------------------------------------------- (T_Rcd)
Γ ⊢ {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn}
Γ ⊢ t : {..., i:Ti, ...}
----------------------------- (T_Proj)
Γ ⊢ t.i : Ti
t ::= 項:
| ...
| {i1=t1, ..., in=tn} レコード
| t.i 射影
v ::= 値:
| ...
| {i1=v1, ..., in=vn} レコード値
T ::= 型:
| ...
| {i1:T1, ..., in:Tn} レコード型
簡約:
ti ⇒ ti' (ST_Rcd)
--------------------------------------------------------------------
{i1=v1, ..., im=vm, in=tn, ...} ⇒ {i1=v1, ..., im=vm, in=tn', ...}
t1 ⇒ t1'
-------------- (ST_Proj1)
t1.i ⇒ t1'.i
------------------------- (ST_ProjRcd)
{..., i=vi, ...}.i ⇒ vi
型付け:
Γ ⊢ t1 : T1 ... Γ ⊢ tn : Tn
-------------------------------------------------- (T_Rcd)
Γ ⊢ {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn}
Γ ⊢ t : {..., i:Ti, ...}
----------------------------- (T_Proj)
Γ ⊢ t.i : Ti
レコード型の構文を形式化する最も明らかな方法はこうです:
Module FirstTry.
Definition alist (X : Type) := list (id * X).
Inductive ty : Type :=
| ty_base : id → ty
| ty_arrow : ty → ty → ty
| ty_rcd : (alist ty) → ty.
残念ながら、ここで Coq の限界につきあたりました。
この型は期待する帰納原理を自動的には提供してくれないのです。
ty_rcdの場合の帰納法の仮定はリストのty要素について何の情報も提供してくれないのです。
このせいで、行いたい証明に対してこの型は役に立たなくなっています。
(* Check ty_ind.
====>
ty_ind :
forall P : ty -> Prop,
(forall i : id, P (ty_base i)) ->
(forall t : ty, P t -> forall t0 : ty, P t0 -> P (ty_arrow t t0)) ->
(forall a : alist ty, P (ty_rcd a)) -> (* ??? *)
forall t : ty, P t
*)
より良い帰納法の原理をCoqから取り出すこともできます。
しかしそれをやるための詳細はあまりきれいではありません。
またCoqが単純なInductive定義に対して自動生成したものほど直観的でもありません。
幸い、レコードについて、別の、ある意味より単純でより自然な形式化方法があります。 既存のlist型の代わりに、型の構文にリストのコンストラクタ("nil"と"cons") を本質的に含めてしまうという方法です。
幸い、レコードについて、別の、ある意味より単純でより自然な形式化方法があります。 既存のlist型の代わりに、型の構文にリストのコンストラクタ("nil"と"cons") を本質的に含めてしまうという方法です。
Inductive ty : Type :=
| ty_base : id → ty
| ty_arrow : ty → ty → ty
| ty_rnil : ty
| ty_rcons : id → ty → ty → ty.
Tactic Notation "ty_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "ty_base" | Case_aux c "ty_arrow"
| Case_aux c "ty_rnil" | Case_aux c "ty_rcons" ].
同様に、項のレベルで、空レコードに対応するコンストラクタtm_rnilと、
フィールドのリストの前に1つのフィールドを追加するコンストラクタtm_rconsを用意します。
(* レコード *)
| tm_proj : tm → id → tm
| tm_rnil : tm
| tm_rcons : id → tm → tm → tm.
Tactic Notation "tm_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "tm_var" | Case_aux c "tm_app" | Case_aux c "tm_abs"
| Case_aux c "tm_proj" | Case_aux c "tm_rnil" | Case_aux c "tm_rcons" ].
| tm_rnil : tm
| tm_rcons : id → tm → tm → tm.
Tactic Notation "tm_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "tm_var" | Case_aux c "tm_app" | Case_aux c "tm_abs"
| Case_aux c "tm_proj" | Case_aux c "tm_rnil" | Case_aux c "tm_rcons" ].
いくつかの変数、例えば...
Notation a := (Id 0).
Notation f := (Id 1).
Notation g := (Id 2).
Notation l := (Id 3).
Notation A := (ty_base (Id 4)).
Notation B := (ty_base (Id 5)).
Notation k := (Id 6).
Notation i1 := (Id 7).
Notation i2 := (Id 8).
{ i1:A }
(* Check (ty_rcons i1 A ty_rnil). *)
{ i1:A→B, i2:A }
(* Check (ty_rcons i1 (ty_arrow A B)
(ty_rcons i2 A ty_rnil)). *)
レコードの抽象構文を(リストから nil/cons 構成に)一般化すると、
次のような奇妙な型を書くことがができるようになります。
ここでレコード型の「後部」は実際にはレコード型ではありません!
以降で型ジャッジメントを、
weird_typeのようなill-formedの(正しくない形の)型が項に割当てられないように構成します。
これをサポートするために、レコード型と項を識別するためのrecord_tyとrecord_tm、
およびill-formedの型を排除するためのwell_formed_tyを定義します。
最初に、型がレコード型なのは、
それの一番外側のレベルがty_rnilとty_rconsだけを使って構築されたもののときです。
Inductive record_ty : ty → Prop :=
| rty_nil :
record_ty ty_rnil
| rty_cons : ∀ i T1 T2,
record_ty (ty_rcons i T1 T2).
同様に、項がレコード項であるのは、
tm_rnilとtm_rconsから構築されたもののときです。
Inductive record_tm : tm → Prop :=
| rtm_nil :
record_tm tm_rnil
| rtm_cons : ∀ i t1 t2,
record_tm (tm_rcons i t1 t2).
record_tyとrecord_tmは再帰的ではないことに注意します。
両者は、一番外側のコンストラクタだけをチェックします。
一方well_formed_tyは型全体がwell-formedか(正しい形をしているか)、
つまり、レコードのすべての後部(ty_rconsの第2引数)がレコードであるか、を検証します。
もちろん、型だけでなく項についても、ill-formedの可能性を考慮しなければなりません。 しかし、別途well_formed_tmを用意しなくても、ill-formed項は型チェックが排除します。 なぜなら、型チェックが既に項の構成を調べるからです。
もちろん、型だけでなく項についても、ill-formedの可能性を考慮しなければなりません。 しかし、別途well_formed_tmを用意しなくても、ill-formed項は型チェックが排除します。 なぜなら、型チェックが既に項の構成を調べるからです。
LATER : should they fill in part of this as an exercise? We
didn't give rules for it above
(訳注：この"LATER"部分が誰向けに何を言おうとしているのかはっきりしないので、
訳さずに残しておきました。)
Inductive well_formed_ty : ty → Prop :=
| wfty_base : ∀ i,
well_formed_ty (ty_base i)
| wfty_arrow : ∀ T1 T2,
well_formed_ty T1 →
well_formed_ty T2 →
well_formed_ty (ty_arrow T1 T2)
| wfty_rnil :
well_formed_ty ty_rnil
| wfty_rcons : ∀ i T1 T2,
well_formed_ty T1 →
well_formed_ty T2 →
record_ty T2 →
well_formed_ty (ty_rcons i T1 T2).
Hint Constructors record_ty record_tm well_formed_ty.
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tm_var y => if beq_id x y then s else t
| tm_abs y T t1 => tm_abs y T (if beq_id x y then t1 else (subst x s t1))
| tm_app t1 t2 => tm_app (subst x s t1) (subst x s t2)
| tm_proj t1 i => tm_proj (subst x s t1) i
| tm_rnil => tm_rnil
| tm_rcons i t1 tr1 => tm_rcons i (subst x s t1) (subst x s tr1)
end.
次に言語の値を定義します。レコードが値であるのは、そのフィールドがすべて値であるときです。
Inductive value : tm → Prop :=
| v_abs : ∀ x T11 t12,
value (tm_abs x T11 t12)
| v_rnil : value tm_rnil
| v_rcons : ∀ i v1 vr,
value v1 →
value vr →
value (tm_rcons i v1 vr).
Hint Constructors value.
レコード型またはレコード項から1つのフィールドを取り出すユーティリティ関数です:
Fixpoint ty_lookup (i:id) (Tr:ty) : option ty :=
match Tr with
| ty_rcons i' T Tr' => if beq_id i i' then Some T else ty_lookup i Tr'
| _ => None
end.
Fixpoint tm_lookup (i:id) (tr:tm) : option tm :=
match tr with
| tm_rcons i' t tr' => if beq_id i i' then Some t else tm_lookup i tr'
| _ => None
end.
step関数は(射影規則について)項レベルのlookup関数を使います。
一方、型レベルのlookupはhas_typeで必要になります。
Reserved Notation "t1 '==>' t2" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀ x T11 t12 v2,
value v2 →
(tm_app (tm_abs x T11 t12) v2) ⇒ (subst x v2 t12)
| ST_App1 : ∀ t1 t1' t2,
t1 ⇒ t1' →
(tm_app t1 t2) ⇒ (tm_app t1' t2)
| ST_App2 : ∀ v1 t2 t2',
value v1 →
t2 ⇒ t2' →
(tm_app v1 t2) ⇒ (tm_app v1 t2')
| ST_Proj1 : ∀ t1 t1' i,
t1 ⇒ t1' →
(tm_proj t1 i) ⇒ (tm_proj t1' i)
| ST_ProjRcd : ∀ tr i vi,
value tr →
tm_lookup i tr = Some vi →
(tm_proj tr i) ⇒ vi
| ST_Rcd_Head : ∀ i t1 t1' tr2,
t1 ⇒ t1' →
(tm_rcons i t1 tr2) ⇒ (tm_rcons i t1' tr2)
| ST_Rcd_Tail : ∀ i v1 tr2 tr2',
value v1 →
tr2 ⇒ tr2' →
(tm_rcons i v1 tr2) ⇒ (tm_rcons i v1 tr2')
where "t1 '==>' t2" := (step t1 t2).
Tactic Notation "step_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "ST_AppAbs" | Case_aux c "ST_App1" | Case_aux c "ST_App2"
| Case_aux c "ST_Proj1" | Case_aux c "ST_ProjRcd"
| Case_aux c "ST_Rcd_Head" | Case_aux c "ST_Rcd_Tail" ].
Notation stepmany := (refl_step_closure step).
Notation "t1 '==>*' t2" := (stepmany t1 t2) (at level 40).
Hint Constructors step.
次に型付け規則を定義します。これは上述の推論規則をほぼそのまま転写したものです。
大きな違いはwell_formed_tyの使用だけです。
非形式的な表記では、well-formedレコード型だけを許す文法を使ったので、
別のチェックを用意する必要はありませんでした。
ここでは、has_type Γ t T が成立するときは常に well_formed_ty T が成立するようにしたいところです。つまり、has_type は項にill-formed型を割当てることはないようにするということです。 このことを後で実際に証明します。
しかしながらhas_typeの定義を、well_formed_ty を不必要に使って取り散らかしたくはありません。 その代わりwell_formed_tyによるチェックを必要な所だけに配置します。 ここで、必要な所というのは、has_type の帰納的呼び出しによっても未だ型のwell-formed性のチェックが行われていない所のことです。
例えば、T_Varの場合、well_formed_ty T をチェックします。 なぜなら、Tの形がwell-formedであることを調べる帰納的なhas_typeの呼び出しがないからです。 同様にT_Absの場合、well_formed_ty T11 の証明を必要とします。 なぜなら、has_typeの帰納的呼び出しは T12 がwell-formedであることだけを保証するからです。
読者が記述しなければならない規則の中でwell_formed_tyチェックが必要なのは、 tm_nilの場合だけです。
ここでは、has_type Γ t T が成立するときは常に well_formed_ty T が成立するようにしたいところです。つまり、has_type は項にill-formed型を割当てることはないようにするということです。 このことを後で実際に証明します。
しかしながらhas_typeの定義を、well_formed_ty を不必要に使って取り散らかしたくはありません。 その代わりwell_formed_tyによるチェックを必要な所だけに配置します。 ここで、必要な所というのは、has_type の帰納的呼び出しによっても未だ型のwell-formed性のチェックが行われていない所のことです。
例えば、T_Varの場合、well_formed_ty T をチェックします。 なぜなら、Tの形がwell-formedであることを調べる帰納的なhas_typeの呼び出しがないからです。 同様にT_Absの場合、well_formed_ty T11 の証明を必要とします。 なぜなら、has_typeの帰納的呼び出しは T12 がwell-formedであることだけを保証するからです。
読者が記述しなければならない規則の中でwell_formed_tyチェックが必要なのは、 tm_nilの場合だけです。
Inductive has_type : context → tm → ty → Prop :=
| T_Var : ∀ Γ x T,
Γ x = Some T →
well_formed_ty T →
has_type Γ (tm_var x) T
| T_Abs : ∀ Γ x T11 T12 t12,
well_formed_ty T11 →
has_type (extend Γ x T11) t12 T12 →
has_type Γ (tm_abs x T11 t12) (ty_arrow T11 T12)
| T_App : ∀ T1 T2 Γ t1 t2,
has_type Γ t1 (ty_arrow T1 T2) →
has_type Γ t2 T1 →
has_type Γ (tm_app t1 t2) T2
| T_Proj : ∀ Γ i t Ti Tr,
has_type Γ t Tr →
ty_lookup i Tr = Some Ti →
has_type Γ (tm_proj t i) Ti
| T_RNil : ∀ Γ,
has_type Γ tm_rnil ty_rnil
| T_RCons : ∀ Γ i t T tr Tr,
has_type Γ t T →
has_type Γ tr Tr →
record_ty Tr →
record_tm tr →
has_type Γ (tm_rcons i t tr) (ty_rcons i T Tr).
Hint Constructors has_type.
Tactic Notation "has_type_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "T_Var" | Case_aux c "T_Abs" | Case_aux c "T_App"
| Case_aux c "T_Proj" | Case_aux c "T_RNil" | Case_aux c "T_RCons" ].
証明を完成させなさい。
証明の中ではCoq の自動化機能を自由に使って構いません。
しかし、もし型システムがどのように動作するか確信できていないなら、
最初に基本機能(特にeapplyではなくapply)を使った証明を行い、
次に自動化を使ってその証明を圧縮するのがよいかもしれません。
Lemma typing_example_2 :
has_type empty
(tm_app (tm_abs a (ty_rcons i1 (ty_arrow A A)
(ty_rcons i2 (ty_arrow B B)
ty_rnil))
(tm_proj (tm_var a) i2))
(tm_rcons i1 (tm_abs a A (tm_var a))
(tm_rcons i2 (tm_abs a B (tm_var a))
tm_rnil)))
(ty_arrow B B).
Proof.
Admitted.
次の事実(あるいはすぐ上の事実も!)の証明を始める前に、
それが何を主張しているかを確認しなさい。
Example typing_nonexample :
~ ∃ T,
has_type (extend empty a (ty_rcons i2 (ty_arrow A A)
ty_rnil))
(tm_rcons i1 (tm_abs a B (tm_var a)) (tm_var a))
T.
Proof.
Admitted.
Example typing_nonexample_2 : ∀ y,
~ ∃ T,
has_type (extend empty y A)
(tm_app (tm_abs a (ty_rcons i1 A ty_rnil)
(tm_proj (tm_var a) i1))
(tm_rcons i1 (tm_var y) (tm_rcons i2 (tm_var y) tm_rnil)))
T.
Proof.
Admitted.
このシステムの進行と保存の証明は、純粋な単純型付きラムダ計算のものと本質的に同じです。
しかし、レコードについての技術的補題を追加する必要があります。
Lemma wf_rcd_lookup : ∀ i T Ti,
well_formed_ty T →
ty_lookup i T = Some Ti →
well_formed_ty Ti.
Proof with eauto.
intros i T.
ty_cases (induction T) Case; intros; try solve by inversion.
Case "ty_rcons".
inversion H. subst. unfold ty_lookup in H0.
remember (beq_id i i0) as b. destruct b; subst...
inversion H0. subst... Qed.
Lemma step_preserves_record_tm : ∀ tr tr',
record_tm tr →
tr ⇒ tr' →
record_tm tr'.
Proof.
intros tr tr' Hrt Hstp.
inversion Hrt; subst; inversion Hstp; subst; auto.
Qed.
Lemma has_type__wf : ∀ Γ t T,
has_type Γ t T → well_formed_ty T.
Proof with eauto.
intros Γ t T Htyp.
has_type_cases (induction Htyp) Case...
Case "T_App".
inversion IHHtyp1...
Case "T_Proj".
eapply wf_rcd_lookup...
Qed.
補題: もし empty ⊢ v : T で、かつ ty_lookup i T が Some Ti を返すならば,
tm_lookup i v はある項 ti について Some ti を返す。
ただし、has_type empty ti Ti となる。
証明: 型の導出Htypについての帰納法で証明する。 ty_lookup i T = Some Ti であることから、 T はレコード型でなければならない。 このこととvが値であることから、ほとんどの場合は精査で除去でき、 T_RConsの場合だけが残る。
型導出の最後のステップがT_RConsによるものであるとき、 あるi0、t、tr、T、Trについて t = tm_rcons i0 t tr かつ T = ty_rcons i0 T Tr である。
このとき2つの可能性が残る。i0 = i か、そうでないかである。
証明: 型の導出Htypについての帰納法で証明する。 ty_lookup i T = Some Ti であることから、 T はレコード型でなければならない。 このこととvが値であることから、ほとんどの場合は精査で除去でき、 T_RConsの場合だけが残る。
型導出の最後のステップがT_RConsによるものであるとき、 あるi0、t、tr、T、Trについて t = tm_rcons i0 t tr かつ T = ty_rcons i0 T Tr である。
このとき2つの可能性が残る。i0 = i か、そうでないかである。
- i = i0 のとき、ty_lookup i (ty_rcons i0 T Tr) = Some Ti から
T = Ti となる。これから t自身が定理を満たすことが言える。
- 一方、i <> i0 とする。すると
ty_lookup i T = ty_lookup i Tr
かつ
tm_lookup i t = tm_lookup i tr
となる。 これから、帰納法の仮定より結果が得られる。
Lemma lookup_field_in_value : ∀ v T i Ti,
value v →
has_type empty v T →
ty_lookup i T = Some Ti →
∃ ti, tm_lookup i v = Some ti ∧ has_type empty ti Ti.
Proof with eauto.
intros v T i Ti Hval Htyp Hget.
remember (@empty ty) as Γ.
has_type_cases (induction Htyp) Case; subst; try solve by inversion...
Case "T_RCons".
simpl in Hget. simpl. destruct (beq_id i i0).
SCase "i is first".
simpl. inversion Hget. subst.
∃ t...
SCase "get tail".
destruct IHHtyp2 as [vi [Hgeti Htypi]]...
inversion Hval... Qed.
Theorem progress : ∀ t T,
has_type empty t T →
value t ∨ ∃ t', t ⇒ t'.
Proof with eauto.
intros t T Ht.
remember (@empty ty) as Γ.
generalize dependent HeqGamma.
has_type_cases (induction Ht) Case; intros HeqGamma; subst.
Case "T_Var".
inversion H.
Case "T_Abs".
left...
Case "T_App".
right.
destruct IHHt1; subst...
SCase "t1 is a value".
destruct IHHt2; subst...
SSCase "t2 is a value".
inversion H; subst; try (solve by inversion).
∃ (subst x t2 t12)...
SSCase "t2 steps".
destruct H0 as [t2' Hstp]. ∃ (tm_app t1 t2')...
SCase "t1 steps".
destruct H as [t1' Hstp]. ∃ (tm_app t1' t2)...
Case "T_Proj".
right. destruct IHHt...
SCase "rcd is value".
destruct (lookup_field_in_value _ _ _ _ H0 Ht H) as [ti [Hlkup _]].
∃ ti...
SCase "rcd_steps".
destruct H0 as [t' Hstp]. ∃ (tm_proj t' i)...
Case "T_RNil".
left...
Case "T_RCons".
destruct IHHt1...
SCase "head is a value".
destruct IHHt2; try reflexivity.
SSCase "tail is a value".
left...
SSCase "tail steps".
right. destruct H2 as [tr' Hstp].
∃ (tm_rcons i t tr')...
SCase "head steps".
right. destruct H1 as [t' Hstp].
∃ (tm_rcons i t' tr)... Qed.
Inductive appears_free_in : id → tm → Prop :=
| afi_var : ∀ x,
appears_free_in x (tm_var x)
| afi_app1 : ∀ x t1 t2,
appears_free_in x t1 → appears_free_in x (tm_app t1 t2)
| afi_app2 : ∀ x t1 t2,
appears_free_in x t2 → appears_free_in x (tm_app t1 t2)
| afi_abs : ∀ x y T11 t12,
y <> x →
appears_free_in x t12 →
appears_free_in x (tm_abs y T11 t12)
| afi_proj : ∀ x t i,
appears_free_in x t →
appears_free_in x (tm_proj t i)
| afi_rhead : ∀ x i ti tr,
appears_free_in x ti →
appears_free_in x (tm_rcons i ti tr)
| afi_rtail : ∀ x i ti tr,
appears_free_in x tr →
appears_free_in x (tm_rcons i ti tr).
Hint Constructors appears_free_in.
Lemma context_invariance : ∀ Γ Γ' t S,
has_type Γ t S →
(∀ x, appears_free_in x t → Γ x = Γ' x) →
has_type Γ' t S.
Proof with eauto.
intros. generalize dependent Γ'.
has_type_cases (induction H) Case;
intros Γ' Heqv...
Case "T_Var".
apply T_Var... rewrite ← Heqv...
Case "T_Abs".
apply T_Abs... apply IHhas_type. intros y Hafi.
unfold extend. remember (beq_id x y) as e.
destruct e...
Case "T_App".
apply T_App with T1...
Case "T_RCons".
apply T_RCons... Qed.
Lemma free_in_context : ∀ x t T Γ,
appears_free_in x t →
has_type Γ t T →
∃ T', Γ x = Some T'.
Proof with eauto.
intros x t T Γ Hafi Htyp.
has_type_cases (induction Htyp) Case; inversion Hafi; subst...
Case "T_Abs".
destruct IHHtyp as [T' Hctx]... ∃ T'.
unfold extend in Hctx.
apply not_eq_beq_id_false in H3. rewrite H3 in Hctx...
Qed.
Lemma substitution_preserves_typing : ∀ Γ x U v t S,
has_type (extend Γ x U) t S →
has_type empty v U →
has_type Γ (subst x v t) S.
Proof with eauto.
intros Γ x U v t S Htypt Htypv.
generalize dependent Γ. generalize dependent S.
tm_cases (induction t) Case;
intros S Γ Htypt; simpl; inversion Htypt; subst...
Case "tm_var".
simpl. rename i into y.
remember (beq_id x y) as e. destruct e.
SCase "x=y".
apply beq_id_eq in Heqe. subst.
unfold extend in H0. rewrite ← beq_id_refl in H0.
inversion H0; subst. clear H0.
eapply context_invariance...
intros x Hcontra.
destruct (free_in_context _ _ S empty Hcontra) as [T' HT']...
inversion HT'.
SCase "x<>y".
apply T_Var... unfold extend in H0. rewrite ← Heqe in H0...
Case "tm_abs".
rename i into y. rename t into T11.
apply T_Abs...
remember (beq_id x y) as e. destruct e.
SCase "x=y".
eapply context_invariance...
apply beq_id_eq in Heqe. subst.
intros x Hafi. unfold extend.
destruct (beq_id y x)...
SCase "x<>y".
apply IHt. eapply context_invariance...
intros z Hafi. unfold extend.
remember (beq_id y z) as e0. destruct e0...
apply beq_id_eq in Heqe0. subst.
rewrite ← Heqe...
Case "tm_rcons".
apply T_RCons... inversion H7; subst; simpl...
Qed.
Theorem preservation : ∀ t t' T,
has_type empty t T →
t ⇒ t' →
has_type empty t' T.
Proof with eauto.
intros t t' T HT.
remember (@empty ty) as Γ. generalize dependent HeqGamma.
generalize dependent t'.
has_type_cases (induction HT) Case;
intros t' HeqGamma HE; subst; inversion HE; subst...
Case "T_App".
inversion HE; subst...
SCase "ST_AppAbs".
apply substitution_preserves_typing with T1...
inversion HT1...
Case "T_Proj".
destruct (lookup_field_in_value _ _ _ _ H2 HT H)
as [vi [Hget Htyp]].
rewrite H4 in Hget. inversion Hget. subst...
Case "T_RCons".
apply T_RCons... eapply step_preserves_record_tm...
Qed.
☐