Case study: simply-typed lambda-calculus¶

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 that

  typing 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 that

  typing 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¶

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

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

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

type envP = int -> Tot (option tyP)

val emptyP : envP
let emptyP = fun _ -> None

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

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

  | _ -> ()

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

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

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

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

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'

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)