SubSubtyping
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
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 ⊢ t1 ∈ T1 T1 <: T2 | (T_Sub) |
Gamma ⊢ t1 ∈ T2 |
The Subtype Relation
Structural Rules
S <: U U <: T | (S_Trans) |
S <: T |
(S_Refl) | |
T <: T |
Products
S1 <: T1 S2 <: T2 | (S_Prod) |
S1 * S2 <: T1 * T2 |
Arrows
f : C → Student
g : (C→Person) → D
S2 <: T2 | (S_Arrow_Co) |
S1 -> S2 <: S1 -> T2 |
T1 <: S1 S2 <: T2 | (S_Arrow) |
S1 -> S2 <: T1 -> T2 |
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 j1..jn, | |
exists ip in i1..im, such that | |
jk=ip and Sp <: Tk | (S_Rcd) |
{i1:S1...im:Sm} <: {j1:T1...jn:Tn} |
n > m | (S_RcdWidth) |
{i1:T1...in:Tn} <: {i1:T1...im:Tm} |
S1 <: T1 ... Sn <: Tn | (S_RcdDepth) |
{i1:S1...in:Sn} <: {i1:T1...in:Tn} |
{i1:S1...in:Sn} is a permutation of {j1:T1...jn:Tn} | (S_RcdPerm) |
{i1:S1...in:Sn} <: {j1:T1...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:S1 <: T1 S2 <: T2 | (S_Arrow_wrong) |
S1 -> S2 <: T1 -> T2 |
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 ⊢ t1 ∈ T1 T1 <: T2 (T_Sub) Gamma ⊢ t1 ∈ T2 - defining a subtype relation as follows:
S <: U U <: T (S_Trans) S <: T (S_Refl) T <: T (S_Top) S <: Top S1 <: T1 S2 <: T2 (S_Prod) S1 * S2 <: T1 * T2 T1 <: S1 S2 <: T2 (S_Arrow) S1 -> S2 <: T1 -> T2 n > m (S_RcdWidth) {i1:T1...in:Tn} <: {i1:T1...im:Tm} S1 <: T1 ... Sn <: Tn (S_RcdDepth) {i1:S1...in:Sn} <: {i1:T1...in:Tn} {i1:S1...in:Sn} is a permutation of {j1:T1...jn:Tn} (S_RcdPerm) {i1:S1...in:Sn} <: {j1:T1...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 T1 T2,
(S <: T1 → T2) →
∃ S1 S2,
S = S1 → S2 ∧ T1 <: S1 ∧ S2 <: T2
∃ S,
S <: S→S
∃ S,
S→S <: S
∀ S T1 T2,
S <: T1×T2 →
∃ S1 S2,
S = S1×S2 ∧ S1 <: T1 ∧ S2 <: T2
(* 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
S0, S1, 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 S0, S1, 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 typesS1 <: T1 S2 <: T2 | (S_Prod) |
S1*S2 <: T1*T2 |
T1*T2 <: T2*T1 |
(* 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, t1}> ⇒
if eqb_string x y then t else <{\y:T, [x:=s] t1}>
| <{t1 t2}> ⇒
<{([x:=s] t1) ([x:=s] t2)}>
| <{true}> ⇒
<{true}>
| <{false}> ⇒
<{false}>
| <{if t1 then t2 else t3}> ⇒
<{if ([x:=s] t1) then ([x:=s] t2) else ([x:=s] t3)}>
| <{unit}> ⇒
<{unit}>
end
where "'[' x ':=' s ']' t" := (subst x s t) (in custom stlc).
Inductive value : tm → Prop :=
| v_abs : ∀ x T2 t1,
value <{\x:T2, t1}>
| 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 T2 t1 v2,
value v2 →
<{(\x:T2, t1) v2}> --> <{ [x:=v2]t1 }>
| ST_App1 : ∀ t1 t1' t2,
t1 --> t1' →
<{t1 t2}> --> <{t1' t2}>
| ST_App2 : ∀ v1 t2 t2',
value v1 →
t2 --> t2' →
<{v1 t2}> --> <{v1 t2'}>
| ST_IfTrue : ∀ t1 t2,
<{if true then t1 else t2}> --> t1
| ST_IfFalse : ∀ t1 t2,
<{if false then t1 else t2}> --> t2
| ST_If : ∀ t1 t1' t2 t3,
t1 --> t1' →
<{if t1 then t2 else t3}> --> <{if t1' then t2 else t3}>
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 : ∀ S1 S2 T1 T2,
T1 <: S1 →
S2 <: T2 →
<{S1→S2}> <: <{T1→T2}>
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 T1,
Gamma x = Some T1 →
Gamma ⊢ x \in T1
| T_Abs : ∀ Gamma x T1 T2 t1,
(x ⊢> T2 ; Gamma) ⊢ t1 \in T1 →
Gamma ⊢ \x:T2, t1 \in (T2 → T1)
| T_App : ∀ T1 T2 Gamma t1 t2,
Gamma ⊢ t1 \in (T2 → T1) →
Gamma ⊢ t2 \in T2 →
Gamma ⊢ t1 t2 \in T1
| T_True : ∀ Gamma,
Gamma ⊢ true \in Bool
| T_False : ∀ Gamma,
Gamma ⊢ false \in Bool
| T_If : ∀ t1 t2 t3 T1 Gamma,
Gamma ⊢ t1 \in Bool →
Gamma ⊢ t2 \in T1 →
Gamma ⊢ t3 \in T1 →
Gamma ⊢ if t1 then t2 else t3 \in T1
| T_Unit : ∀ Gamma,
Gamma ⊢ unit \in Unit
(* New rule of subsumption: *)
| T_Sub : ∀ Gamma t1 T1 T2,
Gamma ⊢ t1 \in T1 →
T1 <: T2 →
Gamma ⊢ t1 \in T2
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 V1 V2,
U <: <{V1→V2}> →
∃ U1 U2,
U = <{U1→U2}> ∧ V1 <: U1 ∧ U2 <: V2.
U <: <{V1→V2}> →
∃ U1 U2,
U = <{U1→U2}> ∧ V1 <: U1 ∧ U2 <: V2.
☐
Canonical Forms
Exercise: 3 stars, standard, optional (canonical_forms_of_arrow_types)
Lemma canonical_forms_of_arrow_types : ∀ Gamma s T1 T2,
Gamma ⊢ s \in (T1→T2) →
value s →
∃ x S1 s2,
s = <{\x:S1,s2}>.
Gamma ⊢ s \in (T1→T2) →
value s →
∃ x S1 s2,
s = <{\x:S1,s2}>.
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 t1 t2 and types T1 and T2 such that
t = t1 t2, T = T2, empty ⊢ t1 \in T1 → T2, and empty ⊢
t2 \in T1. Moreover, by the induction hypothesis, either t1 is
a value or it steps, and either t2 is a value or it steps.
There are three possibilities to consider:
- Suppose t1 --> t1' for some term t1'. Then t1 t2 --> t1' t2
by ST_App1.
- Suppose t1 is a value and t2 --> t2' for some term t2'.
Then t1 t2 --> t1 t2' by rule ST_App2 because t1 is a
value.
- Finally, suppose t1 and t2 are both values. By the
canonical forms lemma for arrow types, we know that t1 has the
form \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 t1 --> t1' for some term t1'. Then t1 t2 --> t1' t2
by ST_App1.
- If the final step of the derivation uses rule T_Test, then there
are terms t1, t2, and t3 such that t = tm_if t1 then t2 else
t3, with empty ⊢ t1 \in Bool and with empty ⊢ t2 \in T and
empty ⊢ t3 \in T. Moreover, by the induction hypothesis,
either t1 is a value or it steps.
- If t1 is a value, then by the canonical forms lemma for
booleans, either t1 = tm_true or t1 = tm_false. In either
case, t can step, using rule ST_TestTrue or ST_TestFalse.
- If t1 can step, then so can t, by rule ST_Test.
- If t1 is a value, then by the canonical forms lemma for
booleans, either t1 = tm_true or t1 = 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 T2 such that T1 <: T2 and empty ⊢ t1 \in T1. 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...
+ (* t1 is a value *)
destruct IHHt2; subst...
× (* t2 is a value *)
eapply canonical_forms_of_arrow_types in Ht1; [|assumption].
destruct Ht1 as [x [S1 [s2 H1]]]. subst.
∃ (<{ [x:=t2]s2 }>)...
× (* t2 steps *)
destruct H0 as [t2' Hstp]. ∃ <{ t1 t2' }>...
+ (* t1 steps *)
destruct H as [t1' Hstp]. ∃ <{ t1' t2 }>...
- (* T_Test *)
right.
destruct IHHt1.
+ (* t1 is a value *) eauto.
+ apply canonical_forms_of_Bool in Ht1; [|assumption].
destruct Ht1; subst...
+ destruct H. rename x into t1'. eauto.
Qed.
intros t T Ht.
remember empty as Gamma.
induction Ht; subst Gamma; auto.
- (* T_Var *)
discriminate.
- (* T_App *)
right.
destruct IHHt1; subst...
+ (* t1 is a value *)
destruct IHHt2; subst...
× (* t2 is a value *)
eapply canonical_forms_of_arrow_types in Ht1; [|assumption].
destruct Ht1 as [x [S1 [s2 H1]]]. subst.
∃ (<{ [x:=t2]s2 }>)...
× (* t2 steps *)
destruct H0 as [t2' Hstp]. ∃ <{ t1 t2' }>...
+ (* t1 steps *)
destruct H as [t1' Hstp]. ∃ <{ t1' t2 }>...
- (* T_Test *)
right.
destruct IHHt1.
+ (* t1 is a value *) eauto.
+ apply canonical_forms_of_Bool in Ht1; [|assumption].
destruct Ht1; subst...
+ destruct H. rename x into t1'. eauto.
Qed.
Inversion Lemmas for Typing
- If the last step of the derivation is a use of T_Abs then there is a type T12 such that T = S1 → T12 and x:S1; Gamma ⊢ t2 \in T12. Picking T12 for S2 gives us what we need: S1 → T12 <: S1 → T12 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:S1.t2 \in S. The IH for the typing subderivation tells us that there is some type S2 with S1 → S2 <: S and x:S1; Gamma ⊢ t2 \in S2. Picking type S2 gives us what we need, since S1 → S2 <: T then follows by S_Trans.
Lemma typing_inversion_abs : ∀ Gamma x S1 t2 T,
Gamma ⊢ \x:S1,t2 \in T →
∃ S2,
<{S1→S2}> <: T
∧ (x ⊢> S1 ; Gamma) ⊢ t2 \in S2.
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 t1 t2 T2,
Gamma ⊢ t1 t2 \in T2 →
∃ T1,
Gamma ⊢ t1 \in (T1→T2) ∧
Gamma ⊢ t2 \in T1.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Gamma ⊢ t1 t2 \in T2 →
∃ T1,
Gamma ⊢ t1 \in (T1→T2) ∧
Gamma ⊢ t2 \in T1.
Proof with eauto.
(* FILL IN HERE *) Admitted.
☐
Lemma abs_arrow : ∀ x S1 s2 T1 T2,
empty ⊢ \x:S1,s2 \in (T1→T2) →
T1 <: S1
∧ (x ⊢> S1 ; empty) ⊢ s2 \in T2.
Proof with eauto.
intros x S1 s2 T1 T2 Hty.
apply typing_inversion_abs in Hty.
destruct Hty as [S2 [Hsub Hty1]].
apply sub_inversion_arrow in Hsub.
destruct Hsub as [U1 [U2 [Heq [Hsub1 Hsub2]]]].
injection Heq as Heq; subst... Qed.
intros x S1 s2 T1 T2 Hty.
apply typing_inversion_abs in Hty.
destruct Hty as [S2 [Hsub Hty1]].
apply sub_inversion_arrow in Hsub.
destruct Hsub as [U1 [U2 [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 t1 and t2 and types T1 and T2 such that
t = t1 t2, T = T2, empty ⊢ t1 \in T1 → T2, and
empty ⊢ t2 \in T1.
- If the final step of the derivation uses rule T_Test, then
there are terms t1, t2, and t3 such that t = tm_if t1 then
t2 else t3, with empty ⊢ t1 \in Bool and with empty ⊢ t2
\in T and empty ⊢ t3 \in T. Moreover, by the induction
hypothesis, if t1 steps to t1' then empty ⊢ t1' : 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 t1' then t2
else t3 with t1 --> t1'. By the induction hypothesis,
empty ⊢ t1' \in Bool, and so empty ⊢ t' \in T by
T_Test.
- If t --> t' by rule ST_TestTrue or ST_TestFalse, then
either t' = t2 or t' = t3, and empty ⊢ t' \in T
follows by assumption.
- If t --> t' by rule ST_Test, then t' = tm_if t1' then t2
else t3 with t1 --> t1'. By the induction hypothesis,
empty ⊢ t1' \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 t1, t2, and t3 such that t = tm_if t1 then
t2 else t3, with empty ⊢ t1 \in Bool and with empty ⊢ t2
\in T and empty ⊢ t3 \in T. Moreover, by the induction
hypothesis, if t1 steps to t1' then empty ⊢ t1' : 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 _ _ _ _ _ HT1) as [HA1 HA2].
apply substitution_preserves_typing with T0...
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 _ _ _ _ _ HT1) as [HA1 HA2].
apply substitution_preserves_typing with T0...
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 ∈ S1->S2 S1 <: T1 T1 <: S1 S2 <: T2 (T_Funny1) Gamma ⊢ t ∈ T1->T2 - 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:
S1 <: T1 S2 <: T2 (S_Arrow') S1->S2 <: T1->T2
(* 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:
S1 <: T1 S2 <: T2 (S_Prod) S1 * S2 <: T1 * T2 - 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.
☐
(* 2021-03-18 17:24 *)