RecordsAdding Records to STLC
Require Import SfLib.
Require Import Maps.
Require Import Imp.
Require Import Smallstep.
Require Import Stlc.
Adding Records
t ::= Terms: | ... | {i1=t1, ..., in=tn} record | t.i projection v ::= Values: | ... | {i1=v1, ..., in=vn} record value T ::= Types: | ... | {i1:T1, ..., in:Tn} record typeReduction:
ti ⇒ ti' (ST_Rcd) | |
{i1=v1, ..., im=vm, in=tn, ...} ⇒ {i1=v1, ..., im=vm, in=tn', ...} |
t1 ⇒ t1' | (ST_Proj1) |
t1.i ⇒ t1'.i |
(ST_ProjRcd) | |
{..., i=vi, ...}.i ⇒ vi |
Γ ⊢ t1 : T1 ... Γ ⊢ tn : Tn | (T_Rcd) |
Γ ⊢ {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn} |
Γ ⊢ t : {..., i:Ti, ...} | (T_Proj) |
Γ ⊢ t.i : Ti |
Syntax and Operational Semantics
Module FirstTry.
Definition alist (X : Type) := list (id × X).
Inductive ty : Type :=
| TBase : id → ty
| TArrow : ty → ty → ty
| TRcd : (alist ty) → ty.
Unfortunately, we encounter here a limitation in Coq: this type
does not automatically give us the induction principle we expect
the induction hypothesis in the TRcd case doesn't give us
any information about the ty elements of the list, making it
useless for the proofs we want to do.
(* Check ty_ind.
====>
ty_ind :
forall P : ty -> Prop,
(forall i : id, P (TBase i)) ->
(forall t : ty, P t -> forall t0 : ty, P t0 -> P (TArrow t t0)) ->
(forall a : alist ty, P (TRcd a)) -> (* ??? *)
forall t : ty, P t
*)
End FirstTry.
It is possible to get a better induction principle out of Coq, but
the details of how this is done are not very pretty, and it is not
as intuitive to use as the ones Coq generates automatically for
simple Inductive definitions.
Fortunately, there is a different way of formalizing records that
is, in some ways, even simpler and more natural: instead of using
the existing list type, we can essentially include its
constructors ("nil" and "cons") in the syntax of types.
Inductive ty : Type :=
| TBase : id → ty
| TArrow : ty → ty → ty
| TRNil : ty
| TRCons : id → ty → ty → ty.
Similarly, at the level of terms, we have constructors trnil
the empty record — and trcons, which adds a single field to
the front of a list of fields.
Inductive tm : Type :=
| tvar : id → tm
| tapp : tm → tm → tm
| tabs : id → ty → tm → tm
(* records *)
| tproj : tm → id → tm
| trnil : tm
| trcons : id → tm → tm → tm.
Some variables, for examples...
Notation a := (Id 0).
Notation f := (Id 1).
Notation g := (Id 2).
Notation l := (Id 3).
Notation A := (TBase (Id 4)).
Notation B := (TBase (Id 5)).
Notation k := (Id 6).
Notation i1 := (Id 7).
Notation i2 := (Id 8).
{ i1:A }
(* Check (TRCons i1 A TRNil). *)
{ i1:A→B, i2:A }
(* Check (TRCons i1 (TArrow A B)
(TRCons i2 A TRNil)). *)
Well-Formedness
where the "tail" of a record type is not actually a record type!
We'll structure our typing judgement so that no ill-formed types
like weird_type are assigned to terms. To support this, we
define record_ty and record_tm, which identify record types
and terms, and well_formed_ty which rules out the ill-formed
types.
First, a type is a record type if it is built with just TRNil
and TRCons at the outermost level.
Inductive record_ty : ty → Prop :=
| RTnil :
record_ty TRNil
| RTcons : ∀i T1 T2,
record_ty (TRCons i T1 T2).
Similarly, a term is a record term if it is built with trnil
and trcons
Inductive record_tm : tm → Prop :=
| rtnil :
record_tm trnil
| rtcons : ∀i t1 t2,
record_tm (trcons i t1 t2).
Note that record_ty and record_tm are not recursive — they
just check the outermost constructor. The well_formed_ty
property, on the other hand, verifies that the whole type is well
formed in the sense that the tail of every record (the second
argument to TRCons) is a record.
Of course, we should also be concerned about ill-formed terms, not
just types; but typechecking can rules those out without the help
of an extra well_formed_tm definition because it already
examines the structure of terms. LATER : should they fill in part of this as an exercise? We
didn't give rules for it above
Inductive well_formed_ty : ty → Prop :=
| wfTBase : ∀i,
well_formed_ty (TBase i)
| wfTArrow : ∀T1 T2,
well_formed_ty T1 →
well_formed_ty T2 →
well_formed_ty (TArrow T1 T2)
| wfTRNil :
well_formed_ty TRNil
| wfTRCons : ∀i T1 T2,
well_formed_ty T1 →
well_formed_ty T2 →
record_ty T2 →
well_formed_ty (TRCons i T1 T2).
Hint Constructors record_ty record_tm well_formed_ty.
Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
match t with
| tvar y ⇒ if beq_id x y then s else t
| tabs y T t1 ⇒ tabs y T (if beq_id x y then t1 else (subst x s t1))
| tapp t1 t2 ⇒ tapp (subst x s t1) (subst x s t2)
| tproj t1 i ⇒ tproj (subst x s t1) i
| trnil ⇒ trnil
| trcons i t1 tr1 ⇒ trcons i (subst x s t1) (subst x s tr1)
end.
Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
Inductive value : tm → Prop :=
| v_abs : ∀x T11 t12,
value (tabs x T11 t12)
| v_rnil : value trnil
| v_rcons : ∀i v1 vr,
value v1 →
value vr →
value (trcons i v1 vr).
Hint Constructors value.
Utility functions for extracting one field from record type or
term:
Fixpoint Tlookup (i:id) (Tr:ty) : option ty :=
match Tr with
| TRCons i' T Tr' ⇒ if beq_id i i' then Some T else Tlookup i Tr'
| _ ⇒ None
end.
Fixpoint tlookup (i:id) (tr:tm) : option tm :=
match tr with
| trcons i' t tr' ⇒ if beq_id i i' then Some t else tlookup i tr'
| _ ⇒ None
end.
The step function uses the term-level lookup function (for the
projection rule), while the type-level lookup is needed for
has_type.
Reserved Notation "t1 '⇒' t2" (at level 40).
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀x T11 t12 v2,
value v2 →
(tapp (tabs x T11 t12) v2) ⇒ ([x:=v2]t12)
| ST_App1 : ∀t1 t1' t2,
t1 ⇒ t1' →
(tapp t1 t2) ⇒ (tapp t1' t2)
| ST_App2 : ∀v1 t2 t2',
value v1 →
t2 ⇒ t2' →
(tapp v1 t2) ⇒ (tapp v1 t2')
| ST_Proj1 : ∀t1 t1' i,
t1 ⇒ t1' →
(tproj t1 i) ⇒ (tproj t1' i)
| ST_ProjRcd : ∀tr i vi,
value tr →
tlookup i tr = Some vi →
(tproj tr i) ⇒ vi
| ST_Rcd_Head : ∀i t1 t1' tr2,
t1 ⇒ t1' →
(trcons i t1 tr2) ⇒ (trcons i t1' tr2)
| ST_Rcd_Tail : ∀i v1 tr2 tr2',
value v1 →
tr2 ⇒ tr2' →
(trcons i v1 tr2) ⇒ (trcons i v1 tr2')
where "t1 '⇒' t2" := (step t1 t2).
Notation multistep := (multi step).
Notation "t1 '⇒*' t2" := (multistep t1 t2) (at level 40).
Hint Constructors step.
Next we define the typing rules. These are nearly direct
transcriptions of the inference rules shown above. The only major
difference is the use of well_formed_ty. In the informal
presentation we used a grammar that only allowed well formed
record types, so we didn't have to add a separate check.
We'd like to set things up so that that whenever has_type Γ t
T holds, we also have well_formed_ty T. That is, has_type
never assigns ill-formed types to terms. In fact, we prove this
theorem below.
However, we don't want to clutter the definition of has_type
with unnecessary uses of well_formed_ty. Instead, we place
well_formed_ty checks only where needed - where an inductive
call to has_type won't already be checking the well-formedness
of a type.
For example, we check well_formed_ty T in the T_Var case,
because there is no inductive has_type call that would
enforce this. Similarly, in the T_Abs case, we require a
proof of well_formed_ty T11 because the inductive call to
has_type only guarantees that T12 is well-formed.
In the rules you must write, the only necessary well_formed_ty
check comes in the tnil case.
Reserved Notation "Gamma '⊢' t '∈' T" (at level 40).
Inductive has_type : context → tm → ty → Prop :=
| T_Var : ∀Γ x T,
Γ x = Some T →
well_formed_ty T →
Γ ⊢ (tvar x) ∈ T
| T_Abs : ∀Γ x T11 T12 t12,
well_formed_ty T11 →
(update Γ x T11) ⊢ t12 ∈ T12 →
Γ ⊢ (tabs x T11 t12) ∈ (TArrow T11 T12)
| T_App : ∀T1 T2 Γ t1 t2,
Γ ⊢ t1 ∈ (TArrow T1 T2) →
Γ ⊢ t2 ∈ T1 →
Γ ⊢ (tapp t1 t2) ∈ T2
(* records: *)
| T_Proj : ∀Γ i t Ti Tr,
Γ ⊢ t ∈ Tr →
Tlookup i Tr = Some Ti →
Γ ⊢ (tproj t i) ∈ Ti
| T_RNil : ∀Γ,
Γ ⊢ trnil ∈ TRNil
| T_RCons : ∀Γ i t T tr Tr,
Γ ⊢ t ∈ T →
Γ ⊢ tr ∈ Tr →
record_ty Tr →
record_tm tr →
Γ ⊢ (trcons i t tr) ∈ (TRCons i T Tr)
where "Gamma '⊢' t '∈' T" := (has_type Γ t T).
Hint Constructors has_type.
Examples
Exercise: 2 stars (examples)
Finish the proofs.Lemma typing_example_2 :
empty ⊢
(tapp (tabs a (TRCons i1 (TArrow A A)
(TRCons i2 (TArrow B B)
TRNil))
(tproj (tvar a) i2))
(trcons i1 (tabs a A (tvar a))
(trcons i2 (tabs a B (tvar a))
trnil))) ∈
(TArrow B B).
Proof.
(* FILL IN HERE *) Admitted.
Before starting to prove this fact (or the one above!), make sure
you understand what it is saying.
Example typing_nonexample :
¬ ∃T,
(update empty a (TRCons i2 (TArrow A A)
TRNil)) ⊢
(trcons i1 (tabs a B (tvar a)) (tvar a)) ∈
T.
Proof.
(* FILL IN HERE *) Admitted.
Example typing_nonexample_2 : ∀y,
¬ ∃T,
(update empty y A) ⊢
(tapp (tabs a (TRCons i1 A TRNil)
(tproj (tvar a) i1))
(trcons i1 (tvar y) (trcons i2 (tvar y) trnil))) ∈
T.
Proof.
(* FILL IN HERE *) Admitted.
Properties of Typing
Lemma wf_rcd_lookup : ∀i T Ti,
well_formed_ty T →
Tlookup i T = Some Ti →
well_formed_ty Ti.
Proof with eauto.
intros i T.
induction T; intros; try solve by inversion.
- (* TRCons *)
inversion H. subst. unfold Tlookup in H0.
destruct (beq_id i i0)...
inversion H0. subst... Qed.
Lemma step_preserves_record_tm : ∀tr tr',
record_tm tr →
tr ⇒ tr' →
record_tm tr'.
Proof.
intros tr tr' Hrt Hstp.
inversion Hrt; subst; inversion Hstp; subst; auto.
Qed.
Lemma has_type__wf : ∀Γ t T,
Γ ⊢ t ∈ T → well_formed_ty T.
Proof with eauto.
intros Γ t T Htyp.
induction Htyp...
- (* T_App *)
inversion IHHtyp1...
- (* T_Proj *)
eapply wf_rcd_lookup...
Qed.
Field Lookup
- If i = i0, then since Tlookup i (TRCons i0 T Tr) = Some
Ti we have T = Ti. It follows that t itself satisfies
the theorem.
- On the other hand, suppose i ≠ i0. Then
Tlookup i T = Tlookup i Trandtlookup i t = tlookup i tr,so the result follows from the induction hypothesis. ☐
Lemma lookup_field_in_value : ∀v T i Ti,
value v →
empty ⊢ v ∈ T →
Tlookup i T = Some Ti →
∃ti, tlookup i v = Some ti ∧ empty ⊢ ti ∈ Ti.
Proof with eauto.
intros v T i Ti Hval Htyp Hget.
remember (@empty ty) as Γ.
induction Htyp; subst; try solve by inversion...
- (* T_RCons *)
simpl in Hget. simpl. destruct (beq_id i i0).
+ (* i is first *)
simpl. inversion Hget. subst.
∃t...
+ (* get tail *)
destruct IHHtyp2 as [vi [Hgeti Htypi]]...
inversion Hval... Qed.
Theorem progress : ∀t T,
empty ⊢ t ∈ T →
value t ∨ ∃t', t ⇒ t'.
Proof with eauto.
(* Theorem: Suppose empty |- t : T. Then either
1. t is a value, or
2. t ==> t' for some t'.
Proof: By induction on the given typing derivation. *)
intros t T Ht.
remember (@empty ty) as Γ.
generalize dependent HeqGamma.
induction Ht; intros HeqGamma; subst.
- (* T_Var *)
(* The final rule in the given typing derivation cannot be T_Var,
since it can never be the case that empty ⊢ x : T (since the
context is empty). *)
inversion H.
- (* T_Abs *)
(* If the T_Abs rule was the last used, then t = tabs x T11 t12,
which is a value. *)
left...
- (* T_App *)
(* If the last rule applied was T_App, then t = t1 t2, and we know
from the form of the rule that
empty ⊢ t1 : T1 → T2
empty ⊢ t2 : T1
By the induction hypothesis, each of t1 and t2 either is a value
or can take a step. *)
right.
destruct IHHt1; subst...
+ (* t1 is a value *)
destruct IHHt2; subst...
× (* t2 is a value *)
(* If both t1 and t2 are values, then we know that
t1 = tabs x T11 t12, since abstractions are the only values
that can have an arrow type. But
(tabs x T11 t12) t2 ⇒ [x:=t2]t12 by ST_AppAbs. *)
inversion H; subst; try (solve by inversion).
∃([x:=t2]t12)...
× (* t2 steps *)
(* If t1 is a value and t2 ⇒ t2', then t1 t2 ⇒ t1 t2'
by ST_App2. *)
destruct H0 as [t2' Hstp]. ∃(tapp t1 t2')...
+ (* t1 steps *)
(* Finally, If t1 ⇒ t1', then t1 t2 ⇒ t1' t2 by ST_App1. *)
destruct H as [t1' Hstp]. ∃(tapp t1' t2)...
- (* T_Proj *)
(* If the last rule in the given derivation is T_Proj, then
t = tproj t i and
empty ⊢ t : (TRcd Tr)
By the IH, t either is a value or takes a step. *)
right. destruct IHHt...
+ (* rcd is value *)
(* If t is a value, then we may use lemma
lookup_field_in_value to show tlookup i t = Some ti for
some ti which gives us tproj i t ⇒ ti by ST_ProjRcd
*)
destruct (lookup_field_in_value _ _ _ _ H0 Ht H) as [ti [Hlkup _]].
∃ti...
+ (* rcd_steps *)
(* On the other hand, if t ⇒ t', then tproj t i ⇒ tproj t' i
by ST_Proj1. *)
destruct H0 as [t' Hstp]. ∃(tproj t' i)...
- (* T_RNil *)
(* If the last rule in the given derivation is T_RNil, then
t = trnil, which is a value. *)
left...
- (* T_RCons *)
(* If the last rule is T_RCons, then t = trcons i t tr and
empty ⊢ t : T
empty ⊢ tr : Tr
By the IH, each of t and tr either is a value or can take
a step. *)
destruct IHHt1...
+ (* head is a value *)
destruct IHHt2; try reflexivity.
× (* tail is a value *)
(* If t and tr are both values, then trcons i t tr
is a value as well. *)
left...
× (* tail steps *)
(* If t is a value and tr ⇒ tr', then
trcons i t tr ⇒ trcons i t tr' by
ST_Rcd_Tail. *)
right. destruct H2 as [tr' Hstp].
∃(trcons i t tr')...
+ (* head steps *)
(* If t ⇒ t', then
trcons i t tr ⇒ trcons i t' tr
by ST_Rcd_Head. *)
right. destruct H1 as [t' Hstp].
∃(trcons i t' tr)... Qed.
Inductive appears_free_in : id → tm → Prop :=
| afi_var : ∀x,
appears_free_in x (tvar x)
| afi_app1 : ∀x t1 t2,
appears_free_in x t1 → appears_free_in x (tapp t1 t2)
| afi_app2 : ∀x t1 t2,
appears_free_in x t2 → appears_free_in x (tapp t1 t2)
| afi_abs : ∀x y T11 t12,
y ≠ x →
appears_free_in x t12 →
appears_free_in x (tabs y T11 t12)
| afi_proj : ∀x t i,
appears_free_in x t →
appears_free_in x (tproj t i)
| afi_rhead : ∀x i ti tr,
appears_free_in x ti →
appears_free_in x (trcons i ti tr)
| afi_rtail : ∀x i ti tr,
appears_free_in x tr →
appears_free_in x (trcons i ti tr).
Hint Constructors appears_free_in.
Lemma context_invariance : ∀Γ Γ' t S,
Γ ⊢ t ∈ S →
(∀x, appears_free_in x t → Γ x = Γ' x) →
Γ' ⊢ t ∈ S.
Proof with eauto.
intros. generalize dependent Γ'.
induction H;
intros Γ' Heqv...
- (* T_Var *)
apply T_Var... rewrite ← Heqv...
- (* T_Abs *)
apply T_Abs... apply IHhas_type. intros y Hafi.
unfold update, t_update. destruct (beq_idP x y)...
- (* T_App *)
apply T_App with T1...
- (* T_RCons *)
apply T_RCons... Qed.
Lemma free_in_context : ∀x t T Γ,
appears_free_in x t →
Γ ⊢ t ∈ T →
∃T', Γ x = Some T'.
Proof with eauto.
intros x t T Γ Hafi Htyp.
induction Htyp; inversion Hafi; subst...
- (* T_Abs *)
destruct IHHtyp as [T' Hctx]... ∃T'.
unfold update, t_update in Hctx.
rewrite false_beq_id in Hctx...
Qed.
Lemma substitution_preserves_typing : ∀Γ x U v t S,
(update Γ x U) ⊢ t ∈ S →
empty ⊢ v ∈ U →
Γ ⊢ ([x:=v]t) ∈ S.
Proof with eauto.
(* Theorem: If Gamma,x:U |- t : S and empty |- v : U, then
Gamma |- (x:=vt) S. *)
intros Γ x U v t S Htypt Htypv.
generalize dependent Γ. generalize dependent S.
(* Proof: By induction on the term t. Most cases follow directly
from the IH, with the exception of tvar, tabs, trcons.
The former aren't automatic because we must reason about how the
variables interact. In the case of trcons, we must do a little
extra work to show that substituting into a term doesn't change
whether it is a record term. *)
induction t;
intros S Γ Htypt; simpl; inversion Htypt; subst...
- (* tvar *)
simpl. rename i into y.
(* If t = y, we know that
empty ⊢ v : U and
Γ,x:U ⊢ y : S
and, by inversion, update Γ x U y = Some S. We want to
show that Γ ⊢ [x:=v]y : S.
There are two cases to consider: either x=y or x≠y. *)
unfold update, t_update in H0. destruct (beq_idP x y) as [Hxy|Hxy].
+ (* x=y *)
(* If x = y, then we know that U = S, and that [x:=v]y = v.
So what we really must show is that if empty ⊢ v : U then
Γ ⊢ v : U. We have already proven a more general version
of this theorem, called context invariance. *)
subst.
inversion H0; subst. clear H0.
eapply context_invariance...
intros x Hcontra.
destruct (free_in_context _ _ S empty Hcontra) as [T' HT']...
inversion HT'.
+ (* x<>y *)
(* If x ≠ y, then Γ y = Some S and the substitution has no
effect. We can show that Γ ⊢ y : S by T_Var. *)
apply T_Var...
- (* tabs *)
rename i into y. rename t into T11.
(* If t = tabs y T11 t0, then we know that
Γ,x:U ⊢ tabs y T11 t0 : T11→T12
Γ,x:U,y:T11 ⊢ t0 : T12
empty ⊢ v : U
As our IH, we know that forall S Gamma,
Γ,x:U ⊢ t0 : S → Γ ⊢ [x:=v]t0 S.
We can calculate that
x:=vt = tabs y T11 (if beq_id x y then t0 else x:=vt0)
And we must show that Γ ⊢ [x:=v]t : T11→T12. We know
we will do so using T_Abs, so it remains to be shown that:
Γ,y:T11 ⊢ if beq_id x y then t0 else [x:=v]t0 : T12
We consider two cases: x = y and x ≠ y.
*)
apply T_Abs...
destruct (beq_idP x y) as [Hxy|Hxy].
+ (* x=y *)
(* If x = y, then the substitution has no effect. Context
invariance shows that Γ,y:U,y:T11 and Γ,y:T11 are
equivalent. Since the former context shows that t0 : T12, so
does the latter. *)
eapply context_invariance...
subst.
intros x Hafi. unfold update, t_update.
destruct (beq_id y x)...
+ (* x<>y *)
(* If x ≠ y, then the IH and context invariance allow us to show that
Γ,x:U,y:T11 ⊢ t0 : T12 =>
Γ,y:T11,x:U ⊢ t0 : T12 =>
Γ,y:T11 ⊢ [x:=v]t0 : T12 *)
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (beq_idP y z)...
subst. rewrite false_beq_id...
- (* trcons *)
apply T_RCons... inversion H7; subst; simpl...
Qed.
Theorem preservation : ∀t t' T,
empty ⊢ t ∈ T →
t ⇒ t' →
empty ⊢ t' ∈ T.
Proof with eauto.
intros t t' T HT.
(* Theorem: If empty ⊢ t : T and t ⇒ t', then empty ⊢ t' : T. *)
remember (@empty ty) as Γ. generalize dependent HeqGamma.
generalize dependent t'.
(* Proof: By induction on the given typing derivation. Many cases are
contradictory (T_Var, T_Abs) or follow directly from the IH
(T_RCons). We show just the interesting ones. *)
induction HT;
intros t' HeqGamma HE; subst; inversion HE; subst...
- (* T_App *)
(* If the last rule used was T_App, then t = t1 t2, and three rules
could have been used to show t ⇒ t': ST_App1, ST_App2, and
ST_AppAbs. In the first two cases, the result follows directly from
the IH. *)
inversion HE; subst...
+ (* ST_AppAbs *)
(* For the third case, suppose
t1 = tabs x T11 t12
and
t2 = v2. We must show that empty ⊢ [x:=v2]t12 : T2.
We know by assumption that
empty ⊢ tabs x T11 t12 : T1→T2
and by inversion
x:T1 ⊢ t12 : T2
We have already proven that substitution_preserves_typing and
empty ⊢ v2 : T1
by assumption, so we are done. *)
apply substitution_preserves_typing with T1...
inversion HT1...
- (* T_Proj *)
(* If the last rule was T_Proj, then t = tproj t1 i. Two rules
could have caused t ⇒ t': T_Proj1 and T_ProjRcd. The typing
of t' follows from the IH in the former case, so we only
consider T_ProjRcd.
Here we have that t is a record value. Since rule T_Proj was
used, we know empty ⊢ t ∈ Tr and Tlookup i Tr = Some Ti for some i and Tr. We may therefore apply lemma
lookup_field_in_value to find the record element this
projection steps to. *)
destruct (lookup_field_in_value _ _ _ _ H2 HT H)
as [vi [Hget Htyp]].
rewrite H4 in Hget. inversion Hget. subst...
- (* T_RCons *)
(* If the last rule was T_RCons, then t = trcons i t tr for
some i, t and tr such that record_tm tr. If the step is
by ST_Rcd_Head, the result is immediate by the IH. If the step
is by ST_Rcd_Tail, tr ⇒ tr2' for some tr2' and we must also
use lemma step_preserves_record_tm to show record_tm tr2'. *)
apply T_RCons... eapply step_preserves_record_tm...
Qed.
☐