# Case study: simply-typed lambda-calculus¶

module STLC

We now look at a larger case study: proving the soundness of a type-checker for the simply-typed \(\lambda\)-calculus (STLC). If you’re not familiar with STLC, you can have a look at the Software Foundations book for a gentle introduction given by the textual explanations (you can ignore the Coq parts there). The formalization and proof here closely follows the one in Software Foundations. Our proofs are, however, shorter and much more readable than Coq proofs.

## Syntax¶

We represent STLC types by the F* inductive datatype `ty`

.

type ty = | TBool : ty | TArrow : tin:ty -> tout:ty -> ty type var = int

We consider Booleans as the only base type (`TBool`

). Function types
are represented by the `TArrow`

constructor taking two type arguments.
For instance we write `TArrow TBool TBool`

for the type of functions
taking a Boolean argument and returning a Boolean result. This would be
written as `bool -> bool`

in F* syntax, and
\(\mathsf{bool} \to \mathsf{bool}\) in paper notation.

We represent the expressions of STLC by the datatype `exp`

.

type exp = | EVar : v:var -> exp | EApp : fn:exp -> arg:exp -> exp | EAbs : v:var -> vty:ty -> body:exp -> exp | ETrue : exp | EFalse : exp | EIf : test:exp -> btrue:exp -> bfalse:exp -> exp

Variables are represented as integer “names” decorated by the
constructor `EVar`

. Variables are “bound” by lambda abstractions
(`EAbs`

). For instance the identity function on Booleans is written
`EAbs 0 TBool (EVar 0)`

. In paper notation one would write this
function as \((\lambda x:\mathsf{bool}.~x)\). The type annotation on
the argument (`TBool`

) allows for very simple type-checking. We are
not considering type inference here, to keep things simple. The
expression that applies the identity function to the `ETrue`

constant
is written

let stlc_app_id_to_true = EApp (EAbs 0 TBool (EVar 0)) ETrue

(in paper notation \((\lambda x:\mathsf{bool}.~x)~\mathsf{true}\)).

The language also has a conditional construct (if-then-else). For instance, the Boolean “not” function can be written as

let stlc_not = EAbs 0 TBool (EIf (EVar 0) EFalse ETrue)

(in paper notation \(\lambda x:\mathsf{bool}.~\mathsf{if }~x~\mathsf{ then~false~else~true}\)).

## Operational semantics¶

We define a standard small-step call-by-value interpreter for STLC. The
final result of successfully evaluating an expression is called a
*value*. We postulate that functions and the Boolean constants are
values by defining `is_value`

, a boolean predicate on expressions (a
total function):

val is_value : exp -> Tot bool let is_value e = match e with | EAbs _ _ _ | ETrue | EFalse -> true | _ -> false

The `EAbs`

, `ETrue`

, and `EFalse`

cases share the same
right-hand-side (`true`

), which is a way to prevent duplication in
definitions.

In order to give a semantics to function applications we define a
function `subst x e e'`

that substitutes `x`

with `e`

in `e'`

:

val subst : int -> exp -> exp -> Tot exp let rec subst x e e' = match e' with | EVar x' -> if x = x' then e else e' | EAbs x' t e1 -> EAbs x' t (if x = x' then e1 else (subst x e e1)) | EApp e1 e2 -> EApp (subst x e e1) (subst x e e2) | ETrue -> ETrue | EFalse -> EFalse | EIf e1 e2 e3 -> EIf (subst x e e1) (subst x e e2) (subst x e e3)

We traverse the expression and when we reach a variable `(EVar x')`

we
check whether this is the variable `x`

we want to substitute, and if
it is we replace it by `e`

. For lambda abstractions `(EAbs x' t e1)`

we only substitute inside the body `e1`

if `x`

and `x'`

are
different; if they are the same we leave the body unchanged. The reason
for this is that the `x`

in `e1`

is bound by the abstraction: it is
a new, local name that just happens to be spelled the same as some
global name `x`

. The global `x`

is no longer accessible in this
scope, since it is shadowed by the local `x`

. The other cases are
straightforward.

Note for experts: Because we will only reduce closed expressions, where all variables are bound by previous lambdas, we will only ever substitute closed expressions`e`

, and this naive definition of substitution is good enough. Substitution would become trickier to define or the representation of variables would have to change if we were considering the case where`e`

, the expression replacing a variable in some other expression, may itself contain free variables.

Given the definition of values and of substitution we can now define a
small-step interpreter, as a function `step`

that takes an expression
`e`

and it either returns the expression to which `e`

reduces in a
single step, or it returns `None`

in case of an error (all errors in
this language are typing errors, and will be prevented statically by the
type system).

val step : exp -> Tot (option exp) let rec step e = match e with | EApp e1 e2 -> if is_value e1 then if is_value e2 then match e1 with | EAbs x t e' -> Some (subst x e2 e') | _ -> None else match (step e2) with | Some e2' -> Some (EApp e1 e2') | None -> None else (match (step e1) with | Some e1' -> Some (EApp e1' e2) | None -> None) | EIf e1 e2 e3 -> if is_value e1 then match e1 with | ETrue -> Some e2 | EFalse -> Some e3 | _ -> None else (match (step e1) with | Some e1' -> Some (EIf e1' e2 e3) | None -> None) | _ -> None

We execute an application expression `EApp e1 e2`

in multiple steps by
first reducing `e1`

to a value, then reducing `e2`

to a value
(following a *call-by-value* evaluation order), and if additionally
`e1`

is an abstraction `EAbs x t e'`

we continue by substituting
the formal argument `x`

by the actual argument `e2`

. If not we
signal a dynamic typing error (a non-functional value is applied to
arguments) by returning `None`

. For `EIf e1 e2 e3`

we first reduce
the guard `e1`

: if the guard reduces to `true`

then we continue with
`e2`

, if the guard reduces to `false`

we continue with `e3`

, and
if the guard reduces to something else (e.g. a function) we report a
dynamic typing error. The `None -> None`

cases simply propagate errors
to the top level.

let _ = assert (step (EApp (EAbs 0 TBool (EVar 0)) ETrue) = Some ETrue) let _ = assert (step (EApp ETrue ETrue) = None)

## Type-checker¶

In order to assign a type to a term, we need to know what assumptions we should make about the types of its free variables. So typing happens with respect to a typing environment—a mapping from the variables in scope to their types. We represent such partial maps as functions taking an integer variable name and returning an optional type:

type env = int -> Tot (option ty)

We start type-checking closed terms in the empty environment, i.e. initially no variables are in scope.

val empty : env let empty = fun _ -> None

When we move under a binder we extend the typing environment.

val extend : env -> int -> ty -> Tot env let extend g x t = fun x' -> if x = x' then Some t else g x'

For instance we type-check `EAbs x t e`

in typing environment `g`

by
first type-checking the body `e`

in the environment `extend g x t`

.

The type-checker is a total function taking an environment `g`

and an
expression `e`

and producing either the type of `e`

or `None`

if
`e`

is not well-typed.

val typing : env -> exp -> Tot (option ty) let rec typing g e = match e with | EVar x -> g x | EAbs x t e1 -> (match typing (extend g x t) e1 with | Some t' -> Some (TArrow t t') | None -> None) | EApp e1 e2 -> (match typing g e1, typing g e2 with | Some (TArrow t11 t12), Some t2 -> if t11 = t2 then Some t12 else None | _ , _ -> None) | ETrue -> Some TBool | EFalse -> Some TBool | EIf e1 e2 e3 -> (match typing g e1, typing g e2, typing g e3 with | Some TBool, Some t2, Some t3 -> if t2 = t3 then Some t2 else None | _ , _ , _ -> None)

Variables are simply looked up in the environment. For abstractions
`EAbs x t e1`

we type-check the body `e1`

under the environment
`extend g x t`

, as explained above. If that succeeds and produces a
type `t'`

, then the whole abstraction is given type `TArrow t t'`

.
For applications `EApp e1 e2`

we type-check `e1`

and `e2`

separately, and if `e1`

has a function type `TArrow t11 t12`

and
`e2`

has type `t11`

, then the whole application has type `t12`

.
`ETrue`

and `EFalse`

have type `TBool`

. For conditionals, we
require that the guard has type `TBool`

and the two branches have the
same type, which is also the type of the conditional.

## Soundness proof¶

We prove progress and preservation for STLC. The **progress** theorem
tells us that closed, well-typed terms do not produce (immediate)
dynamic typing errors: either a well-typed term is a value, or it can
take an evaluation step. The proof is a relatively straightforward
induction.

val progress : e:exp -> Lemma (requires (Some? (typing empty e))) (ensures (is_value e \/ (Some? (step e)))) let rec progress e = match e with | EApp e1 e2 -> progress e1; progress e2 | EIf e1 e2 e3 -> progress e1; progress e2; progress e3 | _ -> ()

Variables are not well-typed in the empty environment, so the theorem holds vacuously for variables. Boolean constants and abstractions are values, so the theorem holds trivially for these. All these simple cases are proved automatically by F*. For the remaining cases we need to use the induction hypothesis, but otherwise the proofs are fully automated. Under the hood F* and Z3 are doing quite a bit of work though.

In case `e = (EApp e1 e2)`

F* and Z3 automate the following intuitive
argument: We case split on the first instance of the induction
hypothesis `(is_value e1 \/ (Some? (step e1)))`

.

- If
`e1`

steps to`e1'`

then, by the definition of`step`

,`(EApp e1 e2)`

steps to`(EApp e1' e2)`

. - If
`e1`

is a value, we case split on the second induction hypothesis instance,`(is_value e2 \/ (Some? (step e2)))`

. - If
`e2`

steps to`e2'`

then`(EApp e1 e2)`

steps to`(EApp e1 e2')`

, since`e1`

is a value. - If
`e2`

is also a value, then we need to obtain that`e1`

has a function type and from this that it is an abstraction. Expression`e1`

has a function type because, by the definition of`typing`

, an application is well-typed only when the first expression is a function. The remaining step is usually done as a separate “canonical forms” lemma, stating that any value that has a function type is actually an abstraction. Z3 can prove this fact automatically from the definitions of`typing`

and`is_value`

.

The intuitive proof of the `EIf`

case is similar.

The **preservation** theorem (sometimes also called “subject reduction”)
states that when a well-typed expression takes a step, the result is a
well-typed expression of the same type. In order to show preservation we
need to prove a couple of auxiliary results for reasoning about
variables and substitution.

The case for function application has to reason about “beta reduction”
steps, i.e. substituting the formal argument of a function with an
actual value. To see that this step preserves typing, we need to know
that the substitution itself does. So we prove a **substitution** lemma,
stating that substituting a (closed) term `v`

for a variable `x`

in
an expression `e`

preserves the type of `e`

. The tricky cases in the
substitution proof are the ones for variables and for function
abstractions. In both cases, we discover that we need to take an
expression `e`

that has been shown to be well-typed in some context
`g`

and consider the same expression `e`

in a slightly different
context `g'`

. For this we prove a **context invariance** lemma,
showing that typing is preserved under “inessential changes” to the
context `g`

—in particular, changes that do not affect any of the free
variables of the expression. For this, we need a definition of the free
variables of an expression—i.e., the variables occurring in the
expression that are not bound by an abstraction.

A variable `x`

appears free in `e`

if `e`

contains some occurrence
of `x`

that is not under an abstraction labeled `x`

:

val appears_free_in : x:int -> e:exp -> Tot bool let rec appears_free_in x e = match e with | EVar y -> x = y | EApp e1 e2 -> appears_free_in x e1 || appears_free_in x e2 | EAbs y _ e1 -> x <> y && appears_free_in x e1 | EIf e1 e2 e3 -> appears_free_in x e1 || appears_free_in x e2 || appears_free_in x e3 | ETrue | EFalse -> false

We also need a technical lemma connecting free variables and typing
contexts. If a variable `x`

appears free in an expression `e`

, and
if we know that `e`

is well typed in context `g`

, then it must be
the case that `g`

assigns some type to `x`

.

val free_in_context : x:int -> e:exp -> g:env -> Lemma (requires (Some? (typing g e))) (ensures (appears_free_in x e ==> Some? (g x))) let rec free_in_context x e g = match e with | EVar _ | ETrue | EFalse -> () | EAbs y t e1 -> free_in_context x e1 (extend g y t) | EApp e1 e2 -> free_in_context x e1 g; free_in_context x e2 g | EIf e1 e2 e3 -> free_in_context x e1 g; free_in_context x e2 g; free_in_context x e3 g

The proof is a straightforward induction. As a corollary for
`g == empty`

we obtain that expressions typable in the empty
environment have no free variables.

val typable_empty_closed : x:int -> e:exp -> Lemma (requires (Some? (typing empty e))) (ensures (not(appears_free_in x e))) [SMTPat (appears_free_in x e)] let typable_empty_closed x e = free_in_context x e empty

The quantifier pattern `[SMTPat (appears_free_in x e)]`

signals to Z3
that it should consider applying this lemma when its context contains a
term of the form `appears_free_in`

Sometimes, we know that `typing g e = Some t`

, and we will need to
replace `g`

by an “equivalent” context `g'`

. We still need to define
formally when two environments are equivalent. A natural definition is
extensional equivalence of functions:

logic type equal (g1:env) (g2:env) = forall (x:int). g1 x = g2 x

According to this definition two environments are equivalent if have the
same domain and they map all variables in the domain to the same type.
We remark `equal`

in particular and logical formulas in general are
*types* in F*, thus the different syntax for this definition.

The context invariance lemma uses in fact a weaker variant of this
equivalence in which the two environments only need to agree on the
variables that appear free in an expression `e`

:

logic type equalE (e:exp) (g1:env) (g2:env) = forall (x:int). appears_free_in x e ==> g1 x = g2 x

The context invariance lemma is then easily proved by induction:

val context_invariance : e:exp -> g:env -> g':env -> Lemma (requires (equalE e g g')) (ensures (typing g e == typing g' e)) let rec context_invariance e g g' = match e with | EAbs x t e1 -> context_invariance e1 (extend g x t) (extend g' x t) | EApp e1 e2 -> context_invariance e1 g g'; context_invariance e2 g g' | EIf e1 e2 e3 -> context_invariance e1 g g'; context_invariance e2 g g'; context_invariance e3 g g' | _ -> ()

Because `equal`

is a stronger relation than `equalE`

we obtain the
same property for `equal`

:

val typing_extensional : g:env -> g':env -> e:exp -> Lemma (requires (equal g g')) (ensures (typing g e == typing g' e)) let typing_extensional g g' e = context_invariance e g g'

We can use these results to show the following substitution lemma:

val substitution_preserves_typing : x:int -> e:exp -> v:exp -> g:env -> Lemma (requires (Some? (typing empty v) /\ Some? (typing (extend g x (Some?.v (typing empty v))) e))) (ensures (Some? (typing empty v) /\ typing g (subst x v e) == typing (extend g x (Some?.v (typing empty v))) e)) let rec substitution_preserves_typing x e v g = let Some t_x = typing empty v in let gx = extend g x t_x in match e with | ETrue -> () | EFalse -> () | EVar y -> if x=y then context_invariance v empty g (* uses lemma typable_empty_closed *) else context_invariance e gx g | EApp e1 e2 -> substitution_preserves_typing x e1 v g; substitution_preserves_typing x e2 v g | EIf e1 e2 e3 -> substitution_preserves_typing x e1 v g; substitution_preserves_typing x e2 v g; substitution_preserves_typing x e3 v g | EAbs y t_y e1 -> let gxy = extend gx y t_y in let gy = extend g y t_y in if x=y then typing_extensional gxy gy e1 else (let gyx = extend gy x t_x in typing_extensional gxy gyx e1; substitution_preserves_typing x e1 v gy)

The proof proceeds by induction on the expression `e`

; we give the
intuition of the two most interesting cases:

Case

`e = EVar y`

Case

`x = y`

: We have`subst x v e = v`

and we already know that`typing empty v == Some t_x`

. However, what we need to show is`typing g v == Some t_x`

for some arbitrary environment`g`

. From the`typable_empty_closed`

lemma we obtain that`v`

contains no free variables, so we have`equalE v empty g`

. This allows us to apply the`context_invariance`

lemma to obtain that`typing empty v = typing g v`

and complete the proof of this case.Case

`x <> y`

We have`subst x v e = e`

and`typing gx e = Some t_e`

and need to show thattyping g e == Some t_e

We have that

`EquivE (EVar y) gx g`

since`x <> y`

so we can apply the`context_invariance`

lemma to conclude.Case

`e = EAbs y t_y e1`

: We have that`typing gxy e1 = Some t_e1`

, and need to show that`typing gy e1 == Some t_e1`

Case

`x = y`

We have`subst x v e = EAbs y t_y e1`

. Since`x = y`

the`x`

binder in`gxy`

is spurious (we have`equal gy gxy`

) and can apply the`typing_extensional`

lemma.Case

`x <> y`

We have`subst x v e = EAbs y t_y (subst x v e1)`

. Since`x <> y`

(and since we are in a simply typed calculus, not a dependently typed one) we can swap the`x`

and`y`

binding to show that`equal gxy xyx`

. By the`typing_extensional`

lemma we obtain that`typing gxy e1 == typing gyx e1`

. By the induction hypothesis we thus obtain thattyping gy (subst x v e1) == Some t_e1

and by the definition of

`typing`

we conclude that`typing g (EAbs y t_y (subst x v e)) = t_e`

.

We now have the tools we need to prove preservation: if a closed
expression `e`

has type `t`

and takes an evaluation step to `e'`

,
then `e'`

is also a closed expression with type `t`

. In other words,
the small-step evaluation relation preserves types.

val preservation : e:exp -> Lemma (requires (Some? (typing empty e) /\ Some? (step e) )) (ensures (Some? (step e) /\ typing empty (Some?.v (step e)) == typing empty e)) let rec preservation e = match e with | EApp e1 e2 -> if is_value e1 then (if is_value e2 then let EAbs x _ ebody = e1 in substitution_preserves_typing x ebody e2 empty else preservation e2) else preservation e1 | EIf e1 _ _ -> if not (is_value e1) then preservation e1

We only have two cases to consider, since only applications and
conditionals can take successful execution steps. The case for
`e = EIf e1 e2 e3`

is simple: either `e1`

is a value and thus the
conditional reduces to `e2`

or `e3`

which by the typing hypothesis
also have type `t`

, or `e1`

takes a successful step and we can apply
the induction hypothesis. We use the `Some?.v`

projector, which
requires F* to prove that indeed `e1`

can take a step; this is
immediate since we know that the whole conditional takes a step and we
know that `e1`

is not a value.

The case for `e = EApp e1 e2`

is a bit more complex. If `e1`

steps
or if `e1`

is a value and `e2`

steps then we just apply the
induction hypothesis. If both `e1`

and `e2`

are values it needs to
be the case that `e1`

is an abstraction `EAbs x targ ebody`

and
`step e = subst x e2 ebody`

. From the typing assumption we have
`typing (extend empty x tags) ebody = Some t`

and
`typing empty e2 = Some targ`

, so we can use the substitution lemma to
obtain that `typing empty (subst x e2 ebody) = Some t`

, which
concludes the proof.

## Exercises for STLC¶

Define a `typed_step`

step function that takes a well-typed expression
`e`

that is not a value and produces the expression to which `e`

steps. Give `typed_step`

the following strong type (basically this
type captures both progress and preservation):

val typed_step : e:exp{Some? (typing empty e) /\ not(is_value e)} -> Tot (e':exp{typing empty e' = typing empty e})

(Hint: the most direct solution to this exercise fits on one line)

let typed_step e = progress e; preservation e; Some?.v (step e)

To add pairs to this formal development we add the following to the definition of types, expressions, values, substitution, and step:

type tyP = (* {{{ 2 unchanged cases *) | TBoolP : tyP | TArrowP : tin:tyP -> tout:tyP -> tyP (* }}} *) | TPairP : tyP -> tyP -> tyP type expP = (* {{{ 6 unchanged cases *) | EVarP : v:var -> expP | EAppP : fn:expP -> arg:expP -> expP | EAbsP : v:var -> vty:tyP -> body:expP -> expP | ETrueP : expP | EFalseP : expP | EIfP : test:expP -> btrue:expP -> bfalse:expP -> expP (* }}} *) | EPairP : expP -> expP -> expP | EFstP : expP -> expP | ESndP : expP -> expP let rec is_valueP e = (* Note the extra let rec! *) match e with (* {{{ 3 unchanged cases *) | EAbsP _ _ _ | ETrueP | EFalseP -> true (* }}} *) | EPairP e1 e2 -> is_valueP e1 && is_valueP e2 | _ -> false let rec substP x e e' = match e' with (* {{{ 6 unchanged cases *) | EVarP x' -> if x = x' then e else e' | EAbsP x' t e1 -> EAbsP x' t (if x = x' then e1 else (substP x e e1)) | EAppP e1 e2 -> EAppP (substP x e e1) (substP x e e2) | ETrueP -> ETrueP | EFalseP -> EFalseP | EIfP e1 e2 e3 -> EIfP (substP x e e1) (substP x e e2) (substP x e e3) (* }}} *) | EPairP e1 e2 -> EPairP (substP x e e1) (substP x e e2) | EFstP e1 -> EFstP (substP x e e1) | ESndP e1 -> ESndP (substP x e e1) let rec stepP e = match e with (* {{{ 2 unchanged cases *) | EAppP e1 e2 -> if is_valueP e1 then if is_valueP e2 then match e1 with | EAbsP x t e' -> Some (substP x e2 e') | _ -> None else match (stepP e2) with | Some e2' -> Some (EAppP e1 e2') | None -> None else (match (stepP e1) with | Some e1' -> Some (EAppP e1' e2) | None -> None) | EIfP e1 e2 e3 -> if is_valueP e1 then match e1 with | ETrueP -> Some e2 | EFalseP -> Some e3 | _ -> None else (match (stepP e1) with | Some e1' -> Some (EIfP e1' e2 e3) | None -> None) (* }}} *) | EPairP e1 e2 -> if is_valueP e1 then if is_valueP e2 then None else (match (stepP e2) with | Some e2' -> Some (EPairP e1 e2') | None -> None) else (match (stepP e1) with | Some e1' -> Some (EPairP e1' e2) | None -> None) | EFstP e1 -> if is_valueP e1 then (match e1 with | EPairP v1 v2 -> Some v1 | _ -> None) else (match (stepP e1) with | Some e1' -> Some (EFstP e1') | None -> None) | ESndP e1 -> if is_valueP e1 then (match e1 with | EPairP v1 v2 -> Some v2 | _ -> None) else (match (stepP e1) with | Some e1' -> Some (ESndP e1') | None -> None) | _ -> None

Add cases to `typingP`

for the new constructs and fix all the proofs.

We extend the `typingP`

and `appears_free_inP`

functions with cases
for `EPairP`

, `EFstP`

, and `ESndP`

:

type envP = int -> Tot (option tyP) val emptyP : envP let emptyP = fun _ -> None

When we move under a binder we extend the typing environment.

val extendP : envP -> int -> tyP -> Tot envP let extendP g x t = fun x' -> if x = x' then Some t else g x' val typingP : envP -> expP -> Tot (option tyP) let rec typingP g e = match e with (* {{{ 6 unchanged cases *) | EVarP x -> g x | EAbsP x t e1 -> (match typingP (extendP g x t) e1 with | Some t' -> Some (TArrowP t t') | None -> None) | EAppP e1 e2 -> (match typingP g e1, typingP g e2 with | Some (TArrowP t11 t12), Some t2 -> if t11 = t2 then Some t12 else None | _ , _ -> None) | ETrueP -> Some TBoolP | EFalseP -> Some TBoolP | EIfP e1 e2 e3 -> (match typingP g e1, typingP g e2, typingP g e3 with | Some TBoolP, Some t2, Some t3 -> if t2 = t3 then Some t2 else None | _ , _ , _ -> None) (* }}} *) | EPairP e1 e2 -> (match typingP g e1, typingP g e2 with | Some t1, Some t2 -> Some (TPairP t1 t2) | _ , _ -> None) | EFstP e1 -> (match typingP g e1 with | Some (TPairP t1 t2) -> Some t1 | _ -> None) | ESndP e1 -> (match typingP g e1 with | Some (TPairP t1 t2) -> Some t2 | _ -> None) val appears_free_inP : x:int -> e:expP -> Tot bool let rec appears_free_inP x e = match e with (* {{{ 6 unchanged cases *) | EVarP y -> x = y | EAppP e1 e2 -> appears_free_inP x e1 || appears_free_inP x e2 | EAbsP y _ e1 -> x <> y && appears_free_inP x e1 | EIfP e1 e2 e3 -> appears_free_inP x e1 || appears_free_inP x e2 || appears_free_inP x e3 | ETrueP | EFalseP -> false (* }}} *) | EPairP e1 e2 -> appears_free_inP x e1 || appears_free_inP x e2 | EFstP e1 -> appears_free_inP x e1 | ESndP e1 -> appears_free_inP x e1

The proofs of the lemmas are also easy to extend by just calling the induction hypothesis:

val free_in_contextP : x:int -> e:expP -> g:envP -> Lemma (requires (Some? (typingP g e))) (ensures (appears_free_inP x e ==> Some? (g x))) let rec free_in_contextP x e g = match e with (* {{{ 6 unchanged cases *) | EVarP _ | ETrueP | EFalseP -> () | EAbsP y t e1 -> free_in_contextP x e1 (extendP g y t) | EAppP e1 e2 -> free_in_contextP x e1 g; free_in_contextP x e2 g | EIfP e1 e2 e3 -> free_in_contextP x e1 g; free_in_contextP x e2 g; free_in_contextP x e3 g (* }}} *) | EPairP e1 e2 -> free_in_contextP x e1 g; free_in_contextP x e2 g | EFstP e1 | ESndP e1 -> free_in_contextP x e1 g logic type equalEP (e:expP) (g1:envP) (g2:envP) = forall (x:int). appears_free_inP x e ==> g1 x = g2 x val context_invarianceP : e:expP -> g:envP -> g':envP -> Lemma (requires (equalEP e g g')) (ensures (typingP g e == typingP g' e)) let rec context_invarianceP e g g' = match e with (* {{{ 3 unchanged cases *) | EAbsP x t e1 -> context_invarianceP e1 (extendP g x t) (extendP g' x t) | EAppP e1 e2 -> context_invarianceP e1 g g'; context_invarianceP e2 g g' | EIfP e1 e2 e3 -> context_invarianceP e1 g g'; context_invarianceP e2 g g'; context_invarianceP e3 g g' (* }}} *) | EPairP e1 e2 -> context_invarianceP e1 g g'; context_invarianceP e2 g g' | EFstP e1 | ESndP e1 -> context_invarianceP e1 g g' | _ -> () (* {{{ similar definitions skipped *) logic type equalP (g1:envP) (g2:envP) = forall (x:int). g1 x = g2 x val typing_extensionalP : g:envP -> g':envP -> e:expP -> Lemma (requires (equalP g g')) (ensures (typingP g e == typingP g' e)) let typing_extensionalP g g' e = context_invarianceP e g g' val typable_empty_closedP : x:int -> e:expP -> Lemma (requires (Some? (typingP emptyP e))) (ensures (not(appears_free_inP x e))) [SMTPat (appears_free_inP x e)] let typable_empty_closedP x e = free_in_contextP x e emptyP (* }}} *) val substitution_preserves_typingP : x:int -> e:expP -> v:expP -> g:envP -> Lemma (requires (Some? (typingP emptyP v) /\ Some? (typingP (extendP g x (Some?.v (typingP emptyP v))) e))) (ensures (Some? (typingP emptyP v) /\ typingP g (substP x v e) == typingP (extendP g x (Some?.v (typingP emptyP v))) e)) let rec substitution_preserves_typingP x e v g = (* {{{ unchanged preamble skipped *) let Some t_x = typingP emptyP v in let gx = extendP g x t_x in match e with | ETrueP -> () | EFalseP -> () | EVarP y -> if x=y then context_invarianceP v emptyP g (* uses lemma typable_empty_closed *) else context_invarianceP e gx g | EAppP e1 e2 -> substitution_preserves_typingP x e1 v g; substitution_preserves_typingP x e2 v g | EIfP e1 e2 e3 -> substitution_preserves_typingP x e1 v g; substitution_preserves_typingP x e2 v g; substitution_preserves_typingP x e3 v g | EAbsP y t_y e1 -> let gxy = extendP gx y t_y in let gy = extendP g y t_y in if x=y then typing_extensionalP gxy gy e1 else (let gyx = extendP gy x t_x in typing_extensionalP gxy gyx e1; substitution_preserves_typingP x e1 v gy) (* }}} *) | EPairP e1 e2 -> (substitution_preserves_typingP x e1 v g; substitution_preserves_typingP x e2 v g) | EFstP e1 | ESndP e1 -> substitution_preserves_typingP x e1 v g | _ -> ()

As for the other cases, the preservation proof when `e = EPair e1 e2`

follows the structure of the `step`

function. If `e1`

is not a value
then it further evaluates, so we apply the induction hypothesis to
`e1`

. If `e1`

is a value, then since we know that the pair
evaluates, it must be the case that `e2`

is not a value and further
evaluates, so we apply the induction hypothesis to it. The cases for
`EFst`

and `ESnd`

are similar.

val preservationP : e:expP{Some? (typingP emptyP e) /\ Some? (stepP e)} -> Tot (u:unit{typingP emptyP (Some?.v (stepP e)) == typingP emptyP e}) let rec preservationP e = match e with (* {{{ two unchanged cases *) | EAppP e1 e2 -> if is_valueP e1 then (if is_valueP e2 then let EAbsP x _ ebody = e1 in substitution_preserves_typingP x ebody e2 emptyP else preservationP e2) else preservationP e1 | EIfP e1 _ _ -> if not (is_valueP e1) then preservationP e1 (* }}} *) | EPairP e1 e2 -> (match is_valueP e1, is_valueP e2 with | false, _ -> preservationP e1 | true , false -> preservationP e2) | EFstP e1 | ESndP e1 -> if not (is_valueP e1) then preservationP e1

We want to add a let construct to this formal development. We add the following to the definition of expressions:

```
type exp =
...
| ELet : int -> exp -> exp -> exp
```

Add cases for `ELet`

to all definitions and proofs.

Define a big-step interpreter for STLC as a recursive function `eval`

that given a well-typed expression `e`

either produces the well-typed
value `v`

to which `e`

evaluates or it diverges if the evaluation of
`e`

loops. Give `eval`

the following strong type ensuring that `v`

has the same type as `e`

(basically this type captures both progress
and preservation):

val eval : e:exp{Some? (typing empty e)} -> Dv (v:exp{is_value v && typing empty v = typing empty e})

The `Dv`

effect is that of potentially divergent computations. We
cannot mark this as `Tot`

since *a priori* STLC computations could
loop, and it is hard to prove that well-typed ones don’t.

Here is a solution that only uses `typed_step`

(suggested by Santiago
Zanella):

let rec eval e = if is_value e then e else eval (typed_step e)

or using the `progress`

and `preservation`

lemmas instead of
`typed_step`

(suggested by Guido Martinez):

val eval' : e:exp{Some? (typing empty e)} -> Dv (v:exp{is_value v && typing empty v = typing empty e}) let rec eval' e = match step e with | None -> progress e; e | Some e' -> preservation e; eval' e'

Here is another solution that only uses the substitution lemma:

val eval'' : e:exp{Some? (typing empty e)} -> Dv (v:exp{is_value v && typing empty v = typing empty e}) let rec eval'' e = let Some t = typing empty e in match e with | EApp e1 e2 -> (let EAbs x _ e' = eval' e1 in let v = eval' e2 in substitution_preserves_typing x e' v empty; eval'' (subst x v e')) | EAbs _ _ _ | ETrue | EFalse -> e | EIf e1 e2 e3 -> (match eval'' e1 with | ETrue -> eval'' e2 | EFalse -> eval'' e3)