SubSubtyping
Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Strings.String.
From PLF Require Import Maps.
From PLF Require Import Types.
From PLF Require Import Smallstep.
From PLF Require Import MoreStlc.
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.
- S is a subtype of T, written S <: T, if a value of type S can safely be used in any context where a value of type T is expected.
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_{1} ∈ T_{1} T_{1} <: T_{2} | (T_Sub) |
Gamma ⊢ t_{1} ∈ T_{2} |
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
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
Records
{name:String, age:Nat, gpa:Nat} <: {name:String, age:Nat}
{name:String, age:Nat} <: {name:String}
{name:String} <: {}
{x:Student} <: {x:Person}
{name:String,age:Nat} <: {age:Nat,name:String}
forall jk in j_{1}..jn, | |
exists 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} |
- 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).
- In early versions of Java, a subclass could 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).
Exercise: 2 stars, standard, especially useful (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
(* Do not modify the following line: *)
Definition manual_grade_for_arrow_sub_wrong : option (nat×string) := None.
☐
Top
(S_Top) | |
S <: Top |
Summary
- adding a base type Top,
- adding the rule of subsumption
to the typing relation, andGamma ⊢ t_{1} ∈ T_{1} T_{1} <: T_{2} (T_Sub) Gamma ⊢ t_{1} ∈ T_{2} - 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, standard, 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, standard (subtype_order)
The following types happen to form a linear order with respect to subtyping:- Top
- Top → Student
- Student → Person
- Student → Top
- Person → Student
(* Do not modify the following line: *)
Definition manual_grade_for_subtype_order : option (nat×string) := None.
☐
Exercise: 1 star, standard (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}
(* Do not modify the following line: *)
Definition manual_grade_for_subtype_instances_tf_2 : option (nat×string) := None.
☐
Exercise: 1 star, standard (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.
(* Do not modify the following line: *)
Definition manual_grade_for_subtype_concepts_tf : option (nat×string) := None.
☐
Exercise: 2 stars, standard (proper_subtypes)
Is the following statement true or false? Briefly explain your answer. (Here Base 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 = Bool ∨ ∃ n, T = Base n) →
∃ S,
S <: T ∧ S ≠ T
(* Do not modify the following line: *)
Definition manual_grade_for_proper_subtypes : option (nat×string) := None.
☐
Exercise: 2 stars, standard (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) \in A→A - What is the largest type T that makes the same assertion true?
(* Do not modify the following line: *)
Definition manual_grade_for_small_large_1 : option (nat×string) := None.
☐
Exercise: 2 stars, standard (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)) \in T - What is the largest type T that makes the same assertion true?
(* Do not modify the following line: *)
Definition manual_grade_for_small_large_2 : option (nat×string) := None.
☐
Exercise: 2 stars, standard, 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) \in A - What is the largest type T that makes the same assertion true?
Exercise: 2 stars, standard (small_large_4)
- What is the smallest type T (if one exists) that makes the
following assertion true?
∃ S,
empty ⊢ (\p:(A×T). (p.snd) (p.fst)) \in S - What is the largest type T that makes the same assertion true?
(* Do not modify the following line: *)
Definition manual_grade_for_small_large_4 : option (nat×string) := None.
☐
Exercise: 2 stars, standard (smallest_1)
What is the smallest type T (if one exists) that makes the following assertion true?∃ S t,
empty ⊢ (\x:T. x x) t \in S
(* Do not modify the following line: *)
Definition manual_grade_for_smallest_1 : option (nat×string) := None.
☐
Exercise: 2 stars, standard (smallest_2)
What is the smallest type T that makes the following assertion true?empty ⊢ (\x:Top. x) ((\z:A.z) , (\z:B.z)) \in T
(* Do not modify the following line: *)
Definition manual_grade_for_smallest_2 : option (nat×string) := None.
☐
Exercise: 3 stars, standard, 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, standard (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} |
(* Do not modify the following line: *)
Definition manual_grade_for_pair_permutation : option (nat×string) := None.
☐
Formal Definitions
Syntax
Inductive ty : Type :=
| Ty_Top : ty
| Ty_Bool : ty
| Ty_Base : string → ty
| Ty_Arrow : ty → ty → ty
| Ty_Unit : ty
.
Inductive tm : Type :=
| tm_var : string → tm
| tm_app : tm → tm → tm
| tm_abs : string → ty → tm → tm
| tm_true : tm
| tm_false : tm
| tm_if : tm → tm → tm → tm
| tm_unit : tm
.
Declare Custom Entry stlc.
Notation "<{ e }>" := e (e custom stlc at level 99).
Notation "( x )" := x (in custom stlc, x at level 99).
Notation "x" := x (in custom stlc at level 0, x constr at level 0).
Notation "S -> T" := (Ty_Arrow S T) (in custom stlc at level 50, right associativity).
Notation "x y" := (tm_app x y) (in custom stlc at level 1, left associativity).
Notation "\ x : t , y" :=
(tm_abs x t y) (in custom stlc at level 90, x at level 99,
t custom stlc at level 99,
y custom stlc at level 99,
left associativity).
Coercion tm_var : string >-> tm.
Notation "'Bool'" := Ty_Bool (in custom stlc at level 0).
Notation "'if' x 'then' y 'else' z" :=
(tm_if x y z) (in custom stlc at level 89,
x custom stlc at level 99,
y custom stlc at level 99,
z custom stlc at level 99,
left associativity).
Notation "'true'" := true (at level 1).
Notation "'true'" := tm_true (in custom stlc at level 0).
Notation "'false'" := false (at level 1).
Notation "'false'" := tm_false (in custom stlc at level 0).
Notation "'Unit'" :=
(Ty_Unit) (in custom stlc at level 0).
Notation "'unit'" := tm_unit (in custom stlc at level 0).
Notation "'Base' x" := (Ty_Base x) (in custom stlc at level 0).
Notation "'Top'" := (Ty_Top) (in custom stlc at level 0).
Reserved Notation "'[' x ':=' s ']' t" (in custom stlc at level 20, x constr).
Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
match t with
| tm_var y ⇒
if eqb_string x y then s else t
| <{\y:T, t_{1}}> ⇒
if eqb_string x y then t else <{\y:T, [x:=s] t_{1}}>
| <{t_{1} t_{2}}> ⇒
<{([x:=s] t_{1}) ([x:=s] t_{2})}>
| <{true}> ⇒
<{true}>
| <{false}> ⇒
<{false}>
| <{if t_{1} then t_{2} else t_{3}}> ⇒
<{if ([x:=s] t_{1}) then ([x:=s] t_{2}) else ([x:=s] t_{3})}>
| <{unit}> ⇒
<{unit}>
end
where "'[' x ':=' s ']' t" := (subst x s t) (in custom stlc).
Inductive value : tm → Prop :=
| v_abs : ∀ x T_{2} t_{1},
value <{\x:T_{2}, t_{1}}>
| v_true :
value <{true}>
| v_false :
value <{false}>
| v_unit :
value <{unit}>
.
Hint Constructors value : core.
Reserved Notation "t '-->' t'" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀ x T_{2} t_{1} v_{2},
value v_{2} →
<{(\x:T_{2}, t_{1}) v_{2}}> --> <{ [x:=v_{2}]t_{1} }>
| ST_App1 : ∀ t_{1} t_{1}' t_{2},
t_{1} --> t_{1}' →
<{t_{1} t_{2}}> --> <{t_{1}' t_{2}}>
| ST_App2 : ∀ v_{1} t_{2} t_{2}',
value v_{1} →
t_{2} --> t_{2}' →
<{v_{1} t_{2}}> --> <{v_{1} t_{2}'}>
| ST_IfTrue : ∀ t_{1} t_{2},
<{if true then t_{1} else t_{2}}> --> t_{1}
| ST_IfFalse : ∀ t_{1} t_{2},
<{if false then t_{1} else t_{2}}> --> t_{2}
| ST_If : ∀ t_{1} t_{1}' t_{2} t_{3},
t_{1} --> t_{1}' →
<{if t_{1} then t_{2} else t_{3}}> --> <{if t_{1}' then t_{2} else t_{3}}>
where "t '-->' t'" := (step t t').
Hint Constructors step : core.
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 <: <{Top}>
| S_Arrow : ∀ S_{1} S_{2} T_{1} T_{2},
T_{1} <: S_{1} →
S_{2} <: T_{2} →
<{S_{1}→S_{2}}> <: <{T_{1}→T_{2}}>
where "T '<:' U" := (subtype T U).
Note that we don't need any special rules for base types (Bool
and Base): they are automatically subtypes of themselves (by
S_Refl) and Top (by S_Top), and that's all we want.
Hint Constructors subtype : core.
Module Examples.
Open Scope string_scope.
Notation x := "x".
Notation y := "y".
Notation z := "z".
Notation A := <{Base "A"}>.
Notation B := <{Base "B"}>.
Notation C := <{Base "C"}>.
Notation String := <{Base "String"}>.
Notation Float := <{Base "Float"}>.
Notation Integer := <{Base "Integer"}>.
Example subtyping_example_0 :
<{C→Bool}> <: <{C→Top}>.
Proof. auto. Qed.
Exercise: 2 stars, standard, optional (subtyping_judgements)
(Leave this exercise Admitted until after you have finished adding 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 }
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.
☐
Exercise: 1 star, standard, optional (subtyping_example_1)
Example subtyping_example_1 :
<{Top→Student}> <: <{(C→C)→Person}>.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
<{Top→Student}> <: <{(C→C)→Person}>.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Example subtyping_example_2 :
<{Top→Person}> <: <{Person→Top}>.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
<{Top→Person}> <: <{Person→Top}>.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Definition context := partial_map ty.
Reserved Notation "Gamma '⊢' t '∈' T" (at level 40,
t custom stlc, T custom stlc at level 0).
Inductive has_type : context → tm → ty → Prop :=
(* Same as before: *)
(* pure STLC *)
| T_Var : ∀ Gamma x T_{1},
Gamma x = Some T_{1} →
Gamma ⊢ x \in T_{1}
| T_Abs : ∀ Gamma x T_{1} T_{2} t_{1},
(x ⊢> T_{2} ; Gamma) ⊢ t_{1} \in T_{1} →
Gamma ⊢ \x:T_{2}, t_{1} \in (T_{2} → T_{1})
| T_App : ∀ T_{1} T_{2} Gamma t_{1} t_{2},
Gamma ⊢ t_{1} \in (T_{2} → T_{1}) →
Gamma ⊢ t_{2} \in T_{2} →
Gamma ⊢ t_{1} t_{2} \in T_{1}
| T_True : ∀ Gamma,
Gamma ⊢ true \in Bool
| T_False : ∀ Gamma,
Gamma ⊢ false \in Bool
| T_If : ∀ t_{1} t_{2} t_{3} T_{1} Gamma,
Gamma ⊢ t_{1} \in Bool →
Gamma ⊢ t_{2} \in T_{1} →
Gamma ⊢ t_{3} \in T_{1} →
Gamma ⊢ if t_{1} then t_{2} else t_{3} \in T_{1}
| T_Unit : ∀ Gamma,
Gamma ⊢ unit \in Unit
(* New rule of subsumption: *)
| T_Sub : ∀ Gamma t_{1} T_{1} T_{2},
Gamma ⊢ t_{1} \in T_{1} →
T_{1} <: T_{2} →
Gamma ⊢ t_{1} \in T_{2}
where "Gamma '⊢' t '∈' T" := (has_type Gamma t T).
Hint Constructors has_type : core.
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, standard, 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, standard, optional (sub_inversion_Bool)
Lemma sub_inversion_arrow : ∀ U V_{1} V_{2},
U <: <{V_{1}→V_{2}}> →
∃ U_{1} U_{2},
U = <{U_{1}→U_{2}}> ∧ V_{1} <: U_{1} ∧ U_{2} <: V_{2}.
U <: <{V_{1}→V_{2}}> →
∃ U_{1} U_{2},
U = <{U_{1}→U_{2}}> ∧ V_{1} <: U_{1} ∧ U_{2} <: V_{2}.
☐
Canonical Forms
Exercise: 3 stars, standard, optional (canonical_forms_of_arrow_types)
Lemma canonical_forms_of_arrow_types : ∀ Gamma s T_{1} T_{2},
Gamma ⊢ s \in (T_{1}→T_{2}) →
value s →
∃ x S_{1} s_{2},
s = <{\x:S_{1},s_{2}}>.
Gamma ⊢ s \in (T_{1}→T_{2}) →
value s →
∃ x S_{1} s_{2},
s = <{\x:S_{1},s_{2}}>.
Proof with eauto.
(* FILL IN HERE *) Admitted.
(* FILL IN HERE *) Admitted.
☐
Similarly, the canonical forms of type Bool are the constants
tm_true and tm_false.
Lemma canonical_forms_of_Bool : ∀ Gamma s,
Gamma ⊢ s \in Bool →
value s →
s = tm_true ∨ s = tm_false.
Proof with eauto.
intros Gamma s Hty Hv.
remember <{Bool}> 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 <{Bool}> 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} \in T_{1} → T_{2}, and empty ⊢
t_{2} \in 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_Test, then there
are terms t_{1}, t_{2}, and t_{3} such that t = tm_if t_{1} then t_{2} else
t_{3}, with empty ⊢ t_{1} \in Bool and with empty ⊢ t_{2} \in T and
empty ⊢ t_{3} \in 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} = tm_true or t_{1} = tm_false. In either
case, t can step, using rule ST_TestTrue or ST_TestFalse.
- If t_{1} can step, then so can t, by rule ST_Test.
- If t_{1} is a value, then by the canonical forms lemma for
booleans, either t_{1} = tm_true or t_{1} = tm_false. In either
case, t can step, using rule ST_TestTrue or ST_TestFalse.
- If the final step of the derivation is by T_Sub, then there is a type T_{2} such that T_{1} <: T_{2} and empty ⊢ t_{1} \in T_{1}. The desired result is exactly the induction hypothesis for the typing subderivation.
Theorem progress : ∀ t T,
empty ⊢ t \in T →
value t ∨ ∃ t', t --> t'.
Proof with eauto.
intros t T Ht.
remember empty as Gamma.
induction Ht; subst Gamma; auto.
- (* T_Var *)
discriminate.
- (* T_App *)
right.
destruct IHHt1; subst...
+ (* t_{1} is a value *)
destruct IHHt2; subst...
× (* t_{2} is a value *)
eapply canonical_forms_of_arrow_types in Ht_{1}; [|assumption].
destruct Ht_{1} as [x [S_{1} [s_{2} H_{1}]]]. subst.
∃ (<{ [x:=t_{2}]s_{2} }>)...
× (* t_{2} steps *)
destruct H_{0} as [t_{2}' Hstp]. ∃ <{ t_{1} t_{2}' }>...
+ (* t_{1} steps *)
destruct H as [t_{1}' Hstp]. ∃ <{ t_{1}' t_{2} }>...
- (* T_Test *)
right.
destruct IHHt1.
+ (* t_{1} is a value *) eauto.
+ apply canonical_forms_of_Bool in Ht_{1}; [|assumption].
destruct Ht_{1}; subst...
+ destruct H. rename x into t_{1}'. eauto.
Qed.
intros t T Ht.
remember empty as Gamma.
induction Ht; subst Gamma; auto.
- (* T_Var *)
discriminate.
- (* T_App *)
right.
destruct IHHt1; subst...
+ (* t_{1} is a value *)
destruct IHHt2; subst...
× (* t_{2} is a value *)
eapply canonical_forms_of_arrow_types in Ht_{1}; [|assumption].
destruct Ht_{1} as [x [S_{1} [s_{2} H_{1}]]]. subst.
∃ (<{ [x:=t_{2}]s_{2} }>)...
× (* t_{2} steps *)
destruct H_{0} as [t_{2}' Hstp]. ∃ <{ t_{1} t_{2}' }>...
+ (* t_{1} steps *)
destruct H as [t_{1}' Hstp]. ∃ <{ t_{1}' t_{2} }>...
- (* T_Test *)
right.
destruct IHHt1.
+ (* t_{1} is a value *) eauto.
+ apply canonical_forms_of_Bool in Ht_{1}; [|assumption].
destruct Ht_{1}; subst...
+ destruct 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 x:S_{1}; Gamma ⊢ t_{2} \in 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 \in S. The IH for the typing subderivation tells us that there is some type S_{2} with S_{1} → S_{2} <: S and x:S_{1}; Gamma ⊢ t_{2} \in 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 ⊢ \x:S_{1},t_{2} \in T →
∃ S_{2},
<{S_{1}→S_{2}}> <: T
∧ (x ⊢> S_{1} ; Gamma) ⊢ t_{2} \in S_{2}.
Lemma typing_inversion_var : ∀ Gamma (x:string) T,
Gamma ⊢ x \in T →
∃ S,
Gamma x = Some S ∧ S <: T.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Gamma ⊢ x \in T →
∃ S,
Gamma x = Some S ∧ S <: T.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Lemma typing_inversion_app : ∀ Gamma t_{1} t_{2} T_{2},
Gamma ⊢ t_{1} t_{2} \in T_{2} →
∃ T_{1},
Gamma ⊢ t_{1} \in (T_{1}→T_{2}) ∧
Gamma ⊢ t_{2} \in T_{1}.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Gamma ⊢ t_{1} t_{2} \in T_{2} →
∃ T_{1},
Gamma ⊢ t_{1} \in (T_{1}→T_{2}) ∧
Gamma ⊢ t_{2} \in T_{1}.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Lemma abs_arrow : ∀ x S_{1} s_{2} T_{1} T_{2},
empty ⊢ \x:S_{1},s_{2} \in (T_{1}→T_{2}) →
T_{1} <: S_{1}
∧ (x ⊢> S_{1} ; empty) ⊢ s_{2} \in T_{2}.
Proof with eauto.
intros x S_{1} s_{2} T_{1} T_{2} Hty.
apply typing_inversion_abs in Hty.
destruct Hty as [S_{2} [Hsub Hty1]].
apply sub_inversion_arrow in Hsub.
destruct Hsub as [U_{1} [U_{2} [Heq [Hsub1 Hsub2]]]].
injection Heq as Heq; subst... Qed.
intros x S_{1} s_{2} T_{1} T_{2} Hty.
apply typing_inversion_abs in Hty.
destruct Hty as [S_{2} [Hsub Hty1]].
apply sub_inversion_arrow in Hsub.
destruct Hsub as [U_{1} [U_{2} [Heq [Hsub1 Hsub2]]]].
injection Heq as Heq; subst... Qed.
Lemma weakening : ∀ Gamma Gamma' t T,
inclusion Gamma Gamma' →
Gamma ⊢ t \in T →
Gamma' ⊢ t \in T.
Proof.
intros Gamma Gamma' t T H Ht.
generalize dependent Gamma'.
induction Ht; eauto using inclusion_update.
Qed.
Lemma weakening_empty : ∀ Gamma t T,
empty ⊢ t \in T →
Gamma ⊢ t \in T.
Proof.
intros Gamma t T.
eapply weakening.
discriminate.
Qed.
Substitution
Lemma substitution_preserves_typing : ∀ Gamma x U t v T,
(x ⊢> U ; Gamma) ⊢ t \in T →
empty ⊢ v \in U →
Gamma ⊢ [x:=v]t \in T.
Proof.
Proof.
intros Gamma x U t v T Ht Hv.
remember (x ⊢> U; Gamma) as Gamma'.
generalize dependent Gamma.
induction Ht; intros Gamma' G; simpl; eauto.
(* FILL IN HERE *) Admitted.
intros Gamma x U t v T Ht Hv.
remember (x ⊢> U; Gamma) as Gamma'.
generalize dependent Gamma.
induction Ht; intros Gamma' G; simpl; eauto.
(* FILL IN HERE *) Admitted.
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} \in T_{1} → T_{2}, and
empty ⊢ t_{2} \in T_{1}.
- If the final step of the derivation uses rule T_Test, then
there are terms t_{1}, t_{2}, and t_{3} such that t = tm_if t_{1} then
t_{2} else t_{3}, with empty ⊢ t_{1} \in Bool and with empty ⊢ t_{2}
\in T and empty ⊢ t_{3} \in 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_Test, then t' = tm_if t_{1}' then t_{2}
else t_{3} with t_{1} --> t_{1}'. By the induction hypothesis,
empty ⊢ t_{1}' \in Bool, and so empty ⊢ t' \in T by
T_Test.
- If t --> t' by rule ST_TestTrue or ST_TestFalse, then
either t' = t_{2} or t' = t_{3}, and empty ⊢ t' \in T
follows by assumption.
- If t --> t' by rule ST_Test, then t' = tm_if t_{1}' then t_{2}
else t_{3} with t_{1} --> t_{1}'. By the induction hypothesis,
empty ⊢ t_{1}' \in Bool, and so empty ⊢ t' \in T by
T_Test.
- If the final step of the derivation uses rule T_Test, then
there are terms t_{1}, t_{2}, and t_{3} such that t = tm_if t_{1} then
t_{2} else t_{3}, with empty ⊢ t_{1} \in Bool and with empty ⊢ t_{2}
\in T and empty ⊢ t_{3} \in 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 \in 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 \in T →
t --> t' →
empty ⊢ t' \in T.
Proof with eauto.
intros t t' T HT. generalize dependent t'.
remember empty as Gamma.
induction HT;
intros t' HE; subst;
try solve [inversion HE; subst; eauto].
- (* T_App *)
inversion HE; subst...
(* Most of the cases are immediate by induction,
and eauto takes care of them *)
+ (* ST_AppAbs *)
destruct (abs_arrow _ _ _ _ _ HT_{1}) as [HA_{1} HA_{2}].
apply substitution_preserves_typing with T_{0}...
Qed.
intros t t' T HT. generalize dependent t'.
remember empty as Gamma.
induction HT;
intros t' HE; subst;
try solve [inversion HE; subst; eauto].
- (* T_App *)
inversion HE; subst...
(* Most of the cases are immediate by induction,
and eauto takes care of them *)
+ (* ST_AppAbs *)
destruct (abs_arrow _ _ _ _ _ HT_{1}) as [HA_{1} HA_{2}].
apply substitution_preserves_typing with T_{0}...
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, standard (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}
(* Do not modify the following line: *)
Definition manual_grade_for_variations : option (nat×string) := None.
☐
Exercise: Adding Products
Exercise: 5 stars, standard (products)
Adding pairs, projections, and product types to the system we have defined is a relatively straightforward matter. Carry out this extension by modifying the definitions and proofs above:- Add constructors for pairs, first and second projections,
and product types to the definitions of ty and tm, and
extend the surrounding definitions accordingly
(refer to chapter MoreSTLC):
- value relation
- substitution
- operational semantics
- typing relation
- Extend the subtyping relation with this rule:
S_{1} <: T_{1} S_{2} <: T_{2} (S_Prod) S_{1} * S_{2} <: T_{1} * T_{2} - 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.)
(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_products : option (nat×string) := None.
☐
(* 2020-09-09 21:08 *)