RecordSubSubtyping with Records
Inductive ty : Type :=
(* proper types *)
| TTop : ty
| TBase : id → ty
| TArrow : ty → ty → ty
(* record types *)
| TRNil : ty
| TRCons : id → ty → ty → ty.
Inductive tm : Type :=
(* proper terms *)
| tvar : id → tm
| tapp : tm → tm → tm
| tabs : id → ty → tm → tm
| tproj : tm → id → tm
(* record terms *)
| trnil : tm
| trcons : id → tm → tm → tm.
Inductive record_ty : ty → Prop :=
| RTnil :
record_ty TRNil
| RTcons : ∀i T1 T2,
record_ty (TRCons i T1 T2).
Inductive record_tm : tm → Prop :=
| rtnil :
record_tm trnil
| rtcons : ∀i t1 t2,
record_tm (trcons i t1 t2).
Inductive well_formed_ty : ty → Prop :=
| wfTTop :
well_formed_ty TTop
| wfTBase : ∀i,
well_formed_ty (TBase i)
| wfTArrow : ∀T1 T2,
well_formed_ty T1 →
well_formed_ty T2 →
well_formed_ty (TArrow T1 T2)
| wfTRNil :
well_formed_ty TRNil
| wfTRCons : ∀i T1 T2,
well_formed_ty T1 →
well_formed_ty T2 →
record_ty T2 →
well_formed_ty (TRCons i T1 T2).
Hint Constructors record_ty record_tm well_formed_ty.
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tvar y ⇒ if beq_id x y then s else t
| tabs y T t1 ⇒ tabs y T (if beq_id x y then t1 else (subst x s t1))
| tapp t1 t2 ⇒ tapp (subst x s t1) (subst x s t2)
| tproj t1 i ⇒ tproj (subst x s t1) i
| trnil ⇒ trnil
| trcons i t1 tr2 ⇒ trcons i (subst x s t1) (subst x s tr2)
end.
Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
Inductive value : tm → Prop :=
| v_abs : ∀x T t,
value (tabs x T t)
| v_rnil : value trnil
| v_rcons : ∀i v vr,
value v →
value vr →
value (trcons i v vr).
Hint Constructors value.
Fixpoint Tlookup (i:id) (Tr:ty) : option ty :=
match Tr with
| TRCons i' T Tr' ⇒ if beq_id i i' then Some T else Tlookup i Tr'
| _ ⇒ None
end.
Fixpoint tlookup (i:id) (tr:tm) : option tm :=
match tr with
| trcons i' t tr' ⇒ if beq_id i i' then Some t else tlookup i tr'
| _ ⇒ None
end.
Reserved Notation "t1 '⇒' t2" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀x T t12 v2,
value v2 →
(tapp (tabs x T t12) v2) ⇒ [x:=v2]t12
| ST_App1 : ∀t1 t1' t2,
t1 ⇒ t1' →
(tapp t1 t2) ⇒ (tapp t1' t2)
| ST_App2 : ∀v1 t2 t2',
value v1 →
t2 ⇒ t2' →
(tapp v1 t2) ⇒ (tapp v1 t2')
| ST_Proj1 : ∀tr tr' i,
tr ⇒ tr' →
(tproj tr i) ⇒ (tproj tr' i)
| ST_ProjRcd : ∀tr i vi,
value tr →
tlookup i tr = Some vi →
(tproj tr i) ⇒ vi
| ST_Rcd_Head : ∀i t1 t1' tr2,
t1 ⇒ t1' →
(trcons i t1 tr2) ⇒ (trcons i t1' tr2)
| ST_Rcd_Tail : ∀i v1 tr2 tr2',
value v1 →
tr2 ⇒ tr2' →
(trcons i v1 tr2) ⇒ (trcons i v1 tr2')
where "t1 '⇒' t2" := (step t1 t2).
Hint Constructors step.
Subtyping
Definition
Inductive subtype : ty → ty → Prop :=
(* Subtyping between proper types *)
| S_Refl : ∀T,
well_formed_ty T →
subtype T T
| S_Trans : ∀S U T,
subtype S U →
subtype U T →
subtype S T
| S_Top : ∀S,
well_formed_ty S →
subtype S TTop
| S_Arrow : ∀S1 S2 T1 T2,
subtype T1 S1 →
subtype S2 T2 →
subtype (TArrow S1 S2) (TArrow T1 T2)
(* Subtyping between record types *)
| S_RcdWidth : ∀i T1 T2,
well_formed_ty (TRCons i T1 T2) →
subtype (TRCons i T1 T2) TRNil
| S_RcdDepth : ∀i S1 T1 Sr2 Tr2,
subtype S1 T1 →
subtype Sr2 Tr2 →
record_ty Sr2 →
record_ty Tr2 →
subtype (TRCons i S1 Sr2) (TRCons i T1 Tr2)
| S_RcdPerm : ∀i1 i2 T1 T2 Tr3,
well_formed_ty (TRCons i1 T1 (TRCons i2 T2 Tr3)) →
i1 ≠ i2 →
subtype (TRCons i1 T1 (TRCons i2 T2 Tr3))
(TRCons i2 T2 (TRCons i1 T1 Tr3)).
Hint Constructors subtype.
Module Examples.
Notation x := (Id 0).
Notation y := (Id 1).
Notation z := (Id 2).
Notation j := (Id 3).
Notation k := (Id 4).
Notation i := (Id 5).
Notation A := (TBase (Id 6)).
Notation B := (TBase (Id 7)).
Notation C := (TBase (Id 8)).
Definition TRcd_j :=
(TRCons j (TArrow B B) TRNil). (* {j:B->B} *)
Definition TRcd_kj :=
TRCons k (TArrow A A) TRcd_j. (* {k:C->C,j:B->B} *)
Example subtyping_example_0 :
subtype (TArrow C TRcd_kj)
(TArrow C TRNil).
(* C->{k:A->A,j:B->B} <: C->{} *)
Proof.
apply S_Arrow.
apply S_Refl. auto.
unfold TRcd_kj, TRcd_j. apply S_RcdWidth; auto.
Qed.
The following facts are mostly easy to prove in Coq. To get
full benefit from the exercises, make sure you also
understand how to prove them on paper!
Exercise: 2 stars
Example subtyping_example_1 :
subtype TRcd_kj TRcd_j.
(* {k:A->A,j:B->B} <: {j:B->B} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
subtype TRcd_kj TRcd_j.
(* {k:A->A,j:B->B} <: {j:B->B} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Example subtyping_example_2 :
subtype (TArrow TTop TRcd_kj)
(TArrow (TArrow C C) TRcd_j).
(* Top->{k:A->A,j:B->B} <: (C->C)->{j:B->B} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
subtype (TArrow TTop TRcd_kj)
(TArrow (TArrow C C) TRcd_j).
(* Top->{k:A->A,j:B->B} <: (C->C)->{j:B->B} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Example subtyping_example_3 :
subtype (TArrow TRNil (TRCons j A TRNil))
(TArrow (TRCons k B TRNil) TRNil).
(* {}->{j:A} <: {k:B}->{} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
subtype (TArrow TRNil (TRCons j A TRNil))
(TArrow (TRCons k B TRNil) TRNil).
(* {}->{j:A} <: {k:B}->{} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Example subtyping_example_4 :
subtype (TRCons x A (TRCons y B (TRCons z C TRNil)))
(TRCons z C (TRCons y B (TRCons x A TRNil))).
(* {x:A,y:B,z:C} <: {z:C,y:B,x:A} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
subtype (TRCons x A (TRCons y B (TRCons z C TRNil)))
(TRCons z C (TRCons y B (TRCons x A TRNil))).
(* {x:A,y:B,z:C} <: {z:C,y:B,x:A} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Definition trcd_kj :=
(trcons k (tabs z A (tvar z))
(trcons j (tabs z B (tvar z))
trnil)).
End Examples.
Lemma subtype__wf : ∀S T,
subtype S T →
well_formed_ty T ∧ well_formed_ty S.
Proof with eauto.
intros S T Hsub.
induction Hsub;
intros; try (destruct IHHsub1; destruct IHHsub2)...
- (* S_RcdPerm *)
split... inversion H. subst. inversion H5... Qed.
Lemma wf_rcd_lookup : ∀i T Ti,
well_formed_ty T →
Tlookup i T = Some Ti →
well_formed_ty Ti.
Proof with eauto.
intros i T.
induction T; intros; try solve by inversion.
- (* TRCons *)
inversion H. subst. unfold Tlookup in H0.
destruct (beq_id i i0)... inversion H0; subst... Qed.
Field Lookup
Lemma rcd_types_match : ∀S T i Ti,
subtype S T →
Tlookup i T = Some Ti →
∃Si, Tlookup i S = Some Si ∧ subtype Si Ti.
Proof with (eauto using wf_rcd_lookup).
intros S T i Ti Hsub Hget. generalize dependent Ti.
induction Hsub; intros Ti Hget;
try solve by inversion.
- (* S_Refl *)
∃Ti...
- (* S_Trans *)
destruct (IHHsub2 Ti) as [Ui Hui]... destruct Hui.
destruct (IHHsub1 Ui) as [Si Hsi]... destruct Hsi.
∃Si...
- (* S_RcdDepth *)
rename i0 into k.
unfold Tlookup. unfold Tlookup in Hget.
destruct (beq_id i k)...
+ (* i = k -- we're looking up the first field *)
inversion Hget. subst. ∃S1...
- (* S_RcdPerm *)
∃Ti. split.
+ (* lookup *)
unfold Tlookup. unfold Tlookup in Hget.
destruct (beq_idP i i1)...
× (* i = i1 -- we're looking up the first field *)
destruct (beq_idP i i2)...
(* i = i2 -- contradictory *)
destruct H0.
subst...
+ (* subtype *)
inversion H. subst. inversion H5. subst... Qed.
Exercise: 3 stars (rcd_types_match_informal)
Write a careful informal proof of the rcd_types_match lemma.(* FILL IN HERE *)
Lemma sub_inversion_arrow : ∀U V1 V2,
subtype U (TArrow V1 V2) →
∃U1, ∃U2,
(U=(TArrow U1 U2)) ∧ (subtype V1 U1) ∧ (subtype U2 V2).
Proof with eauto.
intros U V1 V2 Hs.
remember (TArrow V1 V2) as V.
generalize dependent V2. generalize dependent V1.
(* FILL IN HERE *) Admitted.
subtype U (TArrow V1 V2) →
∃U1, ∃U2,
(U=(TArrow U1 U2)) ∧ (subtype V1 U1) ∧ (subtype U2 V2).
Proof with eauto.
intros U V1 V2 Hs.
remember (TArrow V1 V2) as V.
generalize dependent V2. generalize dependent V1.
(* FILL IN HERE *) Admitted.
☐
Definition context := partial_map ty.
Reserved Notation "Gamma '⊢' t '∈' T" (at level 40).
Inductive has_type : context → tm → ty → Prop :=
| T_Var : ∀Γ x T,
Γ x = Some T →
well_formed_ty T →
has_type Γ (tvar x) T
| T_Abs : ∀Γ x T11 T12 t12,
well_formed_ty T11 →
has_type (update Γ x T11) t12 T12 →
has_type Γ (tabs x T11 t12) (TArrow T11 T12)
| T_App : ∀T1 T2 Γ t1 t2,
has_type Γ t1 (TArrow T1 T2) →
has_type Γ t2 T1 →
has_type Γ (tapp t1 t2) T2
| T_Proj : ∀Γ i t T Ti,
has_type Γ t T →
Tlookup i T = Some Ti →
has_type Γ (tproj t i) Ti
(* Subsumption *)
| T_Sub : ∀Γ t S T,
has_type Γ t S →
subtype S T →
has_type Γ t T
(* Rules for record terms *)
| T_RNil : ∀Γ,
has_type Γ trnil TRNil
| T_RCons : ∀Γ i t T tr Tr,
has_type Γ t T →
has_type Γ tr Tr →
record_ty Tr →
record_tm tr →
has_type Γ (trcons i t tr) (TRCons i T Tr)
where "Gamma '⊢' t '∈' T" := (has_type Γ t T).
Hint Constructors has_type.
Example typing_example_0 :
has_type empty
(trcons k (tabs z A (tvar z))
(trcons j (tabs z B (tvar z))
trnil))
TRcd_kj.
(* empty |- {k=(\z:A.z), j=(\z:B.z)} : {k:A->A,j:B->B} *)
Proof.
(* FILL IN HERE *) Admitted.
has_type empty
(trcons k (tabs z A (tvar z))
(trcons j (tabs z B (tvar z))
trnil))
TRcd_kj.
(* empty |- {k=(\z:A.z), j=(\z:B.z)} : {k:A->A,j:B->B} *)
Proof.
(* FILL IN HERE *) Admitted.
Example typing_example_1 :
has_type empty
(tapp (tabs x TRcd_j (tproj (tvar x) j))
(trcd_kj))
(TArrow B B).
(* empty |- (\x:{k:A->A,j:B->B}. x.j) {k=(\z:A.z), j=(\z:B.z)} : B->B *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
has_type empty
(tapp (tabs x TRcd_j (tproj (tvar x) j))
(trcd_kj))
(TArrow B B).
(* empty |- (\x:{k:A->A,j:B->B}. x.j) {k=(\z:A.z), j=(\z:B.z)} : B->B *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Example typing_example_2 :
has_type empty
(tapp (tabs z (TArrow (TArrow C C) TRcd_j)
(tproj (tapp (tvar z)
(tabs x C (tvar x)))
j))
(tabs z (TArrow C C) trcd_kj))
(TArrow B B).
(* empty |- (\z:(C->C)->{j:B->B}. (z (\x:C.x)).j)
(\z:C->C. {k=(\z:A.z), j=(\z:B.z)})
: B->B *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
has_type empty
(tapp (tabs z (TArrow (TArrow C C) TRcd_j)
(tproj (tapp (tvar z)
(tabs x C (tvar x)))
j))
(tabs z (TArrow C C) trcd_kj))
(TArrow B B).
(* empty |- (\z:(C->C)->{j:B->B}. (z (\x:C.x)).j)
(\z:C->C. {k=(\z:A.z), j=(\z:B.z)})
: B->B *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Lemma has_type__wf : ∀Γ t T,
has_type Γ t T → well_formed_ty T.
Proof with eauto.
intros Γ t T Htyp.
induction Htyp...
- (* T_App *)
inversion IHHtyp1...
- (* T_Proj *)
eapply wf_rcd_lookup...
- (* T_Sub *)
apply subtype__wf in H.
destruct H...
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; eauto.
Qed.
Lemma lookup_field_in_value : ∀v T i Ti,
value v →
has_type empty v T →
Tlookup i T = Some Ti →
∃vi, tlookup i v = Some vi ∧ has_type empty vi Ti.
Proof with eauto.
remember empty as Γ.
intros t T i Ti Hval Htyp. revert Ti HeqGamma Hval.
induction Htyp; intros; subst; try solve by inversion.
- (* T_Sub *)
apply (rcd_types_match S) in H0... destruct H0 as [Si [HgetSi Hsub]].
destruct (IHHtyp Si) as [vi [Hget Htyvi]]...
- (* T_RCons *)
simpl in H0. simpl. simpl in H1.
destruct (beq_id i i0).
+ (* i is first *)
inversion H1. subst. ∃t...
+ (* i in tail *)
destruct (IHHtyp2 Ti) as [vi [get Htyvi]]...
inversion Hval... Qed.
Lemma canonical_forms_of_arrow_types : ∀Γ s T1 T2,
has_type Γ s (TArrow T1 T2) →
value s →
∃x, ∃S1, ∃s2,
s = tabs x S1 s2.
Proof with eauto.
(* FILL IN HERE *) Admitted.
has_type Γ s (TArrow T1 T2) →
value s →
∃x, ∃S1, ∃s2,
s = tabs x S1 s2.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Theorem progress : ∀t T,
has_type empty t T →
value t ∨ ∃t', t ⇒ t'.
Proof with eauto.
intros t T Ht.
remember empty as Γ.
revert HeqGamma.
induction Ht;
intros HeqGamma; subst...
- (* T_Var *)
inversion H.
- (* T_App *)
right.
destruct IHHt1; subst...
+ (* t1 is a value *)
destruct IHHt2; subst...
× (* t2 is a value *)
destruct (canonical_forms_of_arrow_types empty t1 T1 T2)
as [x [S1 [t12 Heqt1]]]...
subst. ∃([x:=t2]t12)...
× (* t2 steps *)
destruct H0 as [t2' Hstp]. ∃(tapp t1 t2')...
+ (* t1 steps *)
destruct H as [t1' Hstp]. ∃(tapp t1' t2)...
- (* T_Proj *)
right. destruct IHHt...
+ (* rcd is value *)
destruct (lookup_field_in_value t T i Ti) as [t' [Hget Ht']]...
+ (* rcd_steps *)
destruct H0 as [t' Hstp]. ∃(tproj t' i)...
- (* T_RCons *)
destruct IHHt1...
+ (* head is a value *)
destruct IHHt2...
× (* tail steps *)
right. destruct H2 as [tr' Hstp].
∃(trcons i t tr')...
+ (* head steps *)
right. destruct H1 as [t' Hstp].
∃(trcons i t' tr)... Qed.
Informal proof of progress:
Theorem : For any term t and type T, if empty ⊢ t : T
then t is a value or t ⇒ t' for some term t'.
Proof : Let t and T be given such that empty ⊢ t : T. We go
by induction on the typing derivation. Cases T_Abs and
T_RNil are immediate because abstractions and {} are always
values. Case T_Var is vacuous because variables cannot be
typed in the empty context.
- If the last step in the typing derivation is by T_App, then
there are terms t1 t2 and types T1 T2 such that
t = t1 t2, T = T2, empty ⊢ t1 : T1 → T2 and
empty ⊢ t2 : T1.
- Suppose t1 ⇒ t1' for some term t1'. Then
t1 t2 ⇒ t1' t2 by ST_App1.
- Otherwise t1 is a value.
- Suppose t2 ⇒ t2' for some term t2'. Then
t1 t2 ⇒ t1 t2' by rule ST_App2 because t1 is a value.
- Otherwise, t2 is a value. By lemma
canonical_forms_for_arrow_types, t1 = \x:S1.s2 for some
x, S1, and s2. And (\x:S1.s2) t2 ⇒ [x:=t2]s2 by
ST_AppAbs, since t2 is a value.
- Suppose t2 ⇒ t2' for some term t2'. Then
t1 t2 ⇒ t1 t2' by rule ST_App2 because t1 is a value.
- Suppose t1 ⇒ t1' for some term t1'. Then
t1 t2 ⇒ t1' t2 by ST_App1.
- If the last step of the derivation is by T_Proj, then there
is a term tr, type Tr and label i such that t = tr.i,
empty ⊢ tr : Tr, and Tlookup i Tr = Some T.
- If the final step of the derivation is by T_Sub, then there
is a type S such that S <: T and empty ⊢ t : S. The
desired result is exactly the induction hypothesis for the
typing subderivation.
- If the final step of the derivation is by T_RCons, then there
exist some terms t1 tr, types T1 Tr and a label t such
that t = {i=t1, tr}, T = {i:T1, Tr}, record_tm tr,
record_tm Tr, empty ⊢ t1 : T1 and empty ⊢ tr : Tr.
- Suppose t1 ⇒ t1' for some term t1'. Then
{i=t1, tr} ⇒ {i=t1', tr} by rule ST_Rcd_Head.
- Otherwise t1 is a value.
- Suppose tr ⇒ tr' for some term tr'. Then
{i=t1, tr} ⇒ {i=t1, tr'} by rule ST_Rcd_Tail,
since t1 is a value.
- Otherwise, tr is also a value. So, {i=t1, tr} is a value by v_rcons.
- Suppose tr ⇒ tr' for some term tr'. Then
{i=t1, tr} ⇒ {i=t1, tr'} by rule ST_Rcd_Tail,
since t1 is a value.
- Suppose t1 ⇒ t1' for some term t1'. Then
{i=t1, tr} ⇒ {i=t1', tr} by rule ST_Rcd_Head.
Lemma typing_inversion_var : ∀Γ x T,
has_type Γ (tvar x) T →
∃S,
Γ x = Some S ∧ subtype S T.
Proof with eauto.
intros Γ x T Hty.
remember (tvar x) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_Var *)
∃T...
- (* T_Sub *)
destruct IHHty as [U [Hctx HsubU]]... Qed.
Lemma typing_inversion_app : ∀Γ t1 t2 T2,
has_type Γ (tapp t1 t2) T2 →
∃T1,
has_type Γ t1 (TArrow T1 T2) ∧
has_type Γ t2 T1.
Proof with eauto.
intros Γ t1 t2 T2 Hty.
remember (tapp t1 t2) as t.
induction Hty; intros;
inversion Heqt; subst; try solve by inversion.
- (* T_App *)
∃T1...
- (* T_Sub *)
destruct IHHty as [U1 [Hty1 Hty2]]...
assert (Hwf := has_type__wf _ _ _ Hty2).
∃U1... Qed.
Lemma typing_inversion_abs : ∀Γ x S1 t2 T,
has_type Γ (tabs x S1 t2) T →
(∃S2, subtype (TArrow S1 S2) T
∧ has_type (update Γ x S1) t2 S2).
Proof with eauto.
intros Γ x S1 t2 T H.
remember (tabs x S1 t2) as t.
induction H;
inversion Heqt; subst; intros; try solve by inversion.
- (* T_Abs *)
assert (Hwf := has_type__wf _ _ _ H0).
∃T12...
- (* T_Sub *)
destruct IHhas_type as [S2 [Hsub Hty]]...
Qed.
Lemma typing_inversion_proj : ∀Γ i t1 Ti,
has_type Γ (tproj t1 i) Ti →
∃T, ∃Si,
Tlookup i T = Some Si ∧ subtype Si Ti ∧ has_type Γ t1 T.
Proof with eauto.
intros Γ i t1 Ti H.
remember (tproj t1 i) as t.
induction H;
inversion Heqt; subst; intros; try solve by inversion.
- (* T_Proj *)
assert (well_formed_ty Ti) as Hwf.
{ (* pf of assertion *)
apply (wf_rcd_lookup i T Ti)...
apply has_type__wf in H... }
∃T. ∃Ti...
- (* T_Sub *)
destruct IHhas_type as [U [Ui [Hget [Hsub Hty]]]]...
∃U. ∃Ui... Qed.
Lemma typing_inversion_rcons : ∀Γ i ti tr T,
has_type Γ (trcons i ti tr) T →
∃Si, ∃Sr,
subtype (TRCons i Si Sr) T ∧ has_type Γ ti Si ∧
record_tm tr ∧ has_type Γ tr Sr.
Proof with eauto.
intros Γ i ti tr T Hty.
remember (trcons i ti tr) as t.
induction Hty;
inversion Heqt; subst...
- (* T_Sub *)
apply IHHty in H0.
destruct H0 as [Ri [Rr [HsubRS [HtypRi HtypRr]]]].
∃Ri. ∃Rr...
- (* T_RCons *)
assert (well_formed_ty (TRCons i T Tr)) as Hwf.
{ (* pf of assertion *)
apply has_type__wf in Hty1.
apply has_type__wf in Hty2... }
∃T. ∃Tr... Qed.
Lemma abs_arrow : ∀x S1 s2 T1 T2,
has_type empty (tabs x S1 s2) (TArrow T1 T2) →
subtype T1 S1
∧ has_type (update empty x S1) s2 T2.
Proof with eauto.
intros x S1 s2 T1 T2 Hty.
apply typing_inversion_abs in Hty.
destruct Hty as [S2 [Hsub Hty]].
apply sub_inversion_arrow in Hsub.
destruct Hsub as [U1 [U2 [Heq [Hsub1 Hsub2]]]].
inversion Heq; subst... Qed.
Inductive appears_free_in : id → tm → Prop :=
| afi_var : ∀x,
appears_free_in x (tvar x)
| afi_app1 : ∀x t1 t2,
appears_free_in x t1 → appears_free_in x (tapp t1 t2)
| afi_app2 : ∀x t1 t2,
appears_free_in x t2 → appears_free_in x (tapp t1 t2)
| afi_abs : ∀x y T11 t12,
y ≠ x →
appears_free_in x t12 →
appears_free_in x (tabs y T11 t12)
| afi_proj : ∀x t i,
appears_free_in x t →
appears_free_in x (tproj t i)
| afi_rhead : ∀x i t tr,
appears_free_in x t →
appears_free_in x (trcons i t tr)
| afi_rtail : ∀x i t tr,
appears_free_in x tr →
appears_free_in x (trcons i t 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 Γ'.
induction H;
intros Γ' Heqv...
- (* T_Var *)
apply T_Var... rewrite ← Heqv...
- (* T_Abs *)
apply T_Abs... apply IHhas_type. intros x0 Hafi.
unfold update, t_update. destruct (beq_idP x x0)...
- (* T_App *)
apply T_App with T1...
- (* 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.
induction Htyp; subst; inversion Hafi; subst...
- (* T_Abs *)
destruct (IHHtyp H5) as [T Hctx]. ∃T.
unfold update, t_update in Hctx. rewrite false_beq_id in Hctx... Qed.
Lemma substitution_preserves_typing : ∀Γ x U v t S,
has_type (update Γ x U) t S →
has_type empty v U →
has_type Γ ([x:=v]t) S.
Proof with eauto.
intros Γ x U v t S Htypt Htypv.
generalize dependent S. generalize dependent Γ.
induction t; intros; simpl.
- (* tvar *)
rename i into y.
destruct (typing_inversion_var _ _ _ Htypt) as [T [Hctx Hsub]].
unfold update, t_update in Hctx.
destruct (beq_idP x y)...
+ (* x=y *)
subst.
inversion Hctx; subst. clear Hctx.
apply context_invariance with empty...
intros x Hcontra.
destruct (free_in_context _ _ S empty Hcontra) as [T' HT']...
inversion HT'.
+ (* x<>y *)
destruct (subtype__wf _ _ Hsub)...
- (* tapp *)
destruct (typing_inversion_app _ _ _ _ Htypt) as [T1 [Htypt1 Htypt2]].
eapply T_App...
- (* tabs *)
rename i into y. rename t into T1.
destruct (typing_inversion_abs _ _ _ _ _ Htypt)
as [T2 [Hsub Htypt2]].
destruct (subtype__wf _ _ Hsub) as [Hwf1 Hwf2].
inversion Hwf2. subst.
apply T_Sub with (TArrow T1 T2)... apply T_Abs...
destruct (beq_idP x y).
+ (* x=y *)
eapply context_invariance...
subst.
intros x Hafi. unfold update, t_update.
destruct (beq_id y x)...
+ (* x<>y *)
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (beq_idP y z)...
subst. rewrite false_beq_id...
- (* tproj *)
destruct (typing_inversion_proj _ _ _ _ Htypt)
as [T [Ti [Hget [Hsub Htypt1]]]]...
- (* trnil *)
eapply context_invariance...
intros y Hcontra. inversion Hcontra.
- (* trcons *)
destruct (typing_inversion_rcons _ _ _ _ _ Htypt) as
[Ti [Tr [Hsub [HtypTi [Hrcdt2 HtypTr]]]]].
apply T_Sub with (TRCons i Ti Tr)...
apply T_RCons...
+ (* record_ty Tr *)
apply subtype__wf in Hsub. destruct Hsub. inversion H0...
+ (* record_tm (x:=vt2) *)
inversion Hrcdt2; 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 as Γ. generalize dependent HeqGamma.
generalize dependent t'.
induction HT;
intros t' HeqGamma HE; subst; inversion HE; subst...
- (* T_App *)
inversion HE; subst...
+ (* ST_AppAbs *)
destruct (abs_arrow _ _ _ _ _ HT1) as [HA1 HA2].
apply substitution_preserves_typing with T...
- (* T_Proj *)
destruct (lookup_field_in_value _ _ _ _ H2 HT H)
as [vi [Hget Hty]].
rewrite H4 in Hget. inversion Hget. subst...
- (* T_RCons *)
eauto using step_preserves_record_tm. Qed.
Informal proof of preservation:
Theorem: If t, t' are terms and T is a type such that
empty ⊢ t : T and t ⇒ t', then empty ⊢ t' : T.
Proof: Let t and T be given such that empty ⊢ t : T. We go
by induction on the structure of this typing derivation, leaving
t' general. Cases T_Abs and T_RNil are vacuous because
abstractions and {} don't step. Case T_Var is vacuous as well,
since the context is empty.
- If the final step of the derivation is by T_App, then there
are terms t1 t2 and types T1 T2 such that t = t1 t2,
T = T2, empty ⊢ t1 : T1 → T2 and empty ⊢ t2 : T1.
- If the final step of the derivation is by T_Proj, then there
is a term tr, type Tr and label i such that t = tr.i,
empty ⊢ tr : Tr, and Tlookup i Tr = Some T.
- If the final step of the derivation is by T_Sub, then there
is a type S such that S <: T and empty ⊢ t : S. The
result is immediate by the induction hypothesis for the typing
subderivation and an application of T_Sub.
- If the final step of the derivation is by T_RCons, then there
exist some terms t1 tr, types T1 Tr and a label t such
that t = {i=t1, tr}, T = {i:T1, Tr}, record_tm tr,
record_tm Tr, empty ⊢ t1 : T1 and empty ⊢ tr : Tr.
Exercises on Typing
Exercise: 2 stars, optional (variations)
Each part of this problem suggests a different way of changing the definition of the STLC with records and subtyping. (These changes are not cumulative: each part starts from the original language.) In each part, list which properties (Progress, Preservation, both, or neither) become false. If a property becomes false, give a counterexample.- Suppose we add the following typing rule:
Γ ⊢ t : S1->S2 S1 <: T1 T1 <: S1 S2 <: T2 (T_Funny1) Γ ⊢ t : T1->T2 - Suppose we add the following reduction rule:
(ST_Funny21) {} ⇒ (\x:Top. x) - Suppose we add the following subtyping rule:
(S_Funny3) {} <: Top->Top - Suppose we add the following subtyping rule:
(S_Funny4) Top->Top <: {} - Suppose we add the following evaluation rule:
(ST_Funny5) ({} t) ⇒ (t {}) - Suppose we add the same evaluation rule *and* a new typing rule:
(ST_Funny5) ({} t) ⇒ (t {}) (T_Funny6) empty ⊢ {} : Top->Top - Suppose we *change* the arrow subtyping rule to:
S1 <: T1 S2 <: T2 (S_Arrow') S1->S2 <: T1->T2