(** * MoreStlc: More on the Simply Typed Lambda-Calculus *) (* Version of 9/13/2009 *) Require Export Stlc. Require Import Relations. (* ###################################################################### *) (** * Typechecking for STLC *) (** The [has_type] relation defines what it means for a term to belong to a type (in some context). But it doesn't, in itself, tell us how to _check_ whether or not a term is well typed. Fortunately, the rules defining [has_type] are _syntax directed_ -- they exactly follow the shape of the term. This makes it straightforward to translate the typing rules into clauses of a typechecking _function_ that takes a term and a context and either returns the term's type or else signals that the term is not typable. *) Module STLCChecker. Import STLC. (* ###################################################################### *) (** ** Comparing types *) (** First, we need a function to compare two types for equality... *) Fixpoint beq_ty (T1 T2:ty) {struct T1} : bool := match T1,T2 with | ty_base i, ty_base i' => beq_id i i' | ty_arrow T11 T12, ty_arrow T21 T22 => andb (beq_ty T11 T21) (beq_ty T12 T22) | _,_ => false end. (** ... and we need to establish the usual two-way connection between [beq_ty] returning the boolean [true] and the logical proposition that its inputs are equal. *) Lemma beq_ty_refl : forall T1, beq_ty T1 T1 = true. Proof. intros T1. induction T1; simpl. apply sym_eq. apply beq_id_refl. rewrite IHT1_1. rewrite IHT1_2. reflexivity. Qed. Lemma beq_ty__eq : forall T1 T2, beq_ty T1 T2 = true -> T1 = T2. Proof with auto. intros T1. induction T1; intros T2 Hbeq; destruct T2; inversion Hbeq. Case "T1=ty_base i". apply sym_eq in H0. apply beq_id_eq in H0. subst... Case "T1=ty_arrow T1_1 T1_2". apply andb_true in H0. destruct H0 as [Hbeq1 Hbeq2]. apply IHT1_1 in Hbeq1. apply IHT1_2 in Hbeq2. subst... Qed. (* ###################################################################### *) (** ** The typechecker *) (** Now here's the typechecker. It works by walking over the structure of the given term, returning either [Some T] or [None]. Each time we make a recursive call to find out the types of the subterms, we need to pattern-match on the results to make sure that they are not [None]. Also, in the [tm_app] case, we use pattern matching to extract the left- and right-hand sides of the function's arrow type (and fail if the type of the function is not [ty_arrow T11 T12] for some [T1] and [T2]). *) Fixpoint type_check (Gamma:context) (t:tm) {struct t} : option ty := match t with | tm_var x => Gamma x | tm_abs x T1 t1 => match type_check (extend Gamma x T1) t1 with | Some T2 => Some (ty_arrow T1 T2) | _ => None end | tm_app t1 t2 => match type_check Gamma t1, type_check Gamma t2 with | Some (ty_arrow T11 T12),Some T2 => if beq_ty T11 T2 then Some T12 else None | _,_ => None end end. (* ###################################################################### *) (** ** Properties *) (** To verify that this typechecking algorithm is the correct one, we show that it is SOUND and COMPLETE for the original [has_type] relation -- that is, [type_check] and [has_type] define the same partial function. *) Theorem type_checking_sound : forall Gamma t T, type_check Gamma t = Some T -> has_type Gamma t T. Proof with eauto. intros Gamma t. generalize dependent Gamma. (tm_cases (induction t) Case); intros Gamma T Htc; inversion Htc. Case "tm_var"... Case "tm_app". remember (type_check Gamma t1) as TO1. remember (type_check Gamma t2) as TO2. destruct TO1 as [T1|]; try solve by inversion; destruct T1 as [|T11 T12]; try solve by inversion. destruct TO2 as [T2|]; try solve by inversion. remember (beq_ty T11 T2) as b. destruct b; try solve by inversion. symmetry in Heqb. apply beq_ty__eq in Heqb. inversion H0; subst... Case "tm_abs". rename i into y. rename t into T1. remember (extend Gamma y T1) as G'. remember (type_check G' t0) as TO2. destruct TO2; try solve by inversion. inversion H0; subst... Qed. Theorem type_checking_complete : forall Gamma t T, has_type Gamma t T -> type_check Gamma t = Some T. Proof with auto. intros Gamma t T Hty. (typing_cases (induction Hty) Case); simpl. Case "T_Var"... Case "T_Abs". rewrite IHHty... Case "T_App". rewrite IHHty1. rewrite IHHty2. rewrite (beq_ty_refl T1)... Qed. End STLCChecker. (* ###################################################################### *) (** * Simple Extensions to STLC *) (** *** [let]-bindings *) (** When writing a complex expression, it is often useful---both for avoiding repetition and for increasing readability---to give names to some of its subexpressions. Most languages provide one or more ways of doing this. In OCaml, for example, we can write [let x=t1 in t2] to mean ``evaluate the expression [t1] and bind the name [x] to the resulting value while evaluating [t2].'' Our [let]-binder follows ML's in choosing a call-by-value evaluation order, where the [let]-bound term must be fully evaluated before evaluation of the [let]-body can begin. The typing rule [T_Let] tells us that the type of a [let] can be calculated by calculating the type of the [let]-bound term, extending the context with a binding with this type, and in this enriched context calculating the type of the body, which is then the type of the whole [let] expression. At this point in the course, it's probably just as easy to simply look at the rules defining this new feature as to wade through a lot of english text conveying the same information. Here they are: Syntax: << t ::= Terms: | x variable | \x:T. t abstraction | t t application | let x=t in t let-binding >> Reduction: << t1 ~~> t1' ---------------------------------- (ST_Let1) let x=t1 in t2 ~~> let x=t1' in t2 ---------------------------- (ST_LetValue) let x=v1 in t2 ~~> [v1/x] t2 >> Typing: << Gamma |- t1 : T1 Gamma, x:T1 |- t2 : T2 -------------------------------------------- (T_Let) Gamma |- let x=t1 in t2 : T2 >> *) (** *** Pairs *) (** Our functional programming examples have made frequent use of _pairs_ of values. The type of such pairs is called a _product type_. In Coq's functional language, the primitive way of extracting the components of a pair is _pattern matching_. An alternative style is to take [fst] and [snd] -- the first- and second-projection operators -- as primitives. Just for fun (and for compatibility with the way we're going to do records just below), let's do our products this way. Syntax: << t ::= Terms: | ... | (t,t) pair | t.fst first projection | t.snd second projection v ::= Values: | \x:T.t | (v,v) pair value T ::= Types: | A base type | T -> T arrow type | T * T product type >> Reduction: << t1 ~~> t1' -------------------- (ST_Pair1) (t1,t2) ~~> (t1',t2) t2 ~~> t2' -------------------- (ST_Pair2) (v1,t2) ~~> (v1,t2') t1 ~~> t1' ------------------ (ST_Fst1) t1.fst ~~> t1'.fst ------------------ (ST_FstPair) (v1,v2).fst ~~> v1 t1 ~~> t1' ------------------ (ST_Snd1) t1.snd ~~> t1'.snd ------------------ (ST_SndPair) (v1,v2).snd ~~> v2 >> (Note the implicit convention that metavariables like [v1] always denote values.) Typing: << Gamma |- t1 : T1 Gamma |- t2 : T2 --------------------------------------- (T_Pair) Gamma |- (t1,t2) : T1*T2 Gamma |- t1 : T1*T2 -------------------- (T_Fst) Gamma |- t1.fst : T1 Gamma |- t1 : T1*T2 -------------------- (T_Snd) Gamma |- t1.snd : T2 >> *) (** *** Records *) (** Next, let's look at the generalization of products to _records_ -- n-ary products with labeled fields. *) (** Syntax: << 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 type >> Intuitively, the generalization is pretty obvious. But it's worth noticing that what we've actually written is rather informal: in particular, we've written "[...]" in several places to mean "any number of these," and we've omitted explicit mention of the usual side-condition that the labels of a record should not contain repetitions. It is possible to devise informal notations that are more precise, but these tend to be quite heavy and to obscure the main points of the definitions. So we'll leave these a bit loose (they are informal anyway, after all) and do the work of tightening things up when the times comes to translate it all into Coq. Reduction: << 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 >> Again, these rules are a bit informal. For example, the first rule is intended to be read "if [ti] is the leftmost field that is not a value and if [ti] steps to [ti'], then the whole record steps..." In the last rule, the intention is that there should only be one field called i, and that all the other fields must contain values. Typing: << Gamma |- t1 : T1 ... Gamma |- tn : Tn -------------------------------------------------- (T_Rcd) Gamma |- {i1=t1, ..., in=tn} : {i1:T1, ..., in:Tn} Gamma |- t : {..., i:Ti, ...} ----------------------------- (T_Proj) Gamma |- t.i : Ti >> *) (** *** Lists *) (** The typing features we have seen can be classified into _base types_ like [Bool] and [Unit], and _type constructors_ like [->] and [*] that build new types from old ones. Another useful type constructor is [list]. For every type [T], the type [list T] describes finite-length lists whose elements are drawn from [T]. Below we give the syntax, semantics, and typing rules for lists. Except for the fact that explicit type annotations are mandatory on nil and cannot appear on cons, these lists are essentially identical to those we defined in Coq. We use [case] (a very simplified form of [match]) to destruct lists, to avoid dealing with questions like "what is the [head] of the empty list?" While we say that [cons v1 v2] is a value, we only mean that when [v2] is also a list -- we'll have to enforce this in the formal definition of value. *) (** Syntax: << t ::= Terms: | nil T | cons t t | case t of nil -> t | x::x -> t v ::= Values: | ... | nil T nil value | cons v v cons value T ::= Types: | list T | ... >> Reduction: << t1 ~~> t1' -------------------------- (ST_Cons1) cons t1 t2 ~~> cons t1' t2 t2 ~~> t2' -------------------------- (ST_Cons2) cons v1 t2 ~~> cons v1 t2' t1 ~~> t1' (ST_Case1) ---------------------------------------------------------------------------- (case t1 of nil -> t2 | h::t -> t3) ~~> (case t1' of nil -> t2 | h::t -> t3) --------------------------------------------- (ST_CaseNil) (case nil T of nil -> t2 | h::t -> t3) ~~> t2 (ST_CaseCons) --------------------------------------------------------------- (case (cons vh vt) of nil -> t2 | h::t -> t3) ~~> [vh/h,vt/t]t3 >> Typing: << ----------------------- (T_Nil) Gamma |- nil T : list T Gamma |- t1 : T Gamma |- t2 : list T ----------------------------------------- (T_Cons) Gamma |- cons t1 t2: list T Gamma |- t1 : list T1 Gamma |- t2 : T Gamma, h:T1, t:list T1 |- t3 : T ------------------------------------------------ (T_Case) Gamma |- (case t1 of nil -> t2 | h::t -> t3) : T >> *) (** *** General recursion *) (** Another facility found in most programming languages (including Coq) is the ability to define recursive functions. For example, we might like to be able to define the factorial function like this: << fact = \x:nat. if x=0 then 1 else x * (fact (pred x))) >> But this would be require quite a bit of work to formalize: we'd have to introduce a notion of "function definitions" and carry around an "environment" of such definitions in the definition of the [step] relation. Here is another way that is straightforward to formalize: instead of writing recursive definitions where the right-hand side can contain the identifier being defined, we can define a _fixed-point operator_ that performs the "unfolding" of the recursive definition in the right-hand side lazily during reduction. << fact = fix (\f:nat->nat. \x:nat. if x=0 then 1 else x * (f (pred x))) >> The intuition is that the higher-order function [f] passed to [fix] is a _generator_ for the [fact] function: if [f] is applied to a function that approximates the desired behavior of [fact] up to some number [n] (that is, a function that returns correct results on inputs less than or equal to [n]), then it returns a better approximation to [fact]---a function that returns correct results for inputs up to [n+1]. Applying [fix] to this generator returns its fixed point---a function that gives the desired behavior for all inputs [n]. Syntax: << t ::= Terms: | ... | fix t fixed-point operator >> Reduction: << t1 ~~> t1' ------------------ (ST_Fix1) fix t1 ~~> fix t1' ------------------------------------------- (ST_FixAbs) fix (\x:T1.t2) ~~> [(fix(\x:T1.t2)) / x] t2 >> Typing: << Gamma |- t1 : T1->T1 -------------------- (T_Fix) Gamma |- fix t1 : T1 >> *) (** **** Exercise: 1 star (halve_fix) *) (** Translate this recursive definition into one using [fix]: << halve = \x:nat. if x=0 then 0 else if (pred x)=0 then 0 else 1 + (halve (pred (pred x)))) >> (* FILL IN HERE *) [] *) (** **** Exercise: 1 star (fact_steps) *) (** Write down the sequence of steps that the term [fact 1] goes through to reduce to a normal form (assuming the usual reduction rules for arithmetic operations). (* FILL IN HERE *) [] *) (* ###################################################################### *) (** * Formalizing the extensions *) (** **** Exercise: 5 stars (STLC_extensions) *) (** The rest of the file formalizes just the most interesting extension, records. Formalizing the others is left to you. We've provided the necessary extensions to the syntax of terms and types, and we've included a few examples that you can test your definitions with to make sure they are working as expected. You'll fill in the rest of the definitions and extend all the proofs accordingly. (A good strategy is to work on the extensions one at a time, in multiple passes, rather than trying to work through the file from start to finish in a single pass.) *) Module STLCExtended. (* ###################################################################### *) (** *** Syntax and operational semantics *) (** The most obvious way to formalize the syntax of record types would be this: *) Module FirstTry. Definition alist (X : Type) := list (id * X). Inductive ty : Type := | ty_base : id -> ty | ty_arrow : ty -> ty -> ty | ty_rcd : (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 [ty_rcd] 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. *) (* Yields: [[ ty_ind : forall P : ty -> Prop, (forall i : id, P (ty_base i)) -> (forall t : ty, P t -> forall t0 : ty, P t0 -> P (ty_arrow t t0)) -> (forall a : alist ty, P (ty_rcd 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. (Since this is the final definition that we'll use for the rest of the chapter, we also include constructors for and pairs lists and a base type of numbers.) *) Inductive ty : Type := | ty_base : id -> ty | ty_arrow : ty -> ty -> ty | ty_pair : ty -> ty -> ty | ty_list : ty -> ty | ty_nat : ty | ty_rnil : ty | ty_rcons : id -> ty -> ty -> ty. Tactic Notation "ty_cases" tactic(first) tactic(c) := first; [ c "ty_base" | c "ty_arrow" | c "ty_pair" | c "ty_list" | c "ty_nat" | c "ty_rnil" | c "ty_rcons" ]. (** Similarly, at the level of terms, we have constructors [tm_rnil] -- the empty record -- and [tm_rcons], which adds a single field to the front of a list of fields. *) Inductive tm : Type := | tm_var : id -> tm | tm_app : tm -> tm -> tm | tm_abs : id -> ty -> tm -> tm | tm_proj : tm -> id -> tm (* pairs *) | tm_pair : tm -> tm -> tm | tm_fst : tm -> tm | tm_snd : tm -> tm (* lists *) | tm_nil : ty -> tm | tm_cons : tm -> tm -> tm | tm_case : tm -> tm -> id -> id -> tm -> tm (* i.e., [case t1 of | nil -> t2 | x::y -> t3] *) (* numbers *) | tm_nat : nat -> tm | tm_succ : tm -> tm | tm_pred : tm -> tm | tm_mult : tm -> tm -> tm | tm_if0 : tm -> tm -> tm -> tm (* let *) | tm_let : id -> tm -> tm -> tm (* i.e., [let x = t1 in t2] *) (* fix *) | tm_fix : tm -> tm (* records *) | tm_rnil : tm | tm_rcons : id -> tm -> tm -> tm. Tactic Notation "tm_cases" tactic(first) tactic(c) := first; [ c "tm_var" | c "tm_app" | c "tm_abs" | c "tm_proj" | c "tm_pair" | c "tm_fst" | c "tm_snd" | c "tm_nil" | c "tm_cons" | c "tm_case" | c "tm_nat" | c "tm_succ" | c "tm_pred" | c "tm_mult" | c "tm_if0" | c "tm_let" | c "tm_fix" | c "tm_rnil" | c "tm_rcons" ]. (** Some variables, for examples... *) Notation a := (Id 0). Notation f := (Id 1). Notation g := (Id 2). Notation l := (Id 3). Notation A := (ty_base (Id 4)). Notation B := (ty_base (Id 5)). Notation k := (Id 6). Notation i1 := (Id 7). Notation i2 := (Id 8). (** [{ i1:A }] *) (* Check (ty_rcons i1 A ty_rnil). *) (** [{ i1:A->B, i2:A }] *) (* Check (ty_rcons i1 (ty_arrow A B) (ty_rcons i2 A ty_rnil)). *) (* ###################################################################### *) (** *** Well-formedness *) (** Generalizing our abstract syntax for records (from lists to the nil/cons presentation) introduces the possibility of writing strange types like this: *) Definition weird_type := ty_rcons X ty_nat ty_nat. (** 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 either [ty_rnil] or [ty_rcons]. *) Inductive record_ty : ty -> Prop := | rty_nil : record_ty ty_rnil | rty_cons : forall i T1 T2, record_ty (ty_rcons i T1 T2). (** Similarly, a term is a record term if it is built with [tm_rnil] or [tm_rcons] *) Inductive record_tm : tm -> Prop := | rtm_nil : record_tm tm_rnil | rtm_cons : forall i t1 t2, record_tm (tm_rcons i t1 t2). (** Note that [record_ty] and [record_tm] are not recursive -- they just checkw the outermost constructor. The [well_formed_ty] predicate, 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 [ty_rcons]) is a record. Of course, we should also be concerned about ill-formed terms, 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 := | wfty_base : forall i, well_formed_ty (ty_base i) | wfty_arrow : forall T1 T2, well_formed_ty T1 -> well_formed_ty T2 -> well_formed_ty (ty_arrow T1 T2) | wfty_pair : forall T1 T2, well_formed_ty T1 -> well_formed_ty T2 -> well_formed_ty (ty_pair T1 T2) | wfty_list : forall T1, well_formed_ty T1 -> well_formed_ty (ty_list T1) | wfty_nat : well_formed_ty ty_nat | wfty_rnil : well_formed_ty ty_rnil | wfty_rcons : forall i T1 T2, well_formed_ty T1 -> well_formed_ty T2 -> record_ty T2 -> well_formed_ty (ty_rcons i T1 T2). Hint Constructors record_ty record_tm well_formed_ty. (* ###################################################################### *) (** *** Substitution *) Fixpoint subst (x:id) (s:tm) (t:tm) {struct t} : tm := match t with | tm_var y => if beq_id x y then s else t | tm_abs y T t1 => tm_abs y T (if beq_id x y then t1 else (subst x s t1)) | tm_app t1 t2 => tm_app (subst x s t1) (subst x s t2) | tm_proj t1 i => tm_proj (subst x s t1) i | tm_rnil => tm_rnil | tm_rcons i t1 tr1 => tm_rcons i (subst x s t1) (subst x s tr1) (* FILL IN HERE *) | _ => t (* ... and delete this line *) end. (* ###################################################################### *) (** *** Reduction *) (** Next we define the valuesof our language. A record is a value if all of its fields are. *) Inductive value : tm -> Prop := | v_abs : forall x T11 t12, value (tm_abs x T11 t12) (* FILL IN HERE *) | v_rnil : value tm_rnil | v_rcons : forall i v1 vr, value v1 -> value vr -> value (tm_rcons i v1 vr). Hint Constructors value. (** Utility functions for extracting one field from record type or term *) Fixpoint ty_lookup (i:id) (Tr:ty) {struct Tr} : option ty := match Tr with | ty_rcons i' T Tr' => if beq_id i i' then Some T else ty_lookup i Tr' | _ => None end. Fixpoint tm_lookup (i:id) (tr:tm) {struct tr} : option tm := match tr with | tm_rcons i' t tr' => if beq_id i i' then Some t else tm_lookup 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 : forall x T11 t12 v2, value v2 -> (tm_app (tm_abs x T11 t12) v2) ~~> (subst x v2 t12) | ST_App1 : forall t1 t1' t2, t1 ~~> t1' -> (tm_app t1 t2) ~~> (tm_app t1' t2) | ST_App2 : forall v1 t2 t2', value v1 -> t2 ~~> t2' -> (tm_app v1 t2) ~~> (tm_app v1 t2') | ST_Proj1 : forall t1 t1' i, t1 ~~> t1' -> (tm_proj t1 i) ~~> (tm_proj t1' i) | ST_ProjRcd : forall tr i vi, value tr -> tm_lookup i tr = Some vi -> (tm_proj tr i) ~~> vi (* FILL IN HERE *) | ST_Rcd_Head : forall i t1 t1' tr2, t1 ~~> t1' -> (tm_rcons i t1 tr2) ~~> (tm_rcons i t1' tr2) | ST_Rcd_Tail : forall i v1 tr2 tr2', value v1 -> tr2 ~~> tr2' -> (tm_rcons i v1 tr2) ~~> (tm_rcons i v1 tr2') where "t1 '~~>' t2" := (step t1 t2). Tactic Notation "step_cases" tactic(first) tactic(c) := first; [ c "ST_AppAbs" | c "ST_App1" | c "ST_App2" | c "ST_Proj1" | c "ST_ProjRcd" | (* FILL IN HERE *) c "ST_Rcd_Head" | c "ST_Rcd_Tail" ]. Notation stepmany := (refl_step_closure step). Notation "t1 '~~>*' t2" := (stepmany t1 t2) (at level 40). Hint Constructors step. (* ###################################################################### *) (** *** Typing *) (* Standard definitions for contexts *) Definition context := id -> (option ty). Definition empty : context := (fun _ => None). Definition extend (Gamma : context) (x:id) (T : ty) := fun x' => if beq_id x x' then Some T else Gamma x'. (** 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 Gamma 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 [tm_nil] case. *) Inductive has_type : context -> tm -> ty -> Prop := (* Typing rules for proper terms *) | T_Var : forall Gamma x T, Gamma x = Some T -> well_formed_ty T -> has_type Gamma (tm_var x) T | T_Abs : forall Gamma x T11 T12 t12, well_formed_ty T11 -> has_type (extend Gamma x T11) t12 T12 -> has_type Gamma (tm_abs x T11 t12) (ty_arrow T11 T12) | T_App : forall T1 T2 Gamma t1 t2, has_type Gamma t1 (ty_arrow T1 T2) -> has_type Gamma t2 T1 -> has_type Gamma (tm_app t1 t2) T2 | T_Proj : forall Gamma i t Ti Tr, has_type Gamma t Tr -> ty_lookup i Tr = Some Ti -> has_type Gamma (tm_proj t i) Ti (* FILL IN HERE *) (* Typing rules for record terms *) | T_RNil : forall Gamma, has_type Gamma tm_rnil ty_rnil | T_RCons : forall Gamma i t T tr Tr, has_type Gamma t T -> has_type Gamma tr Tr -> record_ty Tr -> record_tm tr -> has_type Gamma (tm_rcons i t tr) (ty_rcons i T Tr). Hint Constructors has_type. Tactic Notation "has_type_cases" tactic(first) tactic(c) := first; [ c "T_Var" | c "T_Abs" | c "T_App" | c "T_Proj" | (* FILL IN HERE *) c "T_RNil" | c "T_RCons" ]. (* ###################################################################### *) (** ** Examples *) (** **** Exercise: 2 stars (examples) *) (** Finish the proofs. *) (** << fact := fix (\f:nat->nat. \a:nat. if a=0 then 1 else a * (f (pred a))) >> *) Definition fact := tm_fix (tm_abs f (ty_arrow ty_nat ty_nat) (tm_abs a ty_nat (tm_if0 (tm_var a) (tm_nat 1) (tm_mult (tm_var a) (tm_app (tm_var f) (tm_pred (tm_var a))))))). (** Note that you may be able to type check fact but still have some rules wrong! *) Example fact_typechecks : has_type empty fact (ty_arrow ty_nat ty_nat). Proof with auto. (* FILL IN HERE *) Admitted. Example fact_example: (tm_app fact (tm_nat 1)) ~~>* (tm_nat 1). Proof. (* FILL IN HERE *) Admitted. (* map := \g:nat->nat. fix (\f:[nat]->[nat]. \l:[nat]. case l of | [] -> [] | x::l -> (g x)::(f l)) *) Definition map := tm_abs g (ty_arrow ty_nat ty_nat) (tm_fix (tm_abs f (ty_arrow (ty_list ty_nat) (ty_list ty_nat)) (tm_abs l (ty_list ty_nat) (tm_case (tm_var l) (tm_nil ty_nat) a l (tm_cons (tm_app (tm_var g) (tm_var a)) (tm_app (tm_var f) (tm_var l))))))). Example map_typechecks : has_type empty map (ty_arrow (ty_arrow ty_nat ty_nat) (ty_arrow (ty_list ty_nat) (ty_list ty_nat))). Proof with auto. (* FILL IN HERE *) Admitted. Example map_example : tm_app (tm_app map (tm_abs a ty_nat (tm_succ (tm_var a)))) (tm_cons (tm_nat 1) (tm_cons (tm_nat 2) (tm_nil ty_nat))) ~~>* (tm_cons (tm_nat 2) (tm_cons (tm_nat 3) (tm_nil ty_nat))). Proof with auto. (* FILL IN HERE *) Admitted. (** [] *) Example typing_example : forall y, has_type (extend empty y A) (tm_app (tm_abs a (ty_rcons k A ty_rnil) (tm_proj (tm_var a) k)) (tm_rcons k (tm_var y) tm_rnil)) A. Proof with auto. intros y. apply T_App with (T1:= ty_rcons k A ty_rnil). apply T_Abs... apply T_Proj with (ty_rcons k A ty_rnil). apply T_Var... reflexivity. apply T_RCons... apply T_Var... unfold extend. rewrite <- beq_id_refl... Qed. (** Feel free to use Coq's automation features in this proof. However, if you are not confident about how the type system works, you may want to carry out the proof first using the basic features ([apply] instead of [eapply], in particular) and then perhaps compress it using automation. *) Lemma typing_example_2 : has_type empty (tm_app (tm_abs a (ty_rcons i1 (ty_arrow A A) (ty_rcons i2 (ty_arrow B B) ty_rnil)) (tm_proj (tm_var a) i2)) (tm_rcons i1 (tm_abs a A (tm_var a)) (tm_rcons i2 (tm_abs a B (tm_var a)) tm_rnil))) (ty_arrow 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 : ~ exists T, has_type (extend empty a (ty_rcons i2 (ty_arrow A A) ty_rnil)) (tm_rcons i1 (tm_abs a B (tm_var a)) (tm_var a)) T. Proof. (* FILL IN HERE *) Admitted. Example typing_nonexample_2 : forall y, ~ exists T, has_type (extend empty y A) (tm_app (tm_abs a (ty_rcons i1 A ty_rnil) (tm_proj (tm_var a) i1)) (tm_rcons i1 (tm_var y) (tm_rcons i2 (tm_var y) tm_rnil))) T. Proof. (* FILL IN HERE *) Admitted. (* ###################################################################### *) (** ** Properties of typing *) (** The proofs of progress and preservation for this system are essentially the same (though of course somewhat longer!) as for the pure simply typed lambda-calculus. The main change is the addition of some technical lemmas involving records. *) (* ###################################################################### *) (** *** Well-formedness *) Lemma wf_rcd_lookup : forall i T Ti, well_formed_ty T -> ty_lookup i T = Some Ti -> well_formed_ty Ti. Proof with eauto. intros i T. (ty_cases (induction T) Case); intros; try solve by inversion. Case "ty_rcons". inversion H. subst. unfold ty_lookup in H0. remember (beq_id i i0) as b. destruct b; subst... inversion H0. subst... Qed. Lemma step_preserves_record_tm : forall 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 : forall Gamma t T, has_type Gamma t T -> well_formed_ty T. Proof with eauto. intros Gamma t T Htyp. (has_type_cases (induction Htyp) Case)... Case "T_App". inversion IHHtyp1... Case "T_Proj". eapply wf_rcd_lookup... (* FILL IN HERE *) Qed. (* ###################################################################### *) (** *** Field lookup *) (** Here is an informal proof of the theorem below. *) (** Lemma: If [empty |- v : T] and [ty_lookup i T] returns [Some Ti], then [tm_lookup i v] returns [Some ti] for some term [ti] such that [has_type empty ti Ti]. Proof: By induction on the typing derivation [Htyp]. Since [ty_lookup i T = Some Ti], [T] must be a record type, this and the fact that [v] is a value eliminate most cases by inspection, leaving only the [T_RCons] case. If the last step in the typing derivation is by [T_RCons], then [t = tm_rcons i0 t tr] and [T = ty_rcons i0 T Tr] for some [i0], [t], [tr], [T] and [Tr]. This leaves two possiblities to consider - either [i0 = i] or not. - If [i = i0], then since [ty_lookup i (ty_rcons 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 [[ ty_lookup i T = ty_lookup i Tr ]] and [[ tm_lookup i t = tm_lookup i tr, ]] so the result follows from the induction hypothesis. [] *) Lemma lookup_field_in_value : forall v T i Ti, value v -> has_type empty v T -> ty_lookup i T = Some Ti -> exists ti, tm_lookup i v = Some ti /\ has_type empty ti Ti. Proof with eauto. intros v T i Ti Hval Htyp Hget. remember empty as Gamma. (has_type_cases (induction Htyp) Case); subst; try solve by inversion... Case "T_RCons". simpl in Hget. simpl. destruct (beq_id i i0). SCase "i is first". simpl. inversion Hget. subst. exists t... SCase "get tail". destruct IHHtyp2 as [vi [Hgeti Htypi]]... inversion Hval... Qed. (* ###################################################################### *) (** *** Progress *) Theorem progress : forall t T, has_type empty t T -> value t \/ exists 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 as Gamma. generalize dependent HeqGamma. (has_type_cases (induction Ht) Case); intros HeqGamma; subst. Case "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. Case "T_Abs". (* If the [T_Abs] rule was the last used, then [t = tm_abs x T11 t12], which is a value. *) left... Case "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... SCase "t1 is a value". destruct IHHt2; subst... SSCase "t2 is a value". (* If both [t1] and [t2] are values, then we know that [t1 = tm_abs x T11 t12], since abstractions are the only values that can have an arrow type. But [(tm_abs x T11 t12) t2 ~~> subst x t2 t12] by [ST_AppAbs]. *) inversion H; subst; try (solve by inversion). exists (subst x t2 t12)... SSCase "t2 steps". (* If [t1] is a value and [t2 ~~> t2'], then [t1 t2 ~~> t1 t2'] by [ST_App2]. *) destruct H0 as [t2' Hstp]. exists (tm_app t1 t2')... SCase "t1 steps". (* Finally, If [t1 ~~> t1'], then [t1 t2 ~~> t1' t2] by [ST_App1]. *) destruct H as [t1' Hstp]. exists (tm_app t1' t2)... Case "T_Proj". (* If the last rule in the given derivation is [T_Proj], then [t = tm_proj t i] and [empty |- t : (ty_rcd Tr)] By the IH, [t] either is a value or takes a step. *) right. destruct IHHt... SCase "rcd is value". (* If [t] is a value, then we may use lemma [lookup_field_in_value] to show [tm_lookup i t = Some ti] for some [ti] which gives us [tm_proj i t ~~> ti] by [ST_ProjRcd] *) destruct (lookup_field_in_value _ _ _ _ H0 Ht H) as [ti [Hlkup _]]. exists ti... SCase "rcd_steps". (* On the other hand, if [t ~~> t'], then [tm_proj t i ~~> tm_proj t' i] by [ST_Proj1]. *) destruct H0 as [t' Hstp]. exists (tm_proj t' i)... (* FILL IN HERE *) Case "T_RNil". (* If the last rule in the given derivation is [T_RNil], then [t = tm_rnil], which is a value. *) left... Case "T_RCons". (* If the last rule is [T_RCons], then [t = tm_rcons 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... SCase "head is a value". destruct IHHt2; try reflexivity. SSCase "tail is a value". (* If [t] and [tr] are both values, then [tm_rcons i t tr] is a value as well. *) left... SSCase "tail steps". (* If [t] is a value and [tr ~~> tr'], then [tm_rcons i t tr ~~> tm_rcons i t tr'] by [ST_Rcd_Tail]. *) right. destruct H2 as [tr' Hstp]. exists (tm_rcons i t tr')... SCase "head steps". (* If [t ~~> t'], then [tm_rcons i t tr ~~> tm_rcons i t' tr] by [ST_Rcd_Head]. *) right. destruct H1 as [t' Hstp]. exists (tm_rcons i t' tr)... Qed. (* ###################################################################### *) (** *** Context invariance *) Inductive appears_free_in : id -> tm -> Prop := | afi_var : forall x, appears_free_in x (tm_var x) | afi_app1 : forall x t1 t2, appears_free_in x t1 -> appears_free_in x (tm_app t1 t2) | afi_app2 : forall x t1 t2, appears_free_in x t2 -> appears_free_in x (tm_app t1 t2) | afi_abs : forall x y T11 t12, y <> x -> appears_free_in x t12 -> appears_free_in x (tm_abs y T11 t12) | afi_proj : forall x t i, appears_free_in x t -> appears_free_in x (tm_proj t i) (* FILL IN HERE *) | afi_rhead : forall x i ti tr, appears_free_in x ti -> appears_free_in x (tm_rcons i ti tr) | afi_rtail : forall x i ti tr, appears_free_in x tr -> appears_free_in x (tm_rcons i ti tr). Hint Constructors appears_free_in. Lemma context_invariance : forall Gamma Gamma' t S, has_type Gamma t S -> (forall x, appears_free_in x t -> Gamma x = Gamma' x) -> has_type Gamma' t S. Proof with eauto. intros. generalize dependent Gamma'. (has_type_cases (induction H) Case); intros Gamma' Heqv... Case "T_Var". apply T_Var... rewrite <- Heqv... Case "T_Abs". apply T_Abs... apply IHhas_type. intros y Hafi. unfold extend. remember (beq_id x y) as e. destruct e... Case "T_App". apply T_App with T1... (* FILL IN HERE *) Case "T_RCons". apply T_RCons... Qed. Lemma free_in_context : forall x t T Gamma, appears_free_in x t -> has_type Gamma t T -> exists T', Gamma x = Some T'. Proof with eauto. intros x t T Gamma Hafi Htyp. (has_type_cases (induction Htyp) Case); inversion Hafi; subst... Case "T_Abs". destruct IHHtyp as [T' Hctx]... exists T'. unfold extend in Hctx. apply not_eq_beq_id_false in H3. rewrite H3 in Hctx... (* FILL IN HERE *) Qed. (* ###################################################################### *) (** *** Preservation *) Lemma substitution_preserves_typing : forall Gamma x U v t S, has_type (extend Gamma x U) t S -> has_type empty v U -> has_type Gamma (subst x v t) S. Proof with eauto. (* Theorem: If Gamma,x:U |- t : S and empty |- v : U, then Gamma |- (subst x v t) S. *) intros Gamma x U v t S Htypt Htypv. generalize dependent Gamma. generalize dependent S. (* Proof: By induction on the term t. Most cases follow directly from the IH, with the exception of tm_var, tm_abs, tm_rcons. The former aren't automatic because we must reason about how the variables interact. In the case of tm_rcons, we must do a little extra work to show that substituting into a term doesn't change whether it is a record term. *) (tm_cases (induction t) Case); intros S Gamma Htypt; simpl; inversion Htypt; subst... Case "tm_var". simpl. rename i into y. (* If t = y, we know that [empty |- v : U] and [Gamma,x:U |- y : S] and, by inversion, [extend Gamma x U y = Some S]. We want to show that [Gamma |- subst x v y : S]. There are two cases to consider: either [x=y] or [x<>y]. *) remember (beq_id x y) as e. destruct e. SCase "x=y". (* If [x = y], then we know that [U = S], and that [subst x v y = v]. So what we really must show is that if [empty |- v : U] then [Gamma |- v : U]. We have already proven a more general version of this theorem, called context invariance. *) apply beq_id_eq in Heqe. subst. unfold extend in H0. rewrite <- beq_id_refl in H0. inversion H0; subst. clear H0. eapply context_invariance... intros x Hcontra. destruct (free_in_context _ _ S empty Hcontra) as [T' HT']... inversion HT'. SCase "x<>y". (* If [x <> y], then [Gamma y = Some S] and the substitution has no effect. We can show that [Gamma |- y : S] by [T_Var]. *) apply T_Var... unfold extend in H0. rewrite <- Heqe in H0... Case "tm_abs". rename i into y. rename t into T11. (* If [t = tm_abs y T11 t0], then we know that [Gamma,x:U |- tm_abs y T11 t0 : T11->T12] [Gamma,x:U,y:T11 |- t0 : T12] [empty |- v : U] As our IH, we know that forall S Gamma, [Gamma,x:U |- t0 : S -> Gamma |- subst x v t0 S]. We can calculate that subst x v t = tm_abs y T11 (if beq_id x y then t0 else subst x v t0) And we must show that [Gamma |- subst x v t : T11->T12]. We know we will do so using [T_Abs], so it remains to be shown that: [Gamma,y:T11 |- if beq_id x y then t0 else subst x v t0 : T12] We consider two cases: [x = y] and [x <> y]. *) apply T_Abs... remember (beq_id x y) as e. destruct e. SCase "x=y". (* If [x = y], then the substitution has no effect. Context invariance shows that [Gamma,y:U,y:T11] and [Gamma,y:T11] are equivalent. Since the former context shows that [t0 : T12], so does the latter. *) eapply context_invariance... apply beq_id_eq in Heqe. subst. intros x Hafi. unfold extend. destruct (beq_id y x)... SCase "x<>y". (* If [x <> y], then the IH and context invariance allow us to show that [Gamma,x:U,y:T11 |- t0 : T12] => [Gamma,y:T11,x:U |- t0 : T12] => [Gamma,y:T11 |- subst x v t0 : T12] *) apply IHt. eapply context_invariance... intros z Hafi. unfold extend. remember (beq_id y z) as e0. destruct e0... apply beq_id_eq in Heqe0. subst. rewrite <- Heqe... (* FILL IN HERE *) Case "tm_rcons". apply T_RCons... inversion H7; subst; simpl... Qed. Theorem preservation : forall t t' T, has_type empty t T -> t ~~> t' -> has_type 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 as Gamma. 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. *) (has_type_cases (induction HT) Case); intros t' HeqGamma HE; subst; inversion HE; subst... Case "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... SCase "ST_AppAbs". (* For the third case, suppose [t1 = tm_abs x T11 t12] and [t2 = v2]. We must show that [empty |- subst x v2 t12 : T2]. We know by assumption that [empty |- tm_abs 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... Case "T_Proj". (* If the last rule was [T_Proj], then [t = tm_proj 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 [has_type empty t Tr] and [ty_lookup 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... (* FILL IN HERE *) Case "T_RCons". (* If the last rule was [T_RCons], then [t = tm_rcons 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. (** [] *) End STLCExtended.