SubSubtyping
Set Warnings "-notation-overridden,-parsing".
Require Import Maps.
Require Import Types.
Require Import Smallstep.
Require Import Maps.
Require Import Types.
Require Import Smallstep.
Concepts
A Motivating Example
Person = {name:String, age:Nat} Student = {name:String, age:Nat, gpa:Nat}
(\r:Person. (r.age)+1) {name="Pat",age=21,gpa=1}is not typable, since it applies a function that wants a two-field record to an argument that actually provides three fields, while the T_App rule demands that the domain type of the function being applied must match the type of the argument precisely.
Subtyping and Object-Oriented Languages
The Subsumption Rule
- Defining a binary subtype relation between types.
- Enriching the typing relation to take subtyping into account.
Gamma |- t : S S <: T | (T_Sub) |
Gamma |- t : T |
The Subtype Relation
Structural Rules
S <: U U <: T | (S_Trans) |
S <: T |
(S_Refl) | |
T <: T |
Products
S_{1} <: T_{1} S_{2} <: T_{2} | (S_Prod) |
S_{1} * S_{2} <: T_{1} * T_{2} |
Arrows
f : C → Student
g : (C→Person) → D
That is, f is a function that yields a record of type Student,
and g is a (higher-order) function that expects its argument to be
a function yielding a record of type Person. Also suppose that
Student is a subtype of Person. Then the application g f is
safe even though their types do not match up precisely, because
the only thing g can do with f is to apply it to some
argument (of type C); the result will actually be a Student,
while g will be expecting a Person, but this is safe because
the only thing g can then do is to project out the two fields
that it knows about (name and age), and these will certainly
be among the fields that are present.
g : (C→Person) → D
S_{2} <: T_{2} | (S_Arrow_Co) |
S_{1} → S_{2} <: S_{1} → T_{2} |
T_{1} <: S_{1} S_{2} <: T_{2} | (S_Arrow) |
S_{1} → S_{2} <: T_{1} → T_{2} |
f : Person → C
g : (Student → C) → D
The application g f is safe, because the only thing the body of
g can do with f is to apply it to some argument of type
Student. Since f requires records having (at least) the
fields of a Person, this will always work. So Person → C is a
subtype of Student → C since Student is a subtype of
Person.
g : (Student → C) → D
Records
{name:String, age:Nat, gpa:Nat} <: {name:String, age:Nat}
{name:String, age:Nat} <: {name:String}
{name:String} <: {}
This is known as "width subtyping" for records.
{name:String, age:Nat} <: {name:String}
{name:String} <: {}
{x:Student} <: {x:Person}
This is known as "depth subtyping".
{name:String,age:Nat} <: {age:Nat,name:String}
This is known as "permutation subtyping".
∀ jk in j_{1}..jn, | |
∃ ip in i_{1}..im, such that | |
jk=ip and Sp <: Tk | (S_Rcd) |
{i_{1}:S_{1}...im:Sm} <: {j_{1}:T_{1}...jn:Tn} |
n > m | (S_RcdWidth) |
{i_{1}:T_{1}...in:Tn} <: {i_{1}:T_{1}...im:Tm} |
S_{1} <: T_{1} ... Sn <: Tn | (S_RcdDepth) |
{i_{1}:S_{1}...in:Sn} <: {i_{1}:T_{1}...in:Tn} |
{i_{1}:S_{1}...in:Sn} is a permutation of {j_{1}:T_{1}...jn:Tn} | (S_RcdPerm) |
{i_{1}:S_{1}...in:Sn} <: {j_{1}:T_{1}...jn:Tn} |
- A subclass may not change the argument or result types of a
method of its superclass (i.e., no depth subtyping or no arrow
subtyping, depending how you look at it).
- Each class member (field or method) can be assigned a single
index, adding new indices "on the right" as more members are
added in subclasses (i.e., no permutation for classes).
- A class may implement multiple interfaces — so-called "multiple inheritance" of interfaces (i.e., permutation is allowed for interfaces).
Exercise: 2 stars, recommended (arrow_sub_wrong)
Suppose we had incorrectly defined subtyping as covariant on both the right and the left of arrow types:S_{1} <: T_{1} S_{2} <: T_{2} | (S_Arrow_wrong) |
S_{1} → S_{2} <: T_{1} → T_{2} |
f : Student → Nat
g : (Person → Nat) → Nat
... such that the application g f will get stuck during
execution. (Use informal syntax. No need to prove formally that
the application gets stuck.)
g : (Person → Nat) → Nat
Top
(S_Top) | |
S <: Top |
Summary
- adding a base type Top,
- adding the rule of subsumption
to the typing relation, andGamma |- t : S S <: T (T_Sub) Gamma |- t : T - defining a subtype relation as follows:
S <: U U <: T (S_Trans) S <: T (S_Refl) T <: T (S_Top) S <: Top S_{1} <: T_{1} S_{2} <: T_{2} (S_Prod) S_{1} * S_{2} <: T_{1} * T_{2} T_{1} <: S_{1} S_{2} <: T_{2} (S_Arrow) S_{1} → S_{2} <: T_{1} → T_{2} n > m (S_RcdWidth) {i_{1}:T_{1}...in:Tn} <: {i_{1}:T_{1}...im:Tm} S_{1} <: T_{1} ... Sn <: Tn (S_RcdDepth) {i_{1}:S_{1}...in:Sn} <: {i_{1}:T_{1}...in:Tn} {i_{1}:S_{1}...in:Sn} is a permutation of {j_{1}:T_{1}...jn:Tn} (S_RcdPerm) {i_{1}:S_{1}...in:Sn} <: {j_{1}:T_{1}...jn:Tn}
Exercises
Exercise: 1 star, optional (subtype_instances_tf_1)
Suppose we have types S, T, U, and V with S <: T and U <: V. Which of the following subtyping assertions are then true? Write true or false after each one. (A, B, and C here are base types like Bool, Nat, etc.)- T→S <: T→S
- Top→U <: S→Top
- (C→C) → (A*B) <: (C→C) → (Top*B)
- T→T→U <: S→S→V
- (T→T)→U <: (S→S)→V
- ((T→S)→T)→U <: ((S→T)→S)→V
- S*V <: T*U
Exercise: 2 stars (subtype_order)
The following types happen to form a linear order with respect to subtyping:- Top
- Top → Student
- Student → Person
- Student → Top
- Person → Student
Exercise: 1 star (subtype_instances_tf_2)
Which of the following statements are true? Write true or false after each one.
∀ S T,
S <: T →
S→S <: T→T
∀ S,
S <: A→A →
∃ T,
S = T→T ∧ T <: A
∀ S T_{1} T_{2},
(S <: T_{1} → T_{2}) →
∃ S_{1} S_{2},
S = S_{1} → S_{2} ∧ T_{1} <: S_{1} ∧ S_{2} <: T_{2}
∃ S,
S <: S→S
∃ S,
S→S <: S
∀ S T_{1} T_{2},
S <: T_{1}*T_{2} →
∃ S_{1} S_{2},
S = S_{1}*S_{2} ∧ S_{1} <: T_{1} ∧ S_{2} <: T_{2}
☐
S <: T →
S→S <: T→T
∀ S,
S <: A→A →
∃ T,
S = T→T ∧ T <: A
∀ S T_{1} T_{2},
(S <: T_{1} → T_{2}) →
∃ S_{1} S_{2},
S = S_{1} → S_{2} ∧ T_{1} <: S_{1} ∧ S_{2} <: T_{2}
∃ S,
S <: S→S
∃ S,
S→S <: S
∀ S T_{1} T_{2},
S <: T_{1}*T_{2} →
∃ S_{1} S_{2},
S = S_{1}*S_{2} ∧ S_{1} <: T_{1} ∧ S_{2} <: T_{2}
Exercise: 1 star (subtype_concepts_tf)
Which of the following statements are true, and which are false?- There exists a type that is a supertype of every other type.
- There exists a type that is a subtype of every other type.
- There exists a pair type that is a supertype of every other
pair type.
- There exists a pair type that is a subtype of every other
pair type.
- There exists an arrow type that is a supertype of every other
arrow type.
- There exists an arrow type that is a subtype of every other
arrow type.
- There is an infinite descending chain of distinct types in the
subtype relation—-that is, an infinite sequence of types
S_{0}, S_{1}, etc., such that all the Si's are different and
each S(i+1) is a subtype of Si.
- There is an infinite ascending chain of distinct types in the subtype relation—-that is, an infinite sequence of types S_{0}, S_{1}, etc., such that all the Si's are different and each S(i+1) is a supertype of Si.
Exercise: 2 stars (proper_subtypes)
Is the following statement true or false? Briefly explain your answer. (Here TBase n stands for a base type, where n is a string standing for the name of the base type. See the Syntax section below.)
∀ T,
~(T = TBool ∨ ∃ n, T = TBase n) →
∃ S,
S <: T ∧ S ≠ T
☐
~(T = TBool ∨ ∃ n, T = TBase n) →
∃ S,
S <: T ∧ S ≠ T
Exercise: 2 stars (small_large_1)
- What is the smallest type T ("smallest" in the subtype
relation) that makes the following assertion true? (Assume we
have Unit among the base types and unit as a constant of this
type.)
empty |- (\p:T*Top. p.fst) ((\z:A.z), unit) : A→A
- What is the largest type T that makes the same assertion true?
Exercise: 2 stars (small_large_2)
- What is the smallest type T that makes the following
assertion true?
empty |- (\p:(A→A * B→B). p) ((\z:A.z), (\z:B.z)) : T
- What is the largest type T that makes the same assertion true?
Exercise: 2 stars, optional (small_large_3)
- What is the smallest type T that makes the following
assertion true?
a:A |- (\p:(A*T). (p.snd) (p.fst)) (a , \z:A.z) : A
- What is the largest type T that makes the same assertion true?
Exercise: 2 stars (small_large_4)
- What is the smallest type T that makes the following
assertion true?
∃ S,
empty |- (\p:(A*T). (p.snd) (p.fst)) : S - What is the largest type T that makes the same assertion true?
Exercise: 2 stars (smallest_1)
What is the smallest type T that makes the following assertion true?
∃ S, ∃ t,
empty |- (\x:T. x x) t : S
☐
empty |- (\x:T. x x) t : S
Exercise: 2 stars (smallest_2)
What is the smallest type T that makes the following assertion true?
empty |- (\x:Top. x) ((\z:A.z) , (\z:B.z)) : T
☐
Exercise: 3 stars, optional (count_supertypes)
How many supertypes does the record type {x:A, y:C→C} have? That is, how many different types T are there such that {x:A, y:C→C} <: T? (We consider two types to be different if they are written differently, even if each is a subtype of the other. For example, {x:A,y:B} and {y:B,x:A} are different.)Exercise: 2 stars (pair_permutation)
The subtyping rule for product typesS_{1} <: T_{1} S_{2} <: T_{2} | (S_Prod) |
S_{1}*S_{2} <: T_{1}*T_{2} |
T_{1}*T_{2} <: T_{2}*T_{1} |
Formal Definitions
Syntax
Inductive ty : Type :=
| TTop : ty
| TBool : ty
| TBase : string → ty
| TArrow : ty → ty → ty
| TUnit : ty
.
Inductive tm : Type :=
| tvar : string → tm
| tapp : tm → tm → tm
| tabs : string → ty → tm → tm
| ttrue : tm
| tfalse : tm
| tif : tm → tm → tm → tm
| tunit : tm
.
| TTop : ty
| TBool : ty
| TBase : string → ty
| TArrow : ty → ty → ty
| TUnit : ty
.
Inductive tm : Type :=
| tvar : string → tm
| tapp : tm → tm → tm
| tabs : string → ty → tm → tm
| ttrue : tm
| tfalse : tm
| tif : tm → tm → tm → tm
| tunit : tm
.
Fixpoint subst (x:string) (s:tm) (t:tm) : tm :=
match t with
| tvar y ⇒
if beq_string x y then s else t
| tabs y T t_{1} ⇒
tabs y T (if beq_string x y then t_{1} else (subst x s t_{1}))
| tapp t_{1} t_{2} ⇒
tapp (subst x s t_{1}) (subst x s t_{2})
| ttrue ⇒
ttrue
| tfalse ⇒
tfalse
| tif t_{1} t_{2} t_{3} ⇒
tif (subst x s t_{1}) (subst x s t_{2}) (subst x s t_{3})
| tunit ⇒
tunit
end.
Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
match t with
| tvar y ⇒
if beq_string x y then s else t
| tabs y T t_{1} ⇒
tabs y T (if beq_string x y then t_{1} else (subst x s t_{1}))
| tapp t_{1} t_{2} ⇒
tapp (subst x s t_{1}) (subst x s t_{2})
| ttrue ⇒
ttrue
| tfalse ⇒
tfalse
| tif t_{1} t_{2} t_{3} ⇒
tif (subst x s t_{1}) (subst x s t_{2}) (subst x s t_{3})
| tunit ⇒
tunit
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_true :
value ttrue
| v_false :
value tfalse
| v_unit :
value tunit
.
Hint Constructors value.
Reserved Notation "t_{1} '==>' t_{2}" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀ x T t_{12} v_{2},
value v_{2} →
(tapp (tabs x T t_{12}) v_{2}) ==> [x:=v_{2}]t_{12}
| ST_App1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
(tapp t_{1} t_{2}) ==> (tapp t_{1}' t_{2})
| ST_App2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} →
t_{2} ==> t_{2}' →
(tapp v_{1} t_{2}) ==> (tapp v_{1} t_{2}')
| ST_IfTrue : ∀ t_{1} t_{2},
(tif ttrue t_{1} t_{2}) ==> t_{1}
| ST_IfFalse : ∀ t_{1} t_{2},
(tif tfalse t_{1} t_{2}) ==> t_{2}
| ST_If : ∀ t_{1} t_{1}' t_{2} t_{3},
t_{1} ==> t_{1}' →
(tif t_{1} t_{2} t_{3}) ==> (tif t_{1}' t_{2} t_{3})
where "t_{1} '==>' t_{2}" := (step t_{1} t_{2}).
Hint Constructors step.
| v_abs : ∀ x T t,
value (tabs x T t)
| v_true :
value ttrue
| v_false :
value tfalse
| v_unit :
value tunit
.
Hint Constructors value.
Reserved Notation "t_{1} '==>' t_{2}" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀ x T t_{12} v_{2},
value v_{2} →
(tapp (tabs x T t_{12}) v_{2}) ==> [x:=v_{2}]t_{12}
| ST_App1 : ∀ t_{1} t_{1}' t_{2},
t_{1} ==> t_{1}' →
(tapp t_{1} t_{2}) ==> (tapp t_{1}' t_{2})
| ST_App2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} →
t_{2} ==> t_{2}' →
(tapp v_{1} t_{2}) ==> (tapp v_{1} t_{2}')
| ST_IfTrue : ∀ t_{1} t_{2},
(tif ttrue t_{1} t_{2}) ==> t_{1}
| ST_IfFalse : ∀ t_{1} t_{2},
(tif tfalse t_{1} t_{2}) ==> t_{2}
| ST_If : ∀ t_{1} t_{1}' t_{2} t_{3},
t_{1} ==> t_{1}' →
(tif t_{1} t_{2} t_{3}) ==> (tif t_{1}' t_{2} t_{3})
where "t_{1} '==>' t_{2}" := (step t_{1} t_{2}).
Hint Constructors step.
Subtyping
Reserved Notation "T '<:' U" (at level 40).
Inductive subtype : ty → ty → Prop :=
| S_Refl : ∀ T,
T <: T
| S_Trans : ∀ S U T,
S <: U →
U <: T →
S <: T
| S_Top : ∀ S,
S <: TTop
| S_Arrow : ∀ S_{1} S_{2} T_{1} T_{2},
T_{1} <: S_{1} →
S_{2} <: T_{2} →
(TArrow S_{1} S_{2}) <: (TArrow T_{1} T_{2})
where "T '<:' U" := (subtype T U).
Inductive subtype : ty → ty → Prop :=
| S_Refl : ∀ T,
T <: T
| S_Trans : ∀ S U T,
S <: U →
U <: T →
S <: T
| S_Top : ∀ S,
S <: TTop
| S_Arrow : ∀ S_{1} S_{2} T_{1} T_{2},
T_{1} <: S_{1} →
S_{2} <: T_{2} →
(TArrow S_{1} S_{2}) <: (TArrow T_{1} T_{2})
where "T '<:' U" := (subtype T U).
Note that we don't need any special rules for base types (TBool
and TBase): they are automatically subtypes of themselves (by
S_Refl) and Top (by S_Top), and that's all we want.
Hint Constructors subtype.
Module Examples.
Open Scope string_scope.
Notation x := "x".
Notation y := "y".
Notation z := "z".
Notation A := (TBase "A").
Notation B := (TBase "B").
Notation C := (TBase "C").
Notation String := (TBase "String").
Notation Float := (TBase "Float").
Notation Integer := (TBase "Integer").
Example subtyping_example_0 :
(TArrow C TBool) <: (TArrow C TTop).
(* C->Bool <: C->Top *)
Proof. auto. Qed.
Module Examples.
Open Scope string_scope.
Notation x := "x".
Notation y := "y".
Notation z := "z".
Notation A := (TBase "A").
Notation B := (TBase "B").
Notation C := (TBase "C").
Notation String := (TBase "String").
Notation Float := (TBase "Float").
Notation Integer := (TBase "Integer").
Example subtyping_example_0 :
(TArrow C TBool) <: (TArrow C TTop).
(* C->Bool <: C->Top *)
Proof. auto. Qed.
Exercise: 2 stars, optional (subtyping_judgements)
(Wait to do this exercise after you have added product types to the language — see exercise products — at least up to this point in the file).
Person := { name : String }
Student := { name : String ;
gpa : Float }
Employee := { name : String ;
ssn : Integer }
Student := { name : String ;
gpa : Float }
Employee := { name : String ;
ssn : Integer }
Definition Person : ty
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition Student : ty
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition Employee : ty
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition Student : ty
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Definition Employee : ty
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Now use the definition of the subtype relation to prove the following:
Example sub_student_person :
Student <: Person.
Proof.
(* FILL IN HERE *) Admitted.
Example sub_employee_person :
Employee <: Person.
Proof.
(* FILL IN HERE *) Admitted.
☐
Student <: Person.
Proof.
(* FILL IN HERE *) Admitted.
Example sub_employee_person :
Employee <: Person.
Proof.
(* FILL IN HERE *) Admitted.
Exercise: 1 star, optional (subtyping_example_1)
Example subtyping_example_1 :
(TArrow TTop Student) <: (TArrow (TArrow C C) Person).
(* Top->Student <: (C->C)->Person *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
(TArrow TTop Student) <: (TArrow (TArrow C C) Person).
(* Top->Student <: (C->C)->Person *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Example subtyping_example_2 :
(TArrow TTop Person) <: (TArrow Person TTop).
(* Top->Person <: Person->Top *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
(TArrow TTop Person) <: (TArrow Person TTop).
(* Top->Person <: Person->Top *)
Proof with eauto.
(* FILL IN HERE *) Admitted.
Definition context := partial_map ty.
Reserved Notation "Gamma '|-' t '∈' T" (at level 40).
Inductive has_type : context → tm → ty → Prop :=
(* Same as before *)
| T_Var : ∀ Gamma x T,
Gamma x = Some T →
Gamma |- tvar x ∈ T
| T_Abs : ∀ Gamma x T_{11} T_{12} t_{12},
Gamma & {{x-->T_{11}}} |- t_{12} ∈ T_{12} →
Gamma |- tabs x T_{11} t_{12} ∈ TArrow T_{11} T_{12}
| T_App : ∀ T_{1} T_{2} Gamma t_{1} t_{2},
Gamma |- t_{1} ∈ TArrow T_{1} T_{2} →
Gamma |- t_{2} ∈ T_{1} →
Gamma |- tapp t_{1} t_{2} ∈ T_{2}
| T_True : ∀ Gamma,
Gamma |- ttrue ∈ TBool
| T_False : ∀ Gamma,
Gamma |- tfalse ∈ TBool
| T_If : ∀ t_{1} t_{2} t_{3} T Gamma,
Gamma |- t_{1} ∈ TBool →
Gamma |- t_{2} ∈ T →
Gamma |- t_{3} ∈ T →
Gamma |- tif t_{1} t_{2} t_{3} ∈ T
| T_Unit : ∀ Gamma,
Gamma |- tunit ∈ TUnit
(* New rule of subsumption *)
| T_Sub : ∀ Gamma t S T,
Gamma |- t ∈ S →
S <: T →
Gamma |- t ∈ T
where "Gamma '|-' t '∈' T" := (has_type Gamma t T).
Hint Constructors has_type.
Reserved Notation "Gamma '|-' t '∈' T" (at level 40).
Inductive has_type : context → tm → ty → Prop :=
(* Same as before *)
| T_Var : ∀ Gamma x T,
Gamma x = Some T →
Gamma |- tvar x ∈ T
| T_Abs : ∀ Gamma x T_{11} T_{12} t_{12},
Gamma & {{x-->T_{11}}} |- t_{12} ∈ T_{12} →
Gamma |- tabs x T_{11} t_{12} ∈ TArrow T_{11} T_{12}
| T_App : ∀ T_{1} T_{2} Gamma t_{1} t_{2},
Gamma |- t_{1} ∈ TArrow T_{1} T_{2} →
Gamma |- t_{2} ∈ T_{1} →
Gamma |- tapp t_{1} t_{2} ∈ T_{2}
| T_True : ∀ Gamma,
Gamma |- ttrue ∈ TBool
| T_False : ∀ Gamma,
Gamma |- tfalse ∈ TBool
| T_If : ∀ t_{1} t_{2} t_{3} T Gamma,
Gamma |- t_{1} ∈ TBool →
Gamma |- t_{2} ∈ T →
Gamma |- t_{3} ∈ T →
Gamma |- tif t_{1} t_{2} t_{3} ∈ T
| T_Unit : ∀ Gamma,
Gamma |- tunit ∈ TUnit
(* New rule of subsumption *)
| T_Sub : ∀ Gamma t S T,
Gamma |- t ∈ S →
S <: T →
Gamma |- t ∈ T
where "Gamma '|-' t '∈' T" := (has_type Gamma t T).
Hint Constructors has_type.
The following hints help auto and eauto construct typing
derivations. (See chapter UseAuto for more on hints.)
Hint Extern 2 (has_type _ (tapp _ _) _) ⇒
eapply T_App; auto.
Hint Extern 2 (_ = _) ⇒ compute; reflexivity.
Module Examples2.
Import Examples.
eapply T_App; auto.
Hint Extern 2 (_ = _) ⇒ compute; reflexivity.
Module Examples2.
Import Examples.
Do the following exercises after you have added product types to
the language. For each informal typing judgement, write it as a
formal statement in Coq and prove it.
Exercise: 1 star, optional (typing_example_0)
(* empty |- ((\z:A.z), (\z:B.z))
: (A->A * B->B) *)
(* FILL IN HERE *)
☐
: (A->A * B->B) *)
(* FILL IN HERE *)
(* empty |- (\x:(Top * B->B). x.snd) ((\z:A.z), (\z:B.z))
: B->B *)
(* FILL IN HERE *)
☐
: B->B *)
(* FILL IN HERE *)
(* empty |- (\z:(C->C)->(Top * B->B). (z (\x:C.x)).snd)
(\z:C->C. ((\z:A.z), (\z:B.z)))
: B->B *)
(* FILL IN HERE *)
☐
(\z:C->C. ((\z:A.z), (\z:B.z)))
: B->B *)
(* FILL IN HERE *)
Properties
Inversion Lemmas for Subtyping
- Bool is the only subtype of Bool, and
- every subtype of an arrow type is itself an arrow type.
Exercise: 2 stars, optional (sub_inversion_Bool)
Lemma sub_inversion_arrow : ∀ U V_{1} V_{2},
U <: TArrow V_{1} V_{2} →
∃ U_{1}, ∃ U_{2},
U = TArrow U_{1} U_{2} ∧ V_{1} <: U_{1} ∧ U_{2} <: V_{2}.
☐
U <: TArrow V_{1} V_{2} →
∃ U_{1}, ∃ U_{2},
U = TArrow U_{1} U_{2} ∧ V_{1} <: U_{1} ∧ U_{2} <: V_{2}.
Proof with eauto.
intros U V_{1} V_{2} Hs.
remember (TArrow V_{1} V_{2}) as V.
generalize dependent V_{2}. generalize dependent V_{1}.
(* FILL IN HERE *) Admitted.
intros U V_{1} V_{2} Hs.
remember (TArrow V_{1} V_{2}) as V.
generalize dependent V_{2}. generalize dependent V_{1}.
(* FILL IN HERE *) Admitted.
Canonical Forms
Exercise: 3 stars, optional (canonical_forms_of_arrow_types)
Lemma canonical_forms_of_arrow_types : ∀ Gamma s T_{1} T_{2},
Gamma |- s ∈ TArrow T_{1} T_{2} →
value s →
∃ x, ∃ S_{1}, ∃ s_{2},
s = tabs x S_{1} s_{2}.
☐
Gamma |- s ∈ TArrow T_{1} T_{2} →
value s →
∃ x, ∃ S_{1}, ∃ s_{2},
s = tabs x S_{1} s_{2}.
Proof with eauto.
(* FILL IN HERE *) Admitted.
(* FILL IN HERE *) Admitted.
Lemma canonical_forms_of_Bool : ∀ Gamma s,
Gamma |- s ∈ TBool →
value s →
s = ttrue ∨ s = tfalse.
Gamma |- s ∈ TBool →
value s →
s = ttrue ∨ s = tfalse.
Proof with eauto.
intros Gamma s Hty Hv.
remember TBool as T.
induction Hty; try solve_by_invert...
- (* T_Sub *)
subst. apply sub_inversion_Bool in H. subst...
Qed.
intros Gamma s Hty Hv.
remember TBool as T.
induction Hty; try solve_by_invert...
- (* T_Sub *)
subst. apply sub_inversion_Bool in H. subst...
Qed.
Progress
- If the last step in the typing derivation uses rule T_App,
then there are terms t_{1} t_{2} and types T_{1} and T_{2} such that
t = t_{1} t_{2}, T = T_{2}, empty |- t_{1} : T_{1} → T_{2}, and empty |-
t_{2} : T_{1}. Moreover, by the induction hypothesis, either t_{1} is
a value or it steps, and either t_{2} is a value or it steps.
There are three possibilities to consider:
- Suppose t_{1} ==> t_{1}' for some term t_{1}'. Then t_{1} t_{2} ==> t_{1}' t_{2}
by ST_App1.
- Suppose t_{1} is a value and t_{2} ==> t_{2}' for some term t_{2}'.
Then t_{1} t_{2} ==> t_{1} t_{2}' by rule ST_App2 because t_{1} is a
value.
- Finally, suppose t_{1} and t_{2} are both values. By the
canonical forms lemma for arrow types, we know that t_{1} has the
form \x:S_{1}.s2 for some x, S_{1}, and s_{2}. But then
(\x:S_{1}.s2) t_{2} ==> [x:=t_{2}]s_{2} by ST_AppAbs, since t_{2} is a
value.
- Suppose t_{1} ==> t_{1}' for some term t_{1}'. Then t_{1} t_{2} ==> t_{1}' t_{2}
by ST_App1.
- If the final step of the derivation uses rule T_If, then there
are terms t_{1}, t_{2}, and t_{3} such that t = if t_{1} then t_{2} else
t_{3}, with empty |- t_{1} : Bool and with empty |- t_{2} : T and
empty |- t_{3} : T. Moreover, by the induction hypothesis,
either t_{1} is a value or it steps.
- If t_{1} is a value, then by the canonical forms lemma for
booleans, either t_{1} = true or t_{1} = false. In either
case, t can step, using rule ST_IfTrue or ST_IfFalse.
- If t_{1} can step, then so can t, by rule ST_If.
- If t_{1} is a value, then by the canonical forms lemma for
booleans, either t_{1} = true or t_{1} = false. In either
case, t can step, using rule ST_IfTrue or ST_IfFalse.
- 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.
Theorem progress : ∀ t T,
empty |- t ∈ T →
value t ∨ ∃ t', t ==> t'.
empty |- t ∈ T →
value t ∨ ∃ t', t ==> t'.
Proof with eauto.
intros t T Ht.
remember empty as Gamma.
revert HeqGamma.
induction Ht;
intros HeqGamma; subst...
- (* T_Var *)
inversion H.
- (* T_App *)
right.
destruct IHHt1; subst...
+ (* t_{1} is a value *)
destruct IHHt2; subst...
* (* t_{2} is a value *)
destruct (canonical_forms_of_arrow_types empty t_{1} T_{1} T_{2})
as [x [S_{1} [t_{12} Heqt1]]]...
subst. ∃ ([x:=t_{2}]t_{12})...
* (* t_{2} steps *)
inversion H_{0} as [t_{2}' Hstp]. ∃ (tapp t_{1} t_{2}')...
+ (* t_{1} steps *)
inversion H as [t_{1}' Hstp]. ∃ (tapp t_{1}' t_{2})...
- (* T_If *)
right.
destruct IHHt1.
+ (* t_{1} is a value *) eauto.
+ assert (t_{1} = ttrue ∨ t_{1} = tfalse)
by (eapply canonical_forms_of_Bool; eauto).
inversion H_{0}; subst...
+ inversion H. rename x into t_{1}'. eauto.
Qed.
intros t T Ht.
remember empty as Gamma.
revert HeqGamma.
induction Ht;
intros HeqGamma; subst...
- (* T_Var *)
inversion H.
- (* T_App *)
right.
destruct IHHt1; subst...
+ (* t_{1} is a value *)
destruct IHHt2; subst...
* (* t_{2} is a value *)
destruct (canonical_forms_of_arrow_types empty t_{1} T_{1} T_{2})
as [x [S_{1} [t_{12} Heqt1]]]...
subst. ∃ ([x:=t_{2}]t_{12})...
* (* t_{2} steps *)
inversion H_{0} as [t_{2}' Hstp]. ∃ (tapp t_{1} t_{2}')...
+ (* t_{1} steps *)
inversion H as [t_{1}' Hstp]. ∃ (tapp t_{1}' t_{2})...
- (* T_If *)
right.
destruct IHHt1.
+ (* t_{1} is a value *) eauto.
+ assert (t_{1} = ttrue ∨ t_{1} = tfalse)
by (eapply canonical_forms_of_Bool; eauto).
inversion H_{0}; subst...
+ inversion H. rename x into t_{1}'. eauto.
Qed.
Inversion Lemmas for Typing
- If the last step of the derivation is a use of T_Abs then
there is a type T_{12} such that T = S_{1} → T_{12} and Gamma,
x:S_{1} |- t_{2} : T_{12}. Picking T_{12} for S_{2} gives us what we
need: S_{1} → T_{12} <: S_{1} → T_{12} follows from S_Refl.
- If the last step of the derivation is a use of T_Sub then there is a type S such that S <: T and Gamma |- \x:S_{1}.t2 : S. The IH for the typing subderivation tell us that there is some type S_{2} with S_{1} → S_{2} <: S and Gamma, x:S_{1} |- t_{2} : S_{2}. Picking type S_{2} gives us what we need, since S_{1} → S_{2} <: T then follows by S_Trans.
Lemma typing_inversion_abs : ∀ Gamma x S_{1} t_{2} T,
Gamma |- (tabs x S_{1} t_{2}) ∈ T →
∃ S_{2},
TArrow S_{1} S_{2} <: T
∧ Gamma & {{x-->S_{1}}} |- t_{2} ∈ S_{2}.
Gamma |- (tabs x S_{1} t_{2}) ∈ T →
∃ S_{2},
TArrow S_{1} S_{2} <: T
∧ Gamma & {{x-->S_{1}}} |- t_{2} ∈ S_{2}.
Proof with eauto.
intros Gamma x S_{1} t_{2} T H.
remember (tabs x S_{1} t_{2}) as t.
induction H;
inversion Heqt; subst; intros; try solve_by_invert.
- (* T_Abs *)
∃ T_{12}...
- (* T_Sub *)
destruct IHhas_type as [S_{2} [Hsub Hty]]...
Qed.
intros Gamma x S_{1} t_{2} T H.
remember (tabs x S_{1} t_{2}) as t.
induction H;
inversion Heqt; subst; intros; try solve_by_invert.
- (* T_Abs *)
∃ T_{12}...
- (* T_Sub *)
destruct IHhas_type as [S_{2} [Hsub Hty]]...
Qed.
Similarly...
Lemma typing_inversion_var : ∀ Gamma x T,
Gamma |- (tvar x) ∈ T →
∃ S,
Gamma x = Some S ∧ S <: T.
Lemma typing_inversion_app : ∀ Gamma t_{1} t_{2} T_{2},
Gamma |- (tapp t_{1} t_{2}) ∈ T_{2} →
∃ T_{1},
Gamma |- t_{1} ∈ (TArrow T_{1} T_{2}) ∧
Gamma |- t_{2} ∈ T_{1}.
Lemma typing_inversion_true : ∀ Gamma T,
Gamma |- ttrue ∈ T →
TBool <: T.
Lemma typing_inversion_false : ∀ Gamma T,
Gamma |- tfalse ∈ T →
TBool <: T.
Lemma typing_inversion_if : ∀ Gamma t_{1} t_{2} t_{3} T,
Gamma |- (tif t_{1} t_{2} t_{3}) ∈ T →
Gamma |- t_{1} ∈ TBool
∧ Gamma |- t_{2} ∈ T
∧ Gamma |- t_{3} ∈ T.
Lemma typing_inversion_unit : ∀ Gamma T,
Gamma |- tunit ∈ T →
TUnit <: T.
Gamma |- (tvar x) ∈ T →
∃ S,
Gamma x = Some S ∧ S <: T.
Proof with eauto.
intros Gamma x T Hty.
remember (tvar x) as t.
induction Hty; intros;
inversion Heqt; subst; try solve_by_invert.
- (* T_Var *)
∃ T...
- (* T_Sub *)
destruct IHHty as [U [Hctx HsubU]]... Qed.
intros Gamma x T Hty.
remember (tvar x) as t.
induction Hty; intros;
inversion Heqt; subst; try solve_by_invert.
- (* T_Var *)
∃ T...
- (* T_Sub *)
destruct IHHty as [U [Hctx HsubU]]... Qed.
Lemma typing_inversion_app : ∀ Gamma t_{1} t_{2} T_{2},
Gamma |- (tapp t_{1} t_{2}) ∈ T_{2} →
∃ T_{1},
Gamma |- t_{1} ∈ (TArrow T_{1} T_{2}) ∧
Gamma |- t_{2} ∈ T_{1}.
Proof with eauto.
intros Gamma t_{1} t_{2} T_{2} Hty.
remember (tapp t_{1} t_{2}) as t.
induction Hty; intros;
inversion Heqt; subst; try solve_by_invert.
- (* T_App *)
∃ T_{1}...
- (* T_Sub *)
destruct IHHty as [U_{1} [Hty1 Hty2]]...
Qed.
intros Gamma t_{1} t_{2} T_{2} Hty.
remember (tapp t_{1} t_{2}) as t.
induction Hty; intros;
inversion Heqt; subst; try solve_by_invert.
- (* T_App *)
∃ T_{1}...
- (* T_Sub *)
destruct IHHty as [U_{1} [Hty1 Hty2]]...
Qed.
Lemma typing_inversion_true : ∀ Gamma T,
Gamma |- ttrue ∈ T →
TBool <: T.
Proof with eauto.
intros Gamma T Htyp. remember ttrue as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
intros Gamma T Htyp. remember ttrue as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
Lemma typing_inversion_false : ∀ Gamma T,
Gamma |- tfalse ∈ T →
TBool <: T.
Proof with eauto.
intros Gamma T Htyp. remember tfalse as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
intros Gamma T Htyp. remember tfalse as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
Lemma typing_inversion_if : ∀ Gamma t_{1} t_{2} t_{3} T,
Gamma |- (tif t_{1} t_{2} t_{3}) ∈ T →
Gamma |- t_{1} ∈ TBool
∧ Gamma |- t_{2} ∈ T
∧ Gamma |- t_{3} ∈ T.
Proof with eauto.
intros Gamma t_{1} t_{2} t_{3} T Hty.
remember (tif t_{1} t_{2} t_{3}) as t.
induction Hty; intros;
inversion Heqt; subst; try solve_by_invert.
- (* T_If *)
auto.
- (* T_Sub *)
destruct (IHHty H_{0}) as [H_{1} [H_{2} H_{3}]]...
Qed.
intros Gamma t_{1} t_{2} t_{3} T Hty.
remember (tif t_{1} t_{2} t_{3}) as t.
induction Hty; intros;
inversion Heqt; subst; try solve_by_invert.
- (* T_If *)
auto.
- (* T_Sub *)
destruct (IHHty H_{0}) as [H_{1} [H_{2} H_{3}]]...
Qed.
Lemma typing_inversion_unit : ∀ Gamma T,
Gamma |- tunit ∈ T →
TUnit <: T.
Proof with eauto.
intros Gamma T Htyp. remember tunit as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
intros Gamma T Htyp. remember tunit as tu.
induction Htyp;
inversion Heqtu; subst; intros...
Qed.
The inversion lemmas for typing and for subtyping between arrow
types can be packaged up as a useful "combination lemma" telling
us exactly what we'll actually require below.
Lemma abs_arrow : ∀ x S_{1} s_{2} T_{1} T_{2},
empty |- (tabs x S_{1} s_{2}) ∈ (TArrow T_{1} T_{2}) →
T_{1} <: S_{1}
∧ empty & {{x-->S_{1}}} |- s_{2} ∈ T_{2}.
empty |- (tabs x S_{1} s_{2}) ∈ (TArrow T_{1} T_{2}) →
T_{1} <: S_{1}
∧ empty & {{x-->S_{1}}} |- s_{2} ∈ T_{2}.
Proof with eauto.
intros x S_{1} s_{2} T_{1} T_{2} Hty.
apply typing_inversion_abs in Hty.
inversion Hty as [S_{2} [Hsub Hty1]].
apply sub_inversion_arrow in Hsub.
inversion Hsub as [U_{1} [U_{2} [Heq [Hsub1 Hsub2]]]].
inversion Heq; subst... Qed.
intros x S_{1} s_{2} T_{1} T_{2} Hty.
apply typing_inversion_abs in Hty.
inversion Hty as [S_{2} [Hsub Hty1]].
apply sub_inversion_arrow in Hsub.
inversion Hsub as [U_{1} [U_{2} [Heq [Hsub1 Hsub2]]]].
inversion Heq; subst... Qed.
Inductive appears_free_in : string → tm → Prop :=
| afi_var : ∀ x,
appears_free_in x (tvar x)
| afi_app1 : ∀ x t_{1} t_{2},
appears_free_in x t_{1} → appears_free_in x (tapp t_{1} t_{2})
| afi_app2 : ∀ x t_{1} t_{2},
appears_free_in x t_{2} → appears_free_in x (tapp t_{1} t_{2})
| afi_abs : ∀ x y T_{11} t_{12},
y ≠ x →
appears_free_in x t_{12} →
appears_free_in x (tabs y T_{11} t_{12})
| afi_if_{1} : ∀ x t_{1} t_{2} t_{3},
appears_free_in x t_{1} →
appears_free_in x (tif t_{1} t_{2} t_{3})
| afi_if_{2} : ∀ x t_{1} t_{2} t_{3},
appears_free_in x t_{2} →
appears_free_in x (tif t_{1} t_{2} t_{3})
| afi_if_{3} : ∀ x t_{1} t_{2} t_{3},
appears_free_in x t_{3} →
appears_free_in x (tif t_{1} t_{2} t_{3})
.
Hint Constructors appears_free_in.
Lemma context_invariance : ∀ Gamma Gamma' t S,
Gamma |- t ∈ S →
(∀ x, appears_free_in x t → Gamma x = Gamma' x) →
Gamma' |- t ∈ S.
Lemma free_in_context : ∀ x t T Gamma,
appears_free_in x t →
Gamma |- t ∈ T →
∃ T', Gamma x = Some T'.
| afi_var : ∀ x,
appears_free_in x (tvar x)
| afi_app1 : ∀ x t_{1} t_{2},
appears_free_in x t_{1} → appears_free_in x (tapp t_{1} t_{2})
| afi_app2 : ∀ x t_{1} t_{2},
appears_free_in x t_{2} → appears_free_in x (tapp t_{1} t_{2})
| afi_abs : ∀ x y T_{11} t_{12},
y ≠ x →
appears_free_in x t_{12} →
appears_free_in x (tabs y T_{11} t_{12})
| afi_if_{1} : ∀ x t_{1} t_{2} t_{3},
appears_free_in x t_{1} →
appears_free_in x (tif t_{1} t_{2} t_{3})
| afi_if_{2} : ∀ x t_{1} t_{2} t_{3},
appears_free_in x t_{2} →
appears_free_in x (tif t_{1} t_{2} t_{3})
| afi_if_{3} : ∀ x t_{1} t_{2} t_{3},
appears_free_in x t_{3} →
appears_free_in x (tif t_{1} t_{2} t_{3})
.
Hint Constructors appears_free_in.
Lemma context_invariance : ∀ Gamma Gamma' t S,
Gamma |- t ∈ S →
(∀ x, appears_free_in x t → Gamma x = Gamma' x) →
Gamma' |- t ∈ S.
Proof with eauto.
intros. generalize dependent Gamma'.
induction H;
intros Gamma' Heqv...
- (* T_Var *)
apply T_Var... rewrite <- Heqv...
- (* T_Abs *)
apply T_Abs... apply IHhas_type. intros x_{0} Hafi.
unfold update, t_update. destruct (beq_stringP x x_{0})...
- (* T_If *)
apply T_If...
Qed.
intros. generalize dependent Gamma'.
induction H;
intros Gamma' Heqv...
- (* T_Var *)
apply T_Var... rewrite <- Heqv...
- (* T_Abs *)
apply T_Abs... apply IHhas_type. intros x_{0} Hafi.
unfold update, t_update. destruct (beq_stringP x x_{0})...
- (* T_If *)
apply T_If...
Qed.
Lemma free_in_context : ∀ x t T Gamma,
appears_free_in x t →
Gamma |- t ∈ T →
∃ T', Gamma x = Some T'.
Proof with eauto.
intros x t T Gamma Hafi Htyp.
induction Htyp;
subst; inversion Hafi; subst...
- (* T_Abs *)
destruct (IHHtyp H_{4}) as [T Hctx]. ∃ T.
unfold update, t_update in Hctx.
rewrite <- beq_string_false_iff in H_{2}.
rewrite H_{2} in Hctx... Qed.
intros x t T Gamma Hafi Htyp.
induction Htyp;
subst; inversion Hafi; subst...
- (* T_Abs *)
destruct (IHHtyp H_{4}) as [T Hctx]. ∃ T.
unfold update, t_update in Hctx.
rewrite <- beq_string_false_iff in H_{2}.
rewrite H_{2} in Hctx... Qed.
Substitution
Lemma substitution_preserves_typing : ∀ Gamma x U v t S,
Gamma & {{x-->U}} |- t ∈ S →
empty |- v ∈ U →
Gamma |- [x:=v]t ∈ S.
Gamma & {{x-->U}} |- t ∈ S →
empty |- v ∈ U →
Gamma |- [x:=v]t ∈ S.
Proof with eauto.
intros Gamma x U v t S Htypt Htypv.
generalize dependent S. generalize dependent Gamma.
induction t; intros; simpl.
- (* tvar *)
rename s into y.
destruct (typing_inversion_var _ _ _ Htypt)
as [T [Hctx Hsub]].
unfold update, t_update in Hctx.
destruct (beq_stringP x y) as [Hxy|Hxy]; eauto;
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'.
- (* tapp *)
destruct (typing_inversion_app _ _ _ _ Htypt)
as [T_{1} [Htypt1 Htypt2]].
eapply T_App...
- (* tabs *)
rename s into y. rename t into T_{1}.
destruct (typing_inversion_abs _ _ _ _ _ Htypt)
as [T_{2} [Hsub Htypt2]].
apply T_Sub with (TArrow T_{1} T_{2})... apply T_Abs...
destruct (beq_stringP x y) as [Hxy|Hxy].
+ (* x=y *)
eapply context_invariance...
subst.
intros x Hafi. unfold update, t_update.
destruct (beq_string y x)...
+ (* x<>y *)
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (beq_stringP y z)...
subst.
rewrite <- beq_string_false_iff in Hxy. rewrite Hxy...
- (* ttrue *)
assert (TBool <: S)
by apply (typing_inversion_true _ _ Htypt)...
- (* tfalse *)
assert (TBool <: S)
by apply (typing_inversion_false _ _ Htypt)...
- (* tif *)
assert (Gamma & {{x-->U}} |- t_{1} ∈ TBool
∧ Gamma & {{x-->U}} |- t_{2} ∈ S
∧ Gamma & {{x-->U}} |- t_{3} ∈ S)
by apply (typing_inversion_if _ _ _ _ _ Htypt).
inversion H as [H_{1} [H_{2} H_{3}]].
apply IHt1 in H_{1}. apply IHt2 in H_{2}. apply IHt3 in H_{3}.
auto.
- (* tunit *)
assert (TUnit <: S)
by apply (typing_inversion_unit _ _ Htypt)...
Qed.
intros Gamma x U v t S Htypt Htypv.
generalize dependent S. generalize dependent Gamma.
induction t; intros; simpl.
- (* tvar *)
rename s into y.
destruct (typing_inversion_var _ _ _ Htypt)
as [T [Hctx Hsub]].
unfold update, t_update in Hctx.
destruct (beq_stringP x y) as [Hxy|Hxy]; eauto;
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'.
- (* tapp *)
destruct (typing_inversion_app _ _ _ _ Htypt)
as [T_{1} [Htypt1 Htypt2]].
eapply T_App...
- (* tabs *)
rename s into y. rename t into T_{1}.
destruct (typing_inversion_abs _ _ _ _ _ Htypt)
as [T_{2} [Hsub Htypt2]].
apply T_Sub with (TArrow T_{1} T_{2})... apply T_Abs...
destruct (beq_stringP x y) as [Hxy|Hxy].
+ (* x=y *)
eapply context_invariance...
subst.
intros x Hafi. unfold update, t_update.
destruct (beq_string y x)...
+ (* x<>y *)
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (beq_stringP y z)...
subst.
rewrite <- beq_string_false_iff in Hxy. rewrite Hxy...
- (* ttrue *)
assert (TBool <: S)
by apply (typing_inversion_true _ _ Htypt)...
- (* tfalse *)
assert (TBool <: S)
by apply (typing_inversion_false _ _ Htypt)...
- (* tif *)
assert (Gamma & {{x-->U}} |- t_{1} ∈ TBool
∧ Gamma & {{x-->U}} |- t_{2} ∈ S
∧ Gamma & {{x-->U}} |- t_{3} ∈ S)
by apply (typing_inversion_if _ _ _ _ _ Htypt).
inversion H as [H_{1} [H_{2} H_{3}]].
apply IHt1 in H_{1}. apply IHt2 in H_{2}. apply IHt3 in H_{3}.
auto.
- (* tunit *)
assert (TUnit <: S)
by apply (typing_inversion_unit _ _ Htypt)...
Qed.
Preservation
- If the final step of the derivation is by T_App, then there
are terms t_{1} and t_{2} and types T_{1} and T_{2} such that
t = t_{1} t_{2}, T = T_{2}, empty |- t_{1} : T_{1} → T_{2}, and
empty |- t_{2} : T_{1}.
- If the final step of the derivation uses rule T_If, then
there are terms t_{1}, t_{2}, and t_{3} such that t = if t_{1} then
t_{2} else t_{3}, with empty |- t_{1} : Bool and with empty |- t_{2} :
T and empty |- t_{3} : T. Moreover, by the induction
hypothesis, if t_{1} steps to t_{1}' then empty |- t_{1}' : Bool.
There are three cases to consider, depending on which rule was
used to show t ==> t'.
- If t ==> t' by rule ST_If, then t' = if t_{1}' then t_{2}
else t_{3} with t_{1} ==> t_{1}'. By the induction hypothesis,
empty |- t_{1}' : Bool, and so empty |- t' : T by T_If.
- If t ==> t' by rule ST_IfTrue or ST_IfFalse, then
either t' = t_{2} or t' = t_{3}, and empty |- t' : T
follows by assumption.
- If t ==> t' by rule ST_If, then t' = if t_{1}' then t_{2}
else t_{3} with t_{1} ==> t_{1}'. By the induction hypothesis,
empty |- t_{1}' : Bool, and so empty |- t' : T by T_If.
- If the final step of the derivation uses rule T_If, then
there are terms t_{1}, t_{2}, and t_{3} such that t = if t_{1} then
t_{2} else t_{3}, with empty |- t_{1} : Bool and with empty |- t_{2} :
T and empty |- t_{3} : T. Moreover, by the induction
hypothesis, if t_{1} steps to t_{1}' then empty |- t_{1}' : Bool.
There are three cases to consider, depending on which rule was
used to show t ==> 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. ☐
Theorem preservation : ∀ t t' T,
empty |- t ∈ T →
t ==> t' →
empty |- t' ∈ T.
empty |- t ∈ T →
t ==> t' →
empty |- t' ∈ T.
Proof with eauto.
intros t t' T HT.
remember empty as Gamma. 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 _ _ _ _ _ HT_{1}) as [HA_{1} HA_{2}].
apply substitution_preserves_typing with T...
Qed.
intros t t' T HT.
remember empty as Gamma. 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 _ _ _ _ _ HT_{1}) as [HA_{1} HA_{2}].
apply substitution_preserves_typing with T...
Qed.
Records, via Products and Top
{a:Nat, b:Nat} ----> {Nat,Nat} i.e., (Nat,(Nat,Top)) {c:Nat, a:Nat} ----> {Nat,Top,Nat} i.e., (Nat,(Top,(Nat,Top)))The encoding of record values doesn't change at all. It is easy (and instructive) to check that the subtyping rules above are validated by the encoding.
Exercises
Exercise: 2 stars (variations)
Each part of this problem suggests a different way of changing the definition of the STLC with Unit 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:
Gamma |- t : S_{1}->S_{2} S_{1} <: T_{1} T_{1} <: S_{1} S_{2} <: T_{2} (T_Funny1) Gamma |- t : T_{1}->T_{2} - Suppose we add the following reduction rule:
(ST_Funny21) unit ==> (\x:Top. x) - Suppose we add the following subtyping rule:
(S_Funny3) Unit <: Top->Top - Suppose we add the following subtyping rule:
(S_Funny4) Top->Top <: Unit - Suppose we add the following reduction rule:
(ST_Funny5) (unit t) ==> (t unit) - Suppose we add the same reduction rule and a new typing rule:
(ST_Funny5) (unit t) ==> (t unit) (T_Funny6) empty |- unit : Top->Top - Suppose we change the arrow subtyping rule to:
S_{1} <: T_{1} S_{2} <: T_{2} (S_Arrow') S_{1}->S_{2} <: T_{1}->T_{2}
Exercise: Adding Products
Exercise: 4 stars (products)
Adding pairs, projections, and product types to the system we have defined is a relatively straightforward matter. Carry out this extension:- Below, we've added constructors for pairs, first and second
projections, and product types to the definitions of ty and
tm.
- Copy the definitions of the substitution function and value
relation from above and extend them as in chapter
MoreSTLC to include products.
- Similarly, copy and extend the operational semantics with the
same reduction rules as in chapter MoreSTLC.
- (Copy and) extend the subtyping relation with this rule:
S_{1} <: T_{1} S_{2} <: T_{2} (Sub_Prod) S_{1} * S_{2} <: T_{1} * T_{2} - Extend the typing relation with the same rules for pairs and
projections as in chapter MoreSTLC.
- Extend the proofs of progress, preservation, and all their supporting lemmas to deal with the new constructs. (You'll also need to add a couple of completely new lemmas.)
Module ProductExtension.
Inductive ty : Type :=
| TTop : ty
| TBool : ty
| TBase : string → ty
| TArrow : ty → ty → ty
| TUnit : ty
| TProd : ty → ty → ty.
Inductive tm : Type :=
| tvar : string → tm
| tapp : tm → tm → tm
| tabs : string → ty → tm → tm
| ttrue : tm
| tfalse : tm
| tif : tm → tm → tm → tm
| tunit : tm
| tpair : tm → tm → tm
| tfst : tm → tm
| tsnd : tm → tm.
Inductive ty : Type :=
| TTop : ty
| TBool : ty
| TBase : string → ty
| TArrow : ty → ty → ty
| TUnit : ty
| TProd : ty → ty → ty.
Inductive tm : Type :=
| tvar : string → tm
| tapp : tm → tm → tm
| tabs : string → ty → tm → tm
| ttrue : tm
| tfalse : tm
| tif : tm → tm → tm → tm
| tunit : tm
| tpair : tm → tm → tm
| tfst : tm → tm
| tsnd : tm → tm.
Copy and extend and/or fill in required definitions and lemmas
here.
Theorem progress : ∀ t T,
empty |- t ∈ T →
value t ∨ ∃ t', t ==> t'.
Proof.
(* FILL IN HERE *) Admitted.
Theorem preservation : ∀ t t' T,
empty |- t ∈ T →
t ==> t' →
empty |- t' ∈ T.
Proof.
(* FILL IN HERE *) Admitted.
End ProductExtension.
☐
empty |- t ∈ T →
value t ∨ ∃ t', t ==> t'.
Proof.
(* FILL IN HERE *) Admitted.
Theorem preservation : ∀ t t' T,
empty |- t ∈ T →
t ==> t' →
empty |- t' ∈ T.
Proof.
(* FILL IN HERE *) Admitted.
End ProductExtension.