RecordSubSubtyping with Records
Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Strings.String.
From PLF Require Import Maps.
From PLF Require Import Smallstep.
From PLF Require Import MoreStlc.
Inductive ty : Type :=
(* proper types *)
| Top : ty
| Base : string → ty
| Arrow : ty → ty → ty
(* record types *)
| RNil : ty
| RCons : string → ty → ty → ty.
Inductive tm : Type :=
(* proper terms *)
| var : string → tm
| app : tm → tm → tm
| abs : string → ty → tm → tm
| rproj : tm → string → tm
(* record terms *)
| rnil : tm
| rcons : string → tm → tm → tm.
Well-Formedness
Inductive record_ty : ty → Prop :=
| RTnil :
record_ty RNil
| RTcons : ∀ i T1 T2,
record_ty (RCons i T1 T2).
Inductive record_tm : tm → Prop :=
| rtnil :
record_tm rnil
| rtcons : ∀ i t1 t2,
record_tm (rcons i t1 t2).
Inductive well_formed_ty : ty → Prop :=
| wfTop :
well_formed_ty Top
| wfBase : ∀ i,
well_formed_ty (Base i)
| wfArrow : ∀ T1 T2,
well_formed_ty T1 →
well_formed_ty T2 →
well_formed_ty (Arrow T1 T2)
| wfRNil :
well_formed_ty RNil
| wfRCons : ∀ i T1 T2,
well_formed_ty T1 →
well_formed_ty T2 →
record_ty T2 →
well_formed_ty (RCons i T1 T2).
Hint Constructors record_ty record_tm well_formed_ty.
Fixpoint subst (x:string) (s:tm) (t:tm) : tm :=
match t with
| var y ⇒ if eqb_string x y then s else t
| abs y T t1 ⇒ abs y T (if eqb_string x y then t1
else (subst x s t1))
| app t1 t2 ⇒ app (subst x s t1) (subst x s t2)
| rproj t1 i ⇒ rproj (subst x s t1) i
| rnil ⇒ rnil
| rcons i t1 tr2 ⇒ rcons 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 (abs x T t)
| v_rnil : value rnil
| v_rcons : ∀ i v vr,
value v →
value vr →
value (rcons i v vr).
Hint Constructors value.
Fixpoint Tlookup (i:string) (Tr:ty) : option ty :=
match Tr with
| RCons i' T Tr' ⇒
if eqb_string i i' then Some T else Tlookup i Tr'
| _ ⇒ None
end.
Fixpoint tlookup (i:string) (tr:tm) : option tm :=
match tr with
| rcons i' t tr' ⇒
if eqb_string 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 →
(app (abs x T t12) v2) --> [x:=v2]t12
| ST_App1 : ∀ t1 t1' t2,
t1 --> t1' →
(app t1 t2) --> (app t1' t2)
| ST_App2 : ∀ v1 t2 t2',
value v1 →
t2 --> t2' →
(app v1 t2) --> (app v1 t2')
| ST_Proj1 : ∀ tr tr' i,
tr --> tr' →
(rproj tr i) --> (rproj tr' i)
| ST_ProjRcd : ∀ tr i vi,
value tr →
tlookup i tr = Some vi →
(rproj tr i) --> vi
| ST_Rcd_Head : ∀ i t1 t1' tr2,
t1 --> t1' →
(rcons i t1 tr2) --> (rcons i t1' tr2)
| ST_Rcd_Tail : ∀ i v1 tr2 tr2',
value v1 →
tr2 --> tr2' →
(rcons i v1 tr2) --> (rcons i v1 tr2')
where "t1 '-->' t2" := (step t1 t2).
Hint Constructors step.
Subtyping
Definition
Reserved Notation "T '<:' U" (at level 40).
Inductive subtype : ty → ty → Prop :=
(* Subtyping between proper types *)
| S_Refl : ∀ T,
well_formed_ty T →
T <: T
| S_Trans : ∀ S U T,
S <: U →
U <: T →
S <: T
| S_Top : ∀ S,
well_formed_ty S →
S <: Top
| S_Arrow : ∀ S1 S2 T1 T2,
T1 <: S1 →
S2 <: T2 →
Arrow S1 S2 <: Arrow T1 T2
(* Subtyping between record types *)
| S_RcdWidth : ∀ i T1 T2,
well_formed_ty (RCons i T1 T2) →
RCons i T1 T2 <: RNil
| S_RcdDepth : ∀ i S1 T1 Sr2 Tr2,
S1 <: T1 →
Sr2 <: Tr2 →
record_ty Sr2 →
record_ty Tr2 →
RCons i S1 Sr2 <: RCons i T1 Tr2
| S_RcdPerm : ∀ i1 i2 T1 T2 Tr3,
well_formed_ty (RCons i1 T1 (RCons i2 T2 Tr3)) →
i1 ≠ i2 →
RCons i1 T1 (RCons i2 T2 Tr3)
<: RCons i2 T2 (RCons i1 T1 Tr3)
where "T '<:' U" := (subtype T U).
Hint Constructors subtype.
Module Examples.
Open Scope string_scope.
Notation x := "x".
Notation y := "y".
Notation z := "z".
Notation j := "j".
Notation k := "k".
Notation i := "i".
Notation A := (Base "A").
Notation B := (Base "B").
Notation C := (Base "C").
Definition TRcd_j :=
(RCons j (Arrow B B) RNil). (* {j:B->B} *)
Definition TRcd_kj :=
RCons k (Arrow A A) TRcd_j. (* {k:C->C,j:B->B} *)
Example subtyping_example_0 :
subtype (Arrow C TRcd_kj)
(Arrow C RNil).
(* 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, make sure you also understand how to prove them on
paper!
Exercise: 2 stars, standard (subtyping_example_1)
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 (Arrow Top TRcd_kj)
(Arrow (Arrow C C) TRcd_j).
(* Top->{k:A->A,j:B->B} <: (C->C)->{j:B->B} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
subtype (Arrow Top TRcd_kj)
(Arrow (Arrow 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 (Arrow RNil (RCons j A RNil))
(Arrow (RCons k B RNil) RNil).
(* {}->{j:A} <: {k:B}->{} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
subtype (Arrow RNil (RCons j A RNil))
(Arrow (RCons k B RNil) RNil).
(* {}->{j:A} <: {k:B}->{} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Example subtyping_example_4 :
subtype (RCons x A (RCons y B (RCons z C RNil)))
(RCons z C (RCons y B (RCons x A RNil))).
(* {x:A,y:B,z:C} <: {z:C,y:B,x:A} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
subtype (RCons x A (RCons y B (RCons z C RNil)))
(RCons z C (RCons y B (RCons x A RNil))).
(* {x:A,y:B,z:C} <: {z:C,y:B,x:A} *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Properties of Subtyping
Well-Formedness
Lemma subtype__wf : ∀ S T,
subtype S T →
well_formed_ty T ∧ well_formed_ty S.
Lemma wf_rcd_lookup : ∀ i T Ti,
well_formed_ty T →
Tlookup i T = Some Ti →
well_formed_ty Ti.
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.
Exercise: 3 stars, standard (rcd_types_match_informal)
Write a careful informal proof of the rcd_types_match lemma.(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_rcd_types_match_informal : option (nat×string) := None.
☐
Lemma sub_inversion_arrow : ∀ U V1 V2,
subtype U (Arrow V1 V2) →
∃ U1 U2,
(U=(Arrow U1 U2)) ∧ (subtype V1 U1) ∧ (subtype U2 V2).
subtype U (Arrow V1 V2) →
∃ U1 U2,
(U=(Arrow U1 U2)) ∧ (subtype V1 U1) ∧ (subtype U2 V2).
Definition context := partial_map ty.
Reserved Notation "Gamma '⊢' t '∈' T" (at level 40).
Inductive has_type : context → tm → ty → Prop :=
| T_Var : ∀ Gamma x T,
Gamma x = Some T →
well_formed_ty T →
Gamma ⊢ var x \in T
| T_Abs : ∀ Gamma x T11 T12 t12,
well_formed_ty T11 →
update Gamma x T11 ⊢ t12 \in T12 →
Gamma ⊢ abs x T11 t12 \in Arrow T11 T12
| T_App : ∀ T1 T2 Gamma t1 t2,
Gamma ⊢ t1 \in Arrow T1 T2 →
Gamma ⊢ t2 \in T1 →
Gamma ⊢ app t1 t2 \in T2
| T_Proj : ∀ Gamma i t T Ti,
Gamma ⊢ t \in T →
Tlookup i T = Some Ti →
Gamma ⊢ rproj t i \in Ti
(* Subsumption *)
| T_Sub : ∀ Gamma t S T,
Gamma ⊢ t \in S →
subtype S T →
Gamma ⊢ t \in T
(* Rules for record terms *)
| T_RNil : ∀ Gamma,
Gamma ⊢ rnil \in RNil
| T_RCons : ∀ Gamma i t T tr Tr,
Gamma ⊢ t \in T →
Gamma ⊢ tr \in Tr →
record_ty Tr →
record_tm tr →
Gamma ⊢ rcons i t tr \in RCons i T Tr
where "Gamma '⊢' t '∈' T" := (has_type Gamma t T).
Hint Constructors has_type.
Definition trcd_kj :=
(rcons k (abs z A (var z))
(rcons j (abs z B (var z))
rnil)).
Example typing_example_0 :
has_type empty
(rcons k (abs z A (var z))
(rcons j (abs z B (var z))
rnil))
TRcd_kj.
(* empty ⊢ {k=(\z:A.z), j=(\z:B.z)} : {k:A->A,j:B->B} *)
(rcons k (abs z A (var z))
(rcons j (abs z B (var z))
rnil)).
Example typing_example_0 :
has_type empty
(rcons k (abs z A (var z))
(rcons j (abs z B (var z))
rnil))
TRcd_kj.
(* empty ⊢ {k=(\z:A.z), j=(\z:B.z)} : {k:A->A,j:B->B} *)
Example typing_example_1 :
has_type empty
(app (abs x TRcd_j (rproj (var x) j))
(trcd_kj))
(Arrow B B).
(* empty ⊢ (\x:{k:A->A,j:B->B}. x.j)
{k=(\z:A.z), j=(\z:B.z)}
: B->B *)
has_type empty
(app (abs x TRcd_j (rproj (var x) j))
(trcd_kj))
(Arrow B B).
(* empty ⊢ (\x:{k:A->A,j:B->B}. x.j)
{k=(\z:A.z), j=(\z:B.z)}
: B->B *)
Example typing_example_2 :
has_type empty
(app (abs z (Arrow (Arrow C C) TRcd_j)
(rproj (app (var z)
(abs x C (var x)))
j))
(abs z (Arrow C C) trcd_kj))
(Arrow 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 *)
End Examples2.
has_type empty
(app (abs z (Arrow (Arrow C C) TRcd_j)
(rproj (app (var z)
(abs x C (var x)))
j))
(abs z (Arrow C C) trcd_kj))
(Arrow 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 *)
End Examples2.
Lemma has_type__wf : ∀ Gamma t T,
has_type Gamma t T → well_formed_ty T.
Lemma step_preserves_record_tm : ∀ tr tr',
record_tm tr →
tr --> tr' →
record_tm tr'.
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.
Lemma canonical_forms_of_arrow_types : ∀ Gamma s T1 T2,
has_type Gamma s (Arrow T1 T2) →
value s →
∃ x S1 s2,
s = abs x S1 s2.
Theorem progress : ∀ t T,
has_type empty t T →
value t ∨ ∃ t', t --> t'.
has_type Gamma s (Arrow T1 T2) →
value s →
∃ x S1 s2,
s = abs x S1 s2.
Theorem progress : ∀ t T,
has_type empty t T →
value t ∨ ∃ t', t --> t'.
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
proceed by induction on the given typing derivation.
- The cases where the last step in the typing derivation is
T_Abs or T_RNil are immediate because abstractions and
{} are always values. The case for 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. But then (\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
are a term tr, a type Tr, and a 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_ty
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 : ∀ Gamma x T,
has_type Gamma (var x) T →
∃ S,
Gamma x = Some S ∧ subtype S T.
Lemma typing_inversion_app : ∀ Gamma t1 t2 T2,
has_type Gamma (app t1 t2) T2 →
∃ T1,
has_type Gamma t1 (Arrow T1 T2) ∧
has_type Gamma t2 T1.
Lemma typing_inversion_abs : ∀ Gamma x S1 t2 T,
has_type Gamma (abs x S1 t2) T →
(∃ S2, subtype (Arrow S1 S2) T
∧ has_type (update Gamma x S1) t2 S2).
Lemma typing_inversion_proj : ∀ Gamma i t1 Ti,
has_type Gamma (rproj t1 i) Ti →
∃ T Si,
Tlookup i T = Some Si ∧ subtype Si Ti ∧ has_type Gamma t1 T.
Lemma typing_inversion_rcons : ∀ Gamma i ti tr T,
has_type Gamma (rcons i ti tr) T →
∃ Si Sr,
subtype (RCons i Si Sr) T ∧ has_type Gamma ti Si ∧
record_tm tr ∧ has_type Gamma tr Sr.
Lemma abs_arrow : ∀ x S1 s2 T1 T2,
has_type empty (abs x S1 s2) (Arrow T1 T2) →
subtype T1 S1
∧ has_type (update empty x S1) s2 T2.
Inductive appears_free_in : string → tm → Prop :=
| afi_var : ∀ x,
appears_free_in x (var x)
| afi_app1 : ∀ x t1 t2,
appears_free_in x t1 → appears_free_in x (app t1 t2)
| afi_app2 : ∀ x t1 t2,
appears_free_in x t2 → appears_free_in x (app t1 t2)
| afi_abs : ∀ x y T11 t12,
y ≠ x →
appears_free_in x t12 →
appears_free_in x (abs y T11 t12)
| afi_proj : ∀ x t i,
appears_free_in x t →
appears_free_in x (rproj t i)
| afi_rhead : ∀ x i t tr,
appears_free_in x t →
appears_free_in x (rcons i t tr)
| afi_rtail : ∀ x i t tr,
appears_free_in x tr →
appears_free_in x (rcons i t tr).
Hint Constructors appears_free_in.
Lemma context_invariance : ∀ Gamma Gamma' t S,
has_type Gamma t S →
(∀ x, appears_free_in x t → Gamma x = Gamma' x) →
has_type Gamma' t S.
Lemma free_in_context : ∀ x t T Gamma,
appears_free_in x t →
has_type Gamma t T →
∃ T', Gamma x = Some T'.
Lemma substitution_preserves_typing : ∀ Gamma x U v t S,
has_type (update Gamma x U) t S →
has_type empty v U →
has_type Gamma ([x:=v]t) S.
Theorem preservation : ∀ t t' T,
has_type empty t T →
t --> t' →
has_type empty t' T.
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_ty tr,
record_tm Tr, empty ⊢ t1 : T1 and empty ⊢ tr : Tr.
(* 30 Apr 2020 *)