Simply Typed Lambda Calculus

In this chapter, we look at how inductively defined types can be used to represent both raw data, inductively defined relations, and proofs relating the two.

By way of illustration, we develop a case study in the simply typed lambda calculus (STLC), a very simple programming language which is often studied in introductory courses on the semantics of programming languages. Its syntax, type system, and runtime behavior can be described in just a few lines. The main result we’re interested in proving is the soundness of the type system, i.e., that if a program type checks then it can be executed safely without a certain class of runtime errors.

If you haven’t seen the STLC before, there are several good resources for it available on the web, including the Software Foundations book, though we’ll try to keep the presentation here as self-contained as possible. Thanks to Simon Forest, Catalin Hritcu, and Simon Schaffer for contributing parts of this case study.

Syntax

The syntax of programs \(e\) is defined by the context-free grammar shown below.

\[e~::=~()~|~x~|~\lambda x:t. e_0~|~e_0~e_1\]

This can be read as follows: a program \(e\) is either

  • the unit value \(()\);

  • a variable \(x\);

  • a lambda term \(\lambda x:t. e_0\) associating a variable \(x\) to a type \(t\) and a some sub-program \(e_0\);

  • or, the application of the sub-program \(e_0\) to another sub-program \(e_1\).

The syntax of the type annotation \(t\) is also very simple:

\[t~::=~\mathsf{unit}~|~t_0 \rightarrow t_1\]

A type \(t\) is either

  • the \(\mathsf{unit}\) type constant;

  • or, arrow type \(t_0 \rightarrow t_1\) formed from two smaller types \(t_0\) and \(t_1\)

This language is very minimalistic, but it can be easily extended with some other forms, e.g., one could add a type of integers, integer constants, and operators like addition and subtraction. We’ll look at that as part of some exercises.

We’ll define the syntax of types and programs formally in F* as a pair of simple inductive datatypes typ (for types) and exp (for programs or expressions) with a constructor for each of the cases above.

The main subtlety is in the representation of variables. For example, ignoring the type annotations, in the term \(\lambda x. (\lambda x. x)\) the inner lambda binds a different \(x\) than the outer one, i.e., the term is equivalent to \(\lambda x. (\lambda y. y)\) and our representation of programs must respect this this convention. We’ll use a technique called de Bruijn indices, where the names of the variables are no longer significant and instead each variable is represented by a natural number describing the number of \(\lambda\) binders that one must cross when traversing a term from the occurrence of the variable to that variable’s \(\lambda\) binder.

For example, the terms \(\lambda x. (\lambda x. x)\) and \(\lambda x. (\lambda y. y)\) are both represented as \(\lambda _. (\lambda _. 0)\), since the inner occurrence of \(x\) is associated with the inner \(\lambda\); while \(\lambda x. (\lambda y. (\lambda z. x))\) is represented as \(\lambda _. (\lambda _. (\lambda _. 2)\), since from the inner occurrence of \(x\) one must skip past \(2\) \(\lambda\)’s to reach the \(\lambda\) associated with \(x\). Note, the variable names are no longer significant in de Bruijn’s notation.

Representing types

The inductive type typ defined below is our representation of types.

type typ =
  | TUnit : typ
  | TArr  : typ -> typ -> typ

This is entirely straightforward: a constructor for each case in our type grammar, as described above.

Representing programs

The representation of program expressions is shown below:

let var = nat
type exp =
  | EUnit : exp
  | EVar  : var -> exp
  | ELam  : typ -> exp -> exp
  | EApp  : exp -> exp -> exp

This too is straightforward: a constructor for each case in our program grammar, as described above. We use a nat to represent variables var and ELam represents an annotated lambda term of the form \(\lambda _:t. e\), where the name of the binder is omitted, since we’re using de Bruijn’s representation.

Runtime semantics

STLC has just one main computation rule to execute a program—the function application rule or a \(\beta\) reduction, as shown below:

\[(\lambda x:t. e_0)~e_1 \longrightarrow e_0 [x \mapsto e_1]\]

This says that when a \(\lambda\) literal is applied to an argument \(e_1\) the program takes a single step of computation to the body of the lambda literal \(e_0\) with every occurrence of the bound variable \(x\) replaced by the argument \(e_1\). The substituion has to be careful to avoid “name capture”, i.e., substituting a term in a context that re-binds its free variables. For example, when substituting \(y \mapsto x\) in \(\lambda x. y\), one must make sure that the resulting term is not \(\lambda x. x\). Using de Bruijn notation will help us make precise and avoid name capture.

The other computation rules in the language are inductively defined, e.g., \(e_0~e_1\) can take a step to \(e_0'~e_1\) if \(e_0 \longrightarrow e_0'\), and similarly for \(e_1\).

By choosing these other rules in different ways one obtains different reduction strategies, e.g., call-by-value or call-by-name etc. We’ll leave the choice of reduction strategy non-deterministic and represent the computation rules of the STLC as an indexed inductive type, step e e' encoding one or more steps of computation.

Formalizing an Operational Semantics

The inductive type step below describes a single step of computation in what is known as a “small-step operational semantics”. The type step e e' is a relation between an initial program e and a program e' that results after taking one step of computation on some sub-term of e.

type step : exp -> exp -> Type =
  | Beta :
     t:typ ->
     e1:exp ->
     e2:exp ->
     step (EApp (ELam t e1) e2) (subst (sub_beta e2) e1)

  | AppLeft :
      #e1:exp ->
      e2:exp ->
      #e1':exp ->
      hst:step e1 e1' ->
      step (EApp e1 e2) (EApp e1' e2)

  | AppRight : 
      e1:exp ->
      #e2:exp ->
      #e2':exp ->
      hst:step e2 e2' ->
      step (EApp e1 e2) (EApp e1 e2')

  • The constructor Beta represents the rule for \(\beta\) reduction. The most subtle part of the development is defining subst and sub_beta—we’ll return to that in detail shortly.

  • AppLeft and AppRight allow reducing either the left- or right-subterm of EApp e1 e2.

Exercise

Define an inductive relation steps : exp -> exp -> Type for the transitive closure of step, representing multiple steps of computation.

Use this exercise file for all the exercises that follow.

Answer

type steps : exp -> exp -> Type =
  | Single : #e0:exp ->
             #e1:exp ->
             step e0 e1 -> 
             steps e0 e1

  | Many  : #e0:exp ->
             #e1:exp ->
             #e2:exp -> 
             step e0 e1 ->
             steps e1 e2 -> 
             steps e0 e2

Substitution: Failed Attempt

Defining substitution is the trickiest part of the system. Our first attempt will convey the main intuitions, but F* will refuse to accept it as well-founded. We’ll then enrich our definitions to prove that substitution terminates.

We’ll define a substitution as a total function from variables var to expressions exp.

let sub0 = var -> exp

These kind of substitutions are sometimes called “parallel substitutions”—the each variable is substituted independently of the others.

When doing a \(\beta\) reduction, we want to substitute the variable associated with de Bruijn index 0 in the body of the function with the argument e and then remove the \(\lambda\) binder—sub_beta0 does just that, replacing variable 0 with e and shifting other variables down by 1, since the \(\lambda\) binder of the function is removed.

let sub_beta0 (e:exp)
  : sub0
  = fun (y:var) ->
        if y = 0 then e      (* substitute *)
        else EVar (y-1)    (* shift -1 *)

The function subst s e applies the substitution s to e:

let sub_inc0 : sub0 =  fun y -> EVar (y+1)

[@@expect_failure [19;19]]
let rec subst0 (s:sub0)
               (e:exp)
  : exp
  = match e with
    | EUnit -> EUnit
    | EVar x -> s x
    | EApp e1 e2 -> EApp (subst0 s e1) (subst0 s e2)
    | ELam t e1 -> ELam t (subst0 (sub_elam0 s) e1)

and sub_elam0 (s:sub0) 
  : sub0
  =  fun y ->
        if y=0
        then EVar y
        else subst0 sub_inc0 (s (y - 1))
  • The EUnit case is trivial—there are no variables to substitute.

  • In the variable case subst0 s (EVar x) just applies s to x.

  • In the EApp case, we apply the substitution to each sub-term.

  • The ELam case is the most interesting. To apply the substitution s to the body e1, we have to traverse a binder. The mutally recursive function sub_elam0 s adjusts s to account for this new binder, which has de Bruijn index 0 in the body e1 (at least until another binder is encountered).

    • In sub_elam0, if we are applying s to the newly bound variable at index 0, then we leave that variable unchanged, since s cannot affect it.

    • Otherwise, we have a variable with index at least 1, referencing a binder that is bound in an outer scope; so, we shift it down and apply s to it, and then increment all the variables in the resulting term (using sub_inc0) to avoid capture.

This definition of substitution is correct, but F* refuses to accept it since we have not convinced the typechecker that subst0 and sub_elam0 actually terminate. In fact, F* complains in two locations about a failed termination check.

Note

This definition is expected to fail, so the [@@expect_failure [19;19]] attribute on the definition asks F* to check that the definition raises Error 19 twice. We’ll look in detail as to why it fails, next.

Substitution, Proven Total

Informally, let’s try to convince ourselves why subst0 and sub_elam0 actually terminate.

  • The recursive calls in the EApp case are applied to strictly smaller sub-terms (e0 and e1) of the original term e.

  • In the ELam case, we apply subst0 to a smaller sub-term e1, but we make a mutally recursive call to sub_elam0 s first—so we need to check that that call terminates. This is the first place where F* complains.

  • When calling sub_elam0, it calls back to subst0 on a completely unrelated term s (y - 1), and F* complains that this may not terminate. But, thankfully, this call makes use only of the sub_inc0 substitution, which is just a renaming substitution and which does not make any further recursive calls. Somehow, we have to convince F* that a recursive call with a renaming substitution is fine.

To distinguish renamings from general substitutions, we’ll use an indexed type sub r, shown below.

let sub (renaming:bool) = 
    f:(var -> exp){ renaming <==> (forall x. EVar? (f x)) }
  • sub true is the type of renamings, substitutions that map variables to variables.

  • sub false are substitutions that map at least one variable to a non-variable.

It’s easy to prove that sub_inc is a renaming:

let sub_inc 
  : sub true
  = fun y -> EVar (y+1)

The function sub_beta shown below is the analog of sub_beta0, but with a type that tracks whether it is a renaming or not.

let sub_beta (e:exp)
  : sub (EVar? e)
  = let f = 
      fun (y:var) ->
        if y = 0 then e      (* substitute *)
        else (EVar (y-1))    (* shift -1 *)
    in
    if not (EVar? e)
    then introduce exists (x:var). ~(EVar? (f x))
         with 0 and ();
    f
  • The type says that sub_beta e is a renaming if and only if e is itself a variable.

  • Proving this type, particularly in the case where e is not a variable requires proving an existentially quantified formula, i.e., exists x. ~(EVar (subst_beta e) x). As mentioned previously, the SMT solver cannot always automatically instantiate existential quantifiers in the goal. So, we introduce the existential quantifier explicitly, providing the witness 0, and then the SMT solver can easily prove ~(EVar (subst_beta e) 0).

Finally, we show the definitions of subst and sub_elam below—identical to subst0 and sub_elam0, but enriched with types that allow expressing a termination argument to F* using a 4-ary lexicographic ordering.

let bool_order (b:bool) = if b then 0 else 1
let is_var (e:exp) : int = if EVar? e then 0 else 1

let rec subst (#r:bool)
              (s:sub r)
              (e:exp)
  : Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
        (decreases %[bool_order (EVar? e); 
                     bool_order r;
                     1;
                     e])
  = match e with
    | EUnit -> EUnit
    | EVar x -> s x
    | EApp e1 e2 -> EApp (subst s e1) (subst s e2)
    | ELam t e1 -> ELam t (subst (sub_elam s) e1)

and sub_elam (#r:bool) (s:sub r) 
  : Tot (sub r)
        (decreases %[1;
                     bool_order r;
                     0;
                     EVar 0])
  = let f : var -> exp = 
      fun y ->
        if y=0
        then EVar y
        else subst sub_inc (s (y - 1))
    in
    assert (not r ==> (forall x. ~(EVar? (s x)) ==> ~(EVar? (f (x + 1)))));
    f

Let’s analyze the recursive calls of subst and subst_elam to see why this order works.

  • Cases of subst:

    • The EUnit and EVar cases are trivial, as before.

    • In EApp, e is definitely not a variable, so bool_order (EVar? e) is 1. if e1 (respectively e2) are variables, then this recursive call terminates, the lexicographic tuple (0, _, _, _) << (1, _, _, _), regardles of the other values. Otherwise, the last component of the tuple decreases (since e1 and e2 are proper sub-terms of e), while none of the other components of the tuple change.

    • The call to sub_elam s in ELam terminates because the third component of the tuple decreases from 1 to 0, while the first two do not change.

    • The final recursive call to subst terminates for similar reasons to the recursive calls in the EApp case, since the type of sub_elam guarantees that sub_elam s is renaming if an only of s is (so the r bit does not change).

  • Cases of sub_elam, in the recursive call to subst sub_inc (s (y - 1)), we have already proven that sub_inc is a renaming. So, we have two cases to consider:

    • If s (y - 1) is a variable, then bool_order (EVar? e), the first component of the decreases clause of subst is 0, which clearly precedes 1, the first component of the decreases clause of subst_elam.

    • Otherwwise, s (y - 1) is not a variable, so s is definitely not a renaming while sub_inc is. So, the second second component of the decreases clause decreases while the first component is unchanged.

Finally, we need to prove that sub_elam s is a renaming if and only if s is. For this, we need two things:

  • First, strengthen the type of subst s to show that it maps variables to variables if and only if r is a renaming,

  • Second, we need to instantiate an exisential quantifier in sub_elam, to show that if s is not a renaming, then it must map some x to a non-variable and, hence, sub_elam s (x + 1) is a non-variable too. One way to do this is by asserting this fact, which is a sufficient hint to the SMT solver to find the instantiation needed. Another way is to explicitly introduce the existential, as in the exercise below.

In summary, using indexed types combined with well-founded recursion on lexicographic orderings, we were able to prove our definitions total. That said, coming up with such orderings is non-trivial and requires some ingenuity, but once you do, it allows for relatively compact definitions that handle both substiutions and renamings.

Exercise

Remove the first component of the decreases clause of both definitions and revise the definitions to make F* accept it.

Your solution should have signature

let rec subst1 (#r:bool)
               (s:sub r)
               (e:exp)
  : Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
        (decreases %[bool_order r;
                     1;
                     e])
...

and sub_elam1 (#r:bool) (s:sub r)
  : Tot (sub r)
        (decreases %[bool_order r;
                     0;
                     EVar 0])

Hint

Inline a case of subst in subst_elam. The answer is included with the next problem below.


Replace the assertion in subst_elam with a proof that explicitly introduces the existential quantifier.

Answer

let rec subst1 (#r:bool)
              (s:sub r)
              (e:exp)
  : Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
        (decreases %[bool_order r;
                     1;
                     e])
  = match e with
    | EVar x -> s x
    | ELam t e1 -> ELam t (subst1 (sub_elam1 s) e1)
    | EApp e1 e2 -> EApp (subst1 s e1) (subst1 s e2)
    | EUnit -> EUnit

and sub_elam1 (#r:bool) (s:sub r) 
  : Tot (sub r)
        (decreases %[bool_order r;
                     0;
                     EVar 0])
  = let f : var -> exp = 
      fun y ->
        if y=0
        then EVar y
        else match s (y - 1) with
             | EVar x -> sub_inc x
             | e -> subst1 sub_inc e
    in
    introduce not r ==> (exists x. ~ (EVar? (f x))) 
    with not_r. 
      eliminate exists y. ~ (EVar? (s y))
      returns _
      with not_evar_sy. 
        introduce exists x. ~(EVar? (f x))
        with (y + 1)
        and ()
    ;
    f

Type system

If when running a program, if one ends up with an term like \(()~e\) (i.e., some non-function term like \(()\) being used as if it were a function) then a runtime error has occurred and the program crashes. A type system for the simply-typed lambda calculus is designed to prevent this kind of runtime error.

The type system is an inductively defined relation typing g e t between a

  • typing environment g:env, a partial map from variable indexes in a particular scope to their annotated types;

  • a program expression e:exp;

  • and its type t:typ.

Environments

The code below shows our representation of typing environments env, a total function from variable indexes var to Some t or None.

let env = var -> option typ

let empty : env = fun _ -> None

let extend (t:typ) (g:env) 
  : env 
  = fun y -> if y = 0 then Some t
          else g (y-1)
  • The empty environment maps all variables to None.

  • Extending an an environment g associating a type t with a new variable at index 0 involves shifting up the indexes of all other variables in g by 1.

Typing Relation

The type system of STLC is defined by the inductively defined relation typing g e t shown below. A value of typing g e t is a derivation, or a proof, that e has type t in the environment g.

noeq 
type typing : env -> exp -> typ -> Type =
  | TyUnit :
      #g:env ->
      typing g EUnit TUnit

  | TyVar :
      #g:env ->
      x:var{Some? (g x)} ->
      typing g (EVar x) (Some?.v (g x))

  | TyLam :
      #g :env ->
      t:typ ->
      #e1:exp ->
      #t':typ ->
      hbody:typing (extend t g) e1 t' ->
      typing g (ELam t e1) (TArr t t')
            
  | TyApp :
      #g:env ->
      #e1:exp ->
      #e2:exp ->
      #t11:typ ->
      #t12:typ ->
      h1:typing g e1 (TArr t11 t12) ->
      h2:typing g e2 t11 ->
      typing g (EApp e1 e2) t12
  • The type does not support decidable equality, since all its constructors contain a field g:env, a function-typed value without decidable equality. So, we mark the inductive with the noeq qualifier, as described previously.

  • TyUnit says that the unit value EUnit has type TUnit in all environments.

  • TyVar says that a variable x is well-typed only in an environment g that binds its type to Some t, in which case, the program EVar x has type t. This rule ensures that no out-of-scope variables can be used.

  • TyLam says that a function literal ELam t e1 has type TArr t t' in environment g, when the body of the function e1 has type t' in an environment that extends g with a binding for the new variable at type t (while shifting and retaining all other ariables).

  • Finally, TyApp allows applying e1 to e2 only when e1 has an arrow type and the argument e2 has the type of the formal parameter of e1—the entire term has the return type of e1.

Progress

It’s relatively easy to prove that a well-typed non-unit or lambda term with no free variables can take a single step of computation. This property is known as progress.

Exercise

State and prove progress.

Answer

let is_value (e:exp) : bool = ELam? e || EUnit? e

let rec progress (#e:exp {~ (is_value e) })
                 (#t:typ)
                 (h:typing empty e t)
  : (e':exp & step e e')
  = let TyApp #g #e1 #e2 #t11 #t12 h1 h2 = h in
    match e1 with
    | ELam t e1' -> (| subst (sub_beta e2) e1', Beta t e1' e2 |)
    | _          -> let (| e1', h1' |) = progress h1 in
                   (| EApp e1' e2, AppLeft e2 h1'|)

Preservation

Given a well-typed term satisfying typing g e t and steps e e', we would like to prove that e' has the same type as e, i.e., typing g e' t. This property is known as preservation (or sometimes subject reduction). When taken in combination with progress, this allows us to show that a well-typed term can keep taking a step until it reaches a value.

The proof below establishes preservation for a single step.

let rec preservation_step #e #e' #g #t (ht:typing g e t) (hs:step e e') 
  : typing g e' t
  = let TyApp h1 h2 = ht in
    match hs with
    | Beta tx e1' e2' -> substitution_beta h2 (TyLam?.hbody h1)
    | AppLeft e2' hs1   -> TyApp (preservation_step h1 hs1) h2
    | AppRight e1' hs2   -> TyApp h1 (preservation_step h2 hs2)
  • Since we know the computation takes a step, the typing derivation ht must be an instance of TyApp.

  • In the AppLeft and AppRight case, we can easily use the induction hypothesis depending on which side actually stepped.

  • The Beta case is the most interesting and requires a lemma about substitutions preserving typing.

The substitution lemma follows:

let subst_typing #r (s:sub r) (g1:env) (g2:env) =
    x:var{Some? (g1 x)} -> typing g2 (s x) (Some?.v (g1 x))

let rec substitution (#g1:env) 
                     (#e:exp)
                     (#t:typ)
                     (#r:bool)
                     (s:sub r)
                     (#g2:env)
                     (h1:typing g1 e t)
                     (hs:subst_typing s g1 g2)
   : Tot (typing g2 (subst s e) t)
         (decreases %[bool_order (EVar? e); bool_order r; e])
   = match h1 with
     | TyUnit -> TyUnit
     | TyVar x -> hs x
     | TyApp hfun harg -> TyApp (substitution s hfun hs) (substitution s harg hs)
     | TyLam tlam hbody ->
       let hs'' : subst_typing (sub_inc) g2 (extend tlam g2) =
         fun x -> TyVar (x+1) 
       in
       let hs' : subst_typing (sub_elam s) (extend tlam g1) (extend tlam g2) =
         fun y -> if y = 0 then TyVar y
               else substitution sub_inc (hs (y - 1)) hs''
       in
       TyLam tlam (substitution (sub_elam s) hbody hs')

It starts with a notion of typability of substitutions, subst_typing s g1 g2, which that if a variable x has type g1 x, then s x must have that same type in g2.

The substitution lemma lifts this notion to expressions, stating that applying a well-typed substitution subst_typing s g1 g2 to a term well-typed in g1 produces a term well-typed in g2 with the same type.

Exercise

Use the substitution lemma to state and prove the substitution_beta lemma used in the proof of preservation.

Answer

let substitution_beta #e #v #t_x #t #g 
                      (h1:typing g v t_x)
                      (h2:typing (extend t_x g) e t)
  : typing g (subst (sub_beta v) e) t
  = let hs : subst_typing (sub_beta v) (extend t_x g) g =
        fun y -> if y = 0 then h1 else TyVar (y-1) in
    substitution (sub_beta v) h2 hs

Exercise

Prove a preservation lemma for multiple steps.

Answer

let rec preservation #e #e' #g #t (ht:typing g e t) (hs:steps e e') 
  : Tot (typing g e' t)
        (decreases hs)
  = match hs with
    | Single s -> 
      preservation_step ht s
    | Many s0 s1 -> 
      let ht' = preservation_step ht s0 in
      preservation ht' s1

Exercise

Prove a type soundness lemma with the following statement:

let soundness #e #e' #t 
              (ht:typing empty e t) 
  : either (squash (is_value e))
           (e':exp & steps e e' & typing empty e' t)

Answer

  = if is_value e then Inl ()
    else let (| e', s |) = progress ht in
         let ht' = preservation_step ht s in
         Inr (| e', Single s, ht' |)

Exercise

Add a step for reduction underneath a binder and prove the system sound.

Answer

(*
   Copyright 2014-2015
     Simon Forest - Inria and ENS Paris
     Catalin Hritcu - Inria
     Nikhil Swamy - Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module Part2.STLC.Strong
open FStar.Classical.Sugar
(* Constructive-style progress and preservation proof for STLC with
   strong reduction, using deBruijn indices and parallel substitution. *)

type typ =
  | TUnit : typ
  | TArr  : typ -> typ -> typ

let var = nat
type exp =
  | EUnit : exp
  | EVar  : var -> exp
  | ELam  : typ -> exp -> exp
  | EApp  : exp -> exp -> exp

(* Parallel substitution operation `subst` *)
let sub (renaming:bool) = 
    f:(var -> exp){ renaming <==> (forall x. EVar? (f x)) }

let bool_order (b:bool) = if b then 0 else 1

let sub_inc 
  : sub true
  = fun y -> EVar (y+1)

let is_var (e:exp) : int = if EVar? e then 0 else 1

let rec subst (#r:bool)
              (s:sub r)
              (e:exp)
  : Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
        (decreases %[bool_order (EVar? e); 
                     bool_order r;
                     1;
                     e])
  = match e with
    | EVar x -> s x
    | ELam t e1 -> ELam t (subst (sub_elam s) e1)
    | EApp e1 e2 -> EApp (subst s e1) (subst s e2)
    | EUnit -> EUnit

and sub_elam (#r:bool) (s:sub r) 
  : Tot (sub r)
        (decreases %[1;
                     bool_order r;
                     0;
                     EVar 0])
  = let f : var -> exp = 
      fun y ->
        if y=0
        then EVar y
        else subst sub_inc (s (y - 1))
    in
    introduce not r ==> (exists x. ~ (EVar? (f x)))
    with not_r. 
      eliminate exists y. ~ (EVar? (s y))
      returns (exists x. ~ (EVar? (f x)))
      with (not_evar_sy:squash (~(EVar? (s y)))). 
        introduce exists x. ~(EVar? (f x))
        with (y + 1)
        and ()
    ;
    f

let sub_beta (e:exp)
  : sub (EVar? e)
  = let f = 
      fun (y:var) ->
        if y = 0 then e      (* substitute *)
        else (EVar (y-1))    (* shift -1 *)
    in
    if not (EVar? e)
    then introduce exists (x:var). ~(EVar? (f x))
         with 0 and ();
    f

(* Small-step operational semantics; strong / full-beta reduction is
   non-deterministic, so necessarily as inductive relation *)

type step : exp -> exp -> Type =
  | SBeta : t:typ ->
            e1:exp ->
            e2:exp ->
            step (EApp (ELam t e1) e2) (subst (sub_beta e2) e1)

  | SApp1 : #e1:exp ->
             e2:exp ->
            #e1':exp ->
            hst:step e1 e1' ->
            step (EApp e1 e2) (EApp e1' e2)

  | SApp2 :  e1:exp ->
            #e2:exp ->
            #e2':exp ->
            hst:step e2 e2' ->
            step (EApp e1 e2) (EApp e1 e2')

  | STrans : #e0:exp ->
             #e1:exp ->
             #e2:exp -> 
             step e0 e1 ->
             step e1 e2 -> 
             step e0 e2

  | SStrong : t:typ ->
              e:exp ->
              e':exp ->
              step e e' -> 
              step (ELam t e) (ELam t e')

(* Type system; as inductive relation (not strictly necessary for STLC) *)

type env = var -> option typ

let empty : env = fun _ -> None

(* we only need extend at 0 *)
let extend (t:typ) (g:env) 
  : env 
  = fun y -> if y = 0 then Some t
          else g (y-1)

noeq 
type typing : env -> exp -> typ -> Type =
  | TyUnit : #g:env ->
             typing g EUnit TUnit

  | TyVar : #g:env ->
             x:var{Some? (g x)} ->
             typing g (EVar x) (Some?.v (g x))

  | TyLam : #g :env ->
            t:typ ->
            #e1:exp ->
            #t':typ ->
            hbody:typing (extend t g) e1 t' ->
            typing g (ELam t e1) (TArr t t')
            
  | TyApp : #g:env ->
            #e1:exp ->
            #e2:exp ->
            #t11:typ ->
            #t12:typ ->
            h1:typing g e1 (TArr t11 t12) ->
            h2:typing g e2 t11 ->
            typing g (EApp e1 e2) t12
            

(* Progress *)

let is_value (e:exp) : bool = ELam? e || EUnit? e

let rec progress (#e:exp {~ (is_value e) })
                 (#t:typ)
                 (h:typing empty e t)
  : (e':exp & step e e')
  = let TyApp #g #e1 #e2 #t11 #t12 h1 h2 = h in
    match e1 with
    | ELam t e1' -> (| subst (sub_beta e2) e1', SBeta t e1' e2 |)
    | _          -> let (| e1', h1' |) = progress h1 in
                   (| EApp e1' e2, SApp1 e2 h1'|)

(* Typing of substitutions (very easy, actually) *)
let subst_typing #r (s:sub r) (g1:env) (g2:env) =
    x:var{Some? (g1 x)} -> typing g2 (s x) (Some?.v (g1 x))

(* Substitution preserves typing
   Strongest possible statement; suggested by Steven Schäfer *)
let rec substitution (#g1:env) 
                     (#e:exp)
                     (#t:typ)
                     (#r:bool)
                     (s:sub r)
                     (#g2:env)
                     (h1:typing g1 e t)
                     (hs:subst_typing s g1 g2)
   : Tot (typing g2 (subst s e) t)
         (decreases %[bool_order (EVar? e); bool_order r; e])
   = match h1 with
   | TyVar x -> hs x
   | TyApp hfun harg -> TyApp (substitution s hfun hs) (substitution s harg hs)
   | TyLam tlam hbody ->
     let hs'' : subst_typing (sub_inc) g2 (extend tlam g2) =
       fun x -> TyVar (x+1) in
     let hs' : subst_typing (sub_elam s) (extend tlam g1) (extend tlam g2) =
       fun y -> if y = 0 then TyVar y
             else substitution sub_inc (hs (y - 1)) hs''
     in TyLam tlam (substitution (sub_elam s) hbody hs')
   | TyUnit -> TyUnit

(* Substitution for beta reduction
   Now just a special case of substitution lemma *)
let substitution_beta #e #v #t_x #t #g 
                      (h1:typing g v t_x)
                      (h2:typing (extend t_x g) e t)
  : typing g (subst (sub_beta v) e) t
  = let hs : subst_typing (sub_beta v) (extend t_x g) g =
        fun y -> if y = 0 then h1 else TyVar (y-1) in
    substitution (sub_beta v) h2 hs

(* Type preservation *)
let rec preservation #e #e' #g #t (ht:typing g e t) (hs:step e e') 
  : Tot (typing g e' t)
        (decreases hs)
  = match hs with
    | STrans s0 s1 ->
      let ht' = preservation ht s0 in
      preservation ht' s1
    | _ ->
      match ht with
      | TyApp h1 h2 -> (
        match hs with
        | SBeta tx e1' e2' -> substitution_beta h2 (TyLam?.hbody h1)
        | SApp1 e2' hs1   -> TyApp (preservation h1 hs1) h2
        | SApp2 e1' hs2   -> TyApp h1 (preservation h2 hs2)
      )
      | TyLam t hb ->
        let SStrong t e e' hs' = hs in
        let hb' = preservation hb hs' in
        TyLam t hb'