Week 7: Simply-Typed Lambda Calculus (STLC)

Display all goals and responses

Author: Adam Chlipala, Benjamin C. Pierce Aurèle Barrière,
License: No redistribution allowed (usage by permission in CS-428).

Introduction

The last few chapters have focused on small programming languages that are representative of the essence of the imperative languages. We now turn to lambda-calculus, the usual representative of functional languages.

Notation var := string.
Definition var_eq : forall x y : var, {x = y} + {x <> y} := string_dec.
Infix "==v" := var_eq (no associativity, at level 50).

The simply typed lambda-calculus (STLC) is a tiny core calculus embodying the key concept of functional abstraction. This concept shows up in pretty much every real-world programming language in some form (functions, procedures, methods, etc.).

We will follow a standard pattern: we formalize the calculus (syntax, small-step semantics), we define the typing rules, and finally we prove interesting properties about the type system (progress and preservation).

The new technical challenges arise from the mechanisms of variable binding and substitution. It will take some work to deal with these.

Module Stlc.

Syntax

In our version of STLC, we have natural number constants and addition. This will let us define a simple type systems that checks whether something evaluates to a natural number. If you are used to a simpler definition of Lambda calculus, we will see as exercises how to encode natural numbers using the more basic lambda calculus.

  Inductive exp : Set :=
  | Var (x : var)
  | Const (n : nat)
  | Plus (e1 e2 : exp)
  | Abs (x : var) (e1 : exp)
  | App (e1 e2 : exp).

The STLC is a language of higher-order functions: we can write down functions that take other functions as arguments and/or return other functions as results.

The STLC doesn't provide any primitive syntax for defining named functions: i.e., all functions are "anonymous." But they could easily be introduced: indeed, the fundamental naming and binding mechanisms are exactly the same.

The STLC lives in the lower-left front corner of the famous lambda cube (also called the Barendregt Cube), which visualizes three sets of features that can be added to its simple core:

(*
                            Calculus of Constructions
      type operators +--------+
                    /|       /|
                   / |      / |
     polymorphism +--------+  |
                  |  |     |  |
                  |  +-----|--+
                  | /      | /
                  |/       |/
                  +--------+ dependent types
                STLC
 *)

Moving from bottom to top in the cube corresponds to adding polymorphic types like forall X, X -> X. Adding just polymorphism gives us the famous Girard-Reynolds calculus, System F. (terms bind types)

Moving from front to back corresponds to adding type operators like list. (types bind types)

Moving from left to right corresponds to adding dependent types like forall n, array-of-size n. (types bind terms)

The top right corner on the back, which combines all three features, is called the Calculus of Constructions. First studied by Coquand and Huet, it forms the foundation of Coq's logic. Coq's logic is the Calculus of Inductive Constructions (CIC), a variant of the Calculus of COnstructions.

Semantics

To define the small-step semantics of STLC terms, we begin, as always, by defining the set of values. Next, we define the critical notion of substitution, which is used in the reduction rule for application expressions. And finally we give the small-step relation itself.

  Inductive value : exp -> Prop :=
  | VConst : forall n, value (Const n)
  | VAbs : forall x e1, value (Abs x e1).

Recall that value correspond to terms that have no more work to do. Clearly, constants are value, and applications are not.

For abstractions, we have a choice:

We can say that \x.t is a value only when t is a value -- i.e., only if the function's body has been reduced (as much as it can be without knowing what argument it is going to be applied to).
Or we can say that \x.t is always a value, no matter whether t is one or not -- in other words, we can say that reduction stops at abstractions.

Our usual way of evaluating expressions in Gallina makes the first choice -- for example,

  Compute (fun x:bool => 3 + 4).= fun _ : bool => 7
: bool -> nat

But Gallina is rather unusual in this respect. Most real-world functional programming languages make the second choice -- reduction of a function's body only begins when the function is actually applied to an argument.

We also make the second choice here.

Now we come to the heart of the STLC: the operation of substituting one term for a variable in another term. This operation is used below to define the operational semantics of function application, where we will need to substitute the argument term for the function parameter in the function's body.

Here subst e1 x e2 replaces all occurences of x in e2 with e1. Here we define a functional version, but we could very well have defined an inductive proposition.

subst is not applicable when e1 is not closed, to avoid some complexity we don't need.

  Fixpoint subst (e1 : exp) (x : string) (e2 : exp) : exp :=
    match e2 with
      | Var y => if y ==v x then e1 else Var y
      | Const n => Const n
      | Plus e2' e2'' => Plus (subst e1 x e2') (subst e1 x e2'')
      | Abs y e2' => Abs y (if y ==v x then e2' else subst e1 x e2')
      | App e2' e2'' => App (subst e1 x e2') (subst e1 x e2'')
    end.


  Inductive step : exp -> exp -> Prop :=
  (* These rules show the real action of the semantics. *)
  | Beta : forall x e v,
      value v
      -> step (App (Abs x e) v) (subst v x e)
  | Add : forall n1 n2,
      step (Plus (Const n1) (Const n2)) (Const (n1 + n2))
  (* Then we have a bunch of bureaucratic, repetitive rules encoding
  evaluation order.  See next lecture for how to streamline this
  part, but for now note that the [value] premises below are crucial
  to enforce a single order of evaluation. *)
  | App1 : forall e1 e1' e2,
      step e1 e1'
      -> step (App e1 e2) (App e1' e2)
  | App2 : forall v e2 e2',
      value v
      -> step e2 e2'
      -> step (App v e2) (App v e2')
  | Plus1 : forall e1 e1' e2,
      step e1 e1'
      -> step (Plus e1 e2) (Plus e1' e2)
  | Plus2 : forall v e2 e2',
      value v
      -> step e2 e2'
      -> step (Plus v e2) (Plus v e2').

Some helpful notations to define programs.

  Coercion Const : nat >-> exp.
  Infix "^+^" := Plus (at level 50).
  Coercion Var : var >-> exp.
  Notation "\ x , e" := (Abs x e) (at level 51).
  Infix "@" := App (at level 49, left associativity).

Believe it or not, this is a Turing-complete language! Here's an example nonterminating program.

  Check "x"."x"
     : var
  Example omega := (\"x", "x" @ "x") @ (\"x", "x" @ "x").

  Lemma omega_loop:
    step omega omega.step omega omega
  Proof.step omega omega
    constructor.value (\ "x", "x" @ "x") constructor.
  Qed.

Types and Typing Environments

That language is suitable to describe with a static type system. Here's our modest, but countably infinite, set of types.

  Inductive type :=
  | Nat                  (* Numbers *)
  | Fun (dom ran : type) (* Functions *).

Although we are primarily interested in the binary relation relating a closed term t to its type T, we need to generalize a bit to make the definitions work.

Consider checking that \a,tb has type TA->TB. Intuitively, we need to check that tb has type TB. However, we have removed the binder \a, so a may occur free in tb (that is, tb may be open). While checking that tb has type TB, we must remember that a has type TA, in order to deal with these free occurrences of a. Similarly, tb itself could contain abstractions, and typechecking their bodies could require looking up the declared types of yet more free variables.

To keep track of all this, we add a third element to the relation, a typing context, which records the types of the variables that may occur free in a term -- that is, a partial map from variables to types.

Let us write these type maps and their operations.

  Definition type_map: Type :=  var -> option type.
  Definition empty_map : type_map := (fun v => None).
  Notation "$0" := empty_map.
  Definition tmap_get (tm:type_map) (v:var): option type :=
    tm v.
  Infix "$?" := tmap_get (no associativity, at level 50).
  Definition tmap_set (tm:type_map) (vt:var * type) :=
    fun v =>
      if (v ==v fst vt) then Some (snd vt)
      else tm v.
  Infix "$+" := tmap_set (no associativity, at level 50).
  Lemma tmap_gss:
    forall tm v t,
      (tm $+ (v,t)) $? v = Some t.forall (tm : type_map) (v : var) (t : type),
(tm $+ (v, t)) $? v = Some t
  Proof.forall (tm : type_map) (v : var) (t : type),
(tm $+ (v, t)) $? v = Some t
    intros tm v t.tm: type_map
v: var
t: type
(tm $+ (v, t)) $? v = Some t unfold tmap_get, tmap_set.tm: type_map
v: var
t: type
(if v ==v fst (v, t) then Some (snd (v, t)) else tm v) =
Some t simpl.tm: type_map
v: var
t: type
(if v ==v v then Some t else tm v) = Some t
    unfold var_eq.tm: type_map
v: var
t: type
(if string_dec v v then Some t else tm v) = Some t destruct (string_dec v v); auto.tm: type_map
v: var
t: type
n: v <> v
tm v = Some t
    exfalso.tm: type_map
v: var
t: type
n: v <> v
False apply n.tm: type_map
v: var
t: type
n: v <> v
v = v auto.
  Qed.
  Lemma tmap_gso:
    forall tm v1 v2 t,
      v1 <> v2 ->
      (tm $+ (v1,t)) $? v2 = tm $? v2.forall (tm : type_map) (v1 v2 : var) (t : type),
v1 <> v2 -> (tm $+ (v1, t)) $? v2 = tm $? v2
  Proof.forall (tm : type_map) (v1 v2 : var) (t : type),
v1 <> v2 -> (tm $+ (v1, t)) $? v2 = tm $? v2
    intros tm v1 v2 t H.tm: type_map
v1, v2: var
t: type
H: v1 <> v2
(tm $+ (v1, t)) $? v2 = tm $? v2 unfold tmap_get, tmap_set.tm: type_map
v1, v2: var
t: type
H: v1 <> v2
(if v2 ==v fst (v1, t)
 then Some (snd (v1, t))
 else tm v2) = tm v2 simpl.tm: type_map
v1, v2: var
t: type
H: v1 <> v2
(if v2 ==v v1 then Some t else tm v2) = tm v2
    unfold var_eq.tm: type_map
v1, v2: var
t: type
H: v1 <> v2
(if string_dec v2 v1 then Some t else tm v2) = tm v2 destruct (string_dec v2 v1); auto.tm: type_map
v1, v2: var
t: type
H: v1 <> v2
e: v2 = v1
Some t = tm v2
    exfalso.tm: type_map
v1, v2: var
t: type
H: v1 <> v2
e: v2 = v1
False apply H.tm: type_map
v1, v2: var
t: type
H: v1 <> v2
e: v2 = v1
v1 = v2 auto.
  Qed.
  Lemma tmap_shadow:
    forall tm v t1 t2 v',
      ((tm $+ (v, t1)) $+ (v, t2)) $? v' = (tm $+ (v, t2)) $? v'.forall (tm : type_map) (v : var) (t1 t2 : type)
  (v' : var),
((tm $+ (v, t1)) $+ (v, t2)) $? v' =
(tm $+ (v, t2)) $? v'
  Proof.forall (tm : type_map) (v : var) (t1 t2 : type)
  (v' : var),
((tm $+ (v, t1)) $+ (v, t2)) $? v' =
(tm $+ (v, t2)) $? v'
    intros tm v t1 t2 v'.tm: type_map
v: var
t1, t2: type
v': var
((tm $+ (v, t1)) $+ (v, t2)) $? v' =
(tm $+ (v, t2)) $? v'
    destruct (v' ==v v).tm: type_map
v: var
t1, t2: type
v': var
e: v' = v
((tm $+ (v, t1)) $+ (v, t2)) $? v' =
(tm $+ (v, t2)) $? v'
tm: type_map
v: var
t1, t2: type
v': var
n: v' <> v
((tm $+ (v, t1)) $+ (v, t2)) $? v' =
(tm $+ (v, t2)) $? v'
    +tm: type_map
v: var
t1, t2: type
v': var
e: v' = v
((tm $+ (v, t1)) $+ (v, t2)) $? v' =
(tm $+ (v, t2)) $? v' subst.tm: type_map
v: var
t1, t2: type
((tm $+ (v, t1)) $+ (v, t2)) $? v =
(tm $+ (v, t2)) $? v repeat rewrite tmap_gss.tm: type_map
v: var
t1, t2: type
Some t2 = Some t2 auto.
    +tm: type_map
v: var
t1, t2: type
v': var
n: v' <> v
((tm $+ (v, t1)) $+ (v, t2)) $? v' =
(tm $+ (v, t2)) $? v' repeat (rewrite tmap_gso; auto).
  Qed.
  Lemma tmap_permute:
    forall tm v1 t1 v2 t2 v',
      v1 <> v2 ->
      ((tm $+ (v1, t1)) $+ (v2, t2)) $? v' =
        ((tm $+ (v2, t2)) $+ (v1, t1)) $? v'.forall (tm : type_map) (v1 : var) (t1 : type)
  (v2 : var) (t2 : type) (v' : var),
v1 <> v2 ->
((tm $+ (v1, t1)) $+ (v2, t2)) $? v' =
((tm $+ (v2, t2)) $+ (v1, t1)) $? v'
  Proof.forall (tm : type_map) (v1 : var) (t1 : type)
  (v2 : var) (t2 : type) (v' : var),
v1 <> v2 ->
((tm $+ (v1, t1)) $+ (v2, t2)) $? v' =
((tm $+ (v2, t2)) $+ (v1, t1)) $? v'
    intros tm v1 t1 v2 t2 v' H.tm: type_map
v1: var
t1: type
v2: var
t2: type
v': var
H: v1 <> v2
((tm $+ (v1, t1)) $+ (v2, t2)) $? v' =
((tm $+ (v2, t2)) $+ (v1, t1)) $? v'
    destruct (v' ==v v1); destruct (v' ==v v2); subst.tm: type_map
t1: type
v2: var
t2: type
H: v2 <> v2
((tm $+ (v2, t1)) $+ (v2, t2)) $? v2 =
((tm $+ (v2, t2)) $+ (v2, t1)) $? v2
tm: type_map
v1: var
t1: type
v2: var
t2: type
H, n: v1 <> v2
((tm $+ (v1, t1)) $+ (v2, t2)) $? v1 =
((tm $+ (v2, t2)) $+ (v1, t1)) $? v1
tm: type_map
v1: var
t1: type
v2: var
t2: type
H: v1 <> v2
n: v2 <> v1
((tm $+ (v1, t1)) $+ (v2, t2)) $? v2 =
((tm $+ (v2, t2)) $+ (v1, t1)) $? v2
tm: type_map
v1: var
t1: type
v2: var
t2: type
v': var
H: v1 <> v2
n: v' <> v1
n0: v' <> v2
((tm $+ (v1, t1)) $+ (v2, t2)) $? v' =
((tm $+ (v2, t2)) $+ (v1, t1)) $? v'
    -tm: type_map
t1: type
v2: var
t2: type
H: v2 <> v2
((tm $+ (v2, t1)) $+ (v2, t2)) $? v2 =
((tm $+ (v2, t2)) $+ (v2, t1)) $? v2 exfalso.tm: type_map
t1: type
v2: var
t2: type
H: v2 <> v2
False apply H.tm: type_map
t1: type
v2: var
t2: type
H: v2 <> v2
v2 = v2 auto.
    -tm: type_map
v1: var
t1: type
v2: var
t2: type
H, n: v1 <> v2
((tm $+ (v1, t1)) $+ (v2, t2)) $? v1 =
((tm $+ (v2, t2)) $+ (v1, t1)) $? v1 rewrite tmap_gss.tm: type_map
v1: var
t1: type
v2: var
t2: type
H, n: v1 <> v2
((tm $+ (v1, t1)) $+ (v2, t2)) $? v1 = Some t1 rewrite tmap_gso; auto.tm: type_map
v1: var
t1: type
v2: var
t2: type
H, n: v1 <> v2
(tm $+ (v1, t1)) $? v1 = Some t1 apply tmap_gss.
    -tm: type_map
v1: var
t1: type
v2: var
t2: type
H: v1 <> v2
n: v2 <> v1
((tm $+ (v1, t1)) $+ (v2, t2)) $? v2 =
((tm $+ (v2, t2)) $+ (v1, t1)) $? v2 rewrite tmap_gss.tm: type_map
v1: var
t1: type
v2: var
t2: type
H: v1 <> v2
n: v2 <> v1
Some t2 = ((tm $+ (v2, t2)) $+ (v1, t1)) $? v2 rewrite tmap_gso; auto.tm: type_map
v1: var
t1: type
v2: var
t2: type
H: v1 <> v2
n: v2 <> v1
Some t2 = (tm $+ (v2, t2)) $? v2
      symmetry.tm: type_map
v1: var
t1: type
v2: var
t2: type
H: v1 <> v2
n: v2 <> v1
(tm $+ (v2, t2)) $? v2 = Some t2 apply tmap_gss.
    -tm: type_map
v1: var
t1: type
v2: var
t2: type
v': var
H: v1 <> v2
n: v' <> v1
n0: v' <> v2
((tm $+ (v1, t1)) $+ (v2, t2)) $? v' =
((tm $+ (v2, t2)) $+ (v1, t1)) $? v' repeat (rewrite tmap_gso; auto).
  Qed.

In one proof later, it will be convenient to talk about typing contexts being equal if they just map each variable to the same type option. But take the lemma above: although the two maps return the value for any var v', the two functions are not equal in the sense of Coq equality.

Ley's make a quick detour through functional extensionality.

  Module Ext.

Functional Extensionality

Coq's logic is quite minimalistic. This means that one occasionally encounters cases where translating standard mathematical reasoning into Coq is cumbersome -- or even impossible -- unless we enrich its core logic with additional axioms.

For example, the equality assertions that we have seen so far mostly have concerned elements of inductive types (nat, bool, etc.). But, since Coq's equality operator is polymorphic, we can use it at _any_ type -- in particular, we can write propositions claiming that two _functions_ are equal to each other:

Example function_equality_ex1 :
  (fun x => 3 + x) = (fun x => (pred 4) + x).(fun x : nat => 3 + x) =
(fun x : nat => Nat.pred 4 + x)
Proof.(fun x : nat => 3 + x) =
(fun x : nat => Nat.pred 4 + x) reflexivity. Qed.

These two functions are equal just by simplification, but in general functions can be equal for more interesting reasons.

In common mathematical practice, two functions are considered equal if they produce the same output on every input: This is known as the principle of functional extensionality.

Informally, an "extensional property" is one that pertains to an object's observable behavior. Thus, functional extensionality simply means that a function's identity is completely determined by what we can observe from it -- i.e., the results we obtain after applying it.

However, functional extensionality is not part of Coq's built-in logic. This means that some intuitively obvious propositions are not provable.

Example function_equality_ex2 :
  (fun x => plus x 1) = (fun x => plus 1 x).(fun x : nat => x + 1) = (fun x : nat => 1 + x)
Proof.(fun x : nat => x + 1) = (fun x : nat => 1 + x)
  simpl.(fun x : nat => x + 1) = (fun x : nat => S x)
  Fail rewrite PeanoNat.Nat.add_comm.The command has indeed failed with message:
Found no subterm matching "?M1090 + ?M1091"
in the current goal.
(fun x : nat => x + 1) = (fun x : nat => S x)
Abort.

However, if we like, we can add functional extensionality to Coq's core using the Axiom command.

Axiom functional_extensionality : forall {X Y: Type}
                                    {f g : X -> Y},
  (forall (x:X), f x = g x) -> f = g.

Defining something as an Axiom has the same effect as stating a theorem and skipping its proof using Admitted, but it alerts the reader that this isn't just something we're going to come back and fill in later!

We can now invoke functional extensionality in proofs:

Example function_equality_ex2 :
  (fun x => x + 1) = (fun x => 1 + x).(fun x : nat => x + 1) = (fun x : nat => 1 + x)
Proof.(fun x : nat => x + 1) = (fun x : nat => 1 + x)
  apply functional_extensionality.forall x : nat, x + 1 = 1 + x intros x.x: nat
x + 1 = 1 + x
  apply PeanoNat.Nat.add_comm.
Qed.

Coq provides a nice way to see on which axioms, parameters and admitted proofs each of your theorems depend on. For instance, it can show that the theorem function_equality_ex2 only depends on the functional extensionality axiom.

Print Assumptions function_equality_ex2.Axioms:
functional_extensionality :
  forall (X Y : Type) (f g : X -> Y),
  (forall x : X, f x = g x) -> f = g

Naturally, we need to be quite careful when adding new axioms into Coq's logic, as this can render it inconsistent -- that is, it may become possible to prove every proposition, including False, 2+2=5, etc.!

In general, there is no simple way of telling whether an axiom is safe to add: hard work by highly trained mathematicians is often required to establish the consistency of any particular combination of axioms.

Fortunately, it is known that adding functional extensionality, in particular, is consistent.

For this reason, it's available in the standard library (Logic.FunctionalExtensionality).

Other examples of known consistent axioms include the functional axiom of choice and proof irrelevance. See more details here https://github.com/coq/coq/wiki/The-Logic-of-Coq#axioms.

  End Ext.

  From Coq Require Import Logic.FunctionalExtensionality.Use of “Require” inside a module is fragile. It is not
recommended to use this functionality in finished
proof scripts. [require-in-module,fragile,default]
  Lemma tmap_permute_ext:
    forall tm v1 t1 v2 t2,
      v1 <> v2 ->
      (tm $+ (v1, t1)) $+ (v2, t2) = (tm $+ (v2, t2)) $+ (v1, t1).forall (tm : type_map) (v1 : var) (t1 : type)
  (v2 : var) (t2 : type),
v1 <> v2 ->
(tm $+ (v1, t1)) $+ (v2, t2) =
(tm $+ (v2, t2)) $+ (v1, t1)
  Proof.forall (tm : type_map) (v1 : var) (t1 : type)
  (v2 : var) (t2 : type),
v1 <> v2 ->
(tm $+ (v1, t1)) $+ (v2, t2) =
(tm $+ (v2, t2)) $+ (v1, t1)
    intros tm v1 t1 v2 t2 H.tm: type_map
v1: var
t1: type
v2: var
t2: type
H: v1 <> v2
(tm $+ (v1, t1)) $+ (v2, t2) =
(tm $+ (v2, t2)) $+ (v1, t1) apply functional_extensionality.tm: type_map
v1: var
t1: type
v2: var
t2: type
H: v1 <> v2
forall x : var,
((tm $+ (v1, t1)) $+ (v2, t2)) x =
((tm $+ (v2, t2)) $+ (v1, t1)) x
    intros x.tm: type_map
v1: var
t1: type
v2: var
t2: type
H: v1 <> v2
x: var
((tm $+ (v1, t1)) $+ (v2, t2)) x =
((tm $+ (v2, t2)) $+ (v1, t1)) x pose proof (tmap_permute tm v1 t1 v2 t2).tm: type_map
v1: var
t1: type
v2: var
t2: type
H: v1 <> v2
x: var
H0: forall v' : var,
v1 <> v2 ->
((tm $+ (v1, t1)) $+ (v2, t2)) $? v' =
((tm $+ (v2, t2)) $+ (v1, t1)) $? v'
((tm $+ (v1, t1)) $+ (v2, t2)) x =
((tm $+ (v2, t2)) $+ (v1, t1)) x
    unfold tmap_get in H0.tm: type_map
v1: var
t1: type
v2: var
t2: type
H: v1 <> v2
x: var
H0: forall v' : var,
v1 <> v2 ->
((tm $+ (v1, t1)) $+ (v2, t2)) v' =
((tm $+ (v2, t2)) $+ (v1, t1)) v'
((tm $+ (v1, t1)) $+ (v2, t2)) x =
((tm $+ (v2, t2)) $+ (v1, t1)) x auto.
  Qed.

Typing System

  Inductive has_ty : type_map -> exp -> type -> Prop :=
  | HtVar : forall G x t,
    G $? x = Some t
    -> has_ty G (Var x) t
  | HtConst : forall G n,
    has_ty G (Const n) Nat
  | HtPlus : forall G e1 e2,
    has_ty G e1 Nat
    -> has_ty G e2 Nat
    -> has_ty G (Plus e1 e2) Nat
  | HtAbs : forall G x e1 t1 t2,
    has_ty (G $+ (x, t1)) e1 t2
    -> has_ty G (Abs x e1) (Fun t1 t2)
  | HtApp : forall G e1 e2 t1 t2,
    has_ty G e1 (Fun t1 t2)
    -> has_ty G e2 t1
    -> has_ty G (App e1 e2) t2.

  Local Hint Constructors value step has_ty : core.

  (* some notation for the typing judgement *)
  Notation "Gamma '|--' e '\in' T" := (has_ty Gamma e T) (at level 101).
  Infix "-->" := Fun (at level 60, right associativity).

  (* Some examples of typed programs *)

  Example one_plus_one : $0 |-- (1 ^+^ 1) \in Nat.$0 |-- 1 ^+^ 1 \in Nat
  Proof.$0 |-- 1 ^+^ 1 \in Nat eauto. Qed.

  Example add :
    $0 |-- (\"n", \"m", "n" ^+^ "m") \in (Nat --> Nat --> Nat).$0 |-- \ "n", (\ "m", "n" ^+^ "m") \in
Nat --> Nat --> Nat
  Proof.$0 |-- \ "n", (\ "m", "n" ^+^ "m") \in
Nat --> Nat --> Nat
    repeat (econstructor; simpl).
  Qed.

  Example eleven : $0 |-- ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) \in Nat.$0 |-- (\ "n", (\ "m", "n" ^+^ "m")) @ 7 @ 4 \in Nat
  Proof.$0 |-- (\ "n", (\ "m", "n" ^+^ "m")) @ 7 @ 4 \in Nat
    repeat (econstructor; simpl).
  Qed.

  Example seven_the_long_way :
    $0 |-- ((\"x", "x") @ (\"x", "x") @ 7) \in Nat.$0 |-- (\ "x", "x") @ (\ "x", "x") @ 7 \in Nat
  Proof.$0 |-- (\ "x", "x") @ (\ "x", "x") @ 7 \in Nat
    repeat (econstructor; simpl).
  Qed.

Type Soundness

What useful invariants could we prove about programs in this language? How about that, at every point, either they're finished executing or they can take further steps? For instance, a program that tried to add a function to a number would not satisfy that condition, and we call it stuck. We want to prove that typed programs can never become stuck. Here's a good invariant to strive for.

  Definition unstuck e := value e
                          \/ (exists e' : exp, step e e').

We can now define some useful lemmas about typed values.

  Lemma val_nat:
    forall e,
      ($0 |-- e \in Nat) ->
      value e ->
      exists n, e = Const n.forall e : exp,
($0 |-- e \in Nat) -> value e -> exists n : nat, e = n
  Proof.forall e : exp,
($0 |-- e \in Nat) -> value e -> exists n : nat, e = n
    intros e H H0.e: exp
H: $0 |-- e \in Nat
H0: value e
exists n : nat, e = n inversion H0; subst; inversion H; subst.n: nat
H0: value n
H: $0 |-- n \in Nat
exists n0 : nat, n = n0 eauto.
  Qed.

  Lemma val_fun:
    forall e t1 t2,
      ($0 |-- e \in (t1 --> t2)) ->
      value e ->
      exists x u, e = \x, u.forall (e : exp) (t1 t2 : type),
($0 |-- e \in t1 --> t2) ->
value e -> exists (x : var) (u : exp), e = \ x, u
  Proof.forall (e : exp) (t1 t2 : type),
($0 |-- e \in t1 --> t2) ->
value e -> exists (x : var) (u : exp), e = \ x, u
    intros e t1 t2 H H0.e: exp
t1, t2: type
H: $0 |-- e \in t1 --> t2
H0: value e
exists (x : var) (u : exp), e = \ x, u inversion H0; subst; inversion H; subst.t1, t2: type
x: var
e1: exp
H0: value (\ x, e1)
H: $0 |-- \ x, e1 \in t1 --> t2
H3: $0 $+ (x, t1) |-- e1 \in t2
exists (x0 : var) (u : exp), \ x, e1 = \ x0, u eauto.
  Qed.

The progress theorem tells us that closed, well-typed terms are not stuck: either a well-typed term is a value, or it can take a reduction step.

  Lemma progress : forall e t,
      ($0 |-- e \in t) ->
      unstuck e.forall (e : exp) (t : type),
($0 |-- e \in t) -> unstuck e
  Proof.forall (e : exp) (t : type),
($0 |-- e \in t) -> unstuck e
    intros e t H.e: exp
t: type
H: $0 |-- e \in t
unstuck e remember empty_map as Gamma.e: exp
t: type
Gamma: type_map
HeqGamma: Gamma = $0
H: Gamma |-- e \in t
unstuck e unfold unstuck.e: exp
t: type
Gamma: type_map
HeqGamma: Gamma = $0
H: Gamma |-- e \in t
value e \/ (exists e' : exp, step e e')
    assert ($0 = $0) by auto.e: exp
t: type
Gamma: type_map
HeqGamma: Gamma = $0
H: Gamma |-- e \in t
H0: $0 = $0
value e \/ (exists e' : exp, step e e')
    induction H; subst G; auto.x: var
t: type
H: $0 $? x = Some t
H0: $0 = $0
value x \/ (exists e' : exp, step x e')
e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: $0 = $0 ->
value e2 \/ (exists e' : exp, step e2 e')
IHhas_ty1: $0 = $0 ->
value e1 \/ (exists e' : exp, step e1 e')
value (e1 ^+^ e2) \/
(exists e' : exp, step (e1 ^+^ e2) e')
e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: $0 = $0 ->
value e2 \/ (exists e' : exp, step e2 e')
IHhas_ty1: $0 = $0 ->
value e1 \/ (exists e' : exp, step e1 e')
value (e1 @ e2) \/
(exists e' : exp, step (e1 @ e2) e')
    -x: var
t: type
H: $0 $? x = Some t
H0: $0 = $0
value x \/ (exists e' : exp, step x e') unfold empty_map, tmap_get in H.x: var
t: type
H: None = Some t
H0: $0 = $0
value x \/ (exists e' : exp, step x e') inversion H.
    -e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: $0 = $0 ->
value e2 \/ (exists e' : exp, step e2 e')
IHhas_ty1: $0 = $0 ->
value e1 \/ (exists e' : exp, step e1 e')
value (e1 ^+^ e2) \/
(exists e' : exp, step (e1 ^+^ e2) e') right.e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: $0 = $0 ->
value e2 \/ (exists e' : exp, step e2 e')
IHhas_ty1: $0 = $0 ->
value e1 \/ (exists e' : exp, step e1 e')
exists e' : exp, step (e1 ^+^ e2) e' specialize (IHhas_ty1 H0).e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: $0 = $0 ->
value e2 \/ (exists e' : exp, step e2 e')
IHhas_ty1: value e1 \/ (exists e' : exp, step e1 e')
exists e' : exp, step (e1 ^+^ e2) e' specialize (IHhas_ty2 H0).e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
IHhas_ty1: value e1 \/ (exists e' : exp, step e1 e')
exists e' : exp, step (e1 ^+^ e2) e'
      destruct IHhas_ty1.e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
H2: value e1
exists e' : exp, step (e1 ^+^ e2) e'
e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
H2: exists e' : exp, step e1 e'
exists e' : exp, step (e1 ^+^ e2) e'
      2: {e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
H2: exists e' : exp, step e1 e'
exists e' : exp, step (e1 ^+^ e2) e' destruct H2.e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
x: exp
H2: step e1 x
exists e' : exp, step (e1 ^+^ e2) e' eexists.e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
x: exp
H2: step e1 x
step (e1 ^+^ e2) ?e' apply Plus1; eauto. }e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
H2: value e1
exists e' : exp, step (e1 ^+^ e2) e'
      destruct IHhas_ty2.e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
H3: value e2
H2: value e1
exists e' : exp, step (e1 ^+^ e2) e'
e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
H3: exists e' : exp, step e2 e'
H2: value e1
exists e' : exp, step (e1 ^+^ e2) e'
      +e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
H3: value e2
H2: value e1
exists e' : exp, step (e1 ^+^ e2) e' specialize (val_nat e1 H H2) as [n1 He1].e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
H3: value e2
H2: value e1
n1: nat
He1: e1 = n1
exists e' : exp, step (e1 ^+^ e2) e'
        specialize (val_nat e2 H1 H3) as [n2 He2].e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
H3: value e2
H2: value e1
n1: nat
He1: e1 = n1
n2: nat
He2: e2 = n2
exists e' : exp, step (e1 ^+^ e2) e'
        subst.n2: nat
H1: $0 |-- n2 \in Nat
n1: nat
H: $0 |-- n1 \in Nat
H0: $0 = $0
H3: value n2
H2: value n1
exists e' : exp, step (n1 ^+^ n2) e' eexists.n2: nat
H1: $0 |-- n2 \in Nat
n1: nat
H: $0 |-- n1 \in Nat
H0: $0 = $0
H3: value n2
H2: value n1
step (n1 ^+^ n2) ?e' apply Add.
      +e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
H3: exists e' : exp, step e2 e'
H2: value e1
exists e' : exp, step (e1 ^+^ e2) e' specialize (val_nat e1 H H2) as [n1 He1].e1, e2: exp
H1: $0 |-- e2 \in Nat
H: $0 |-- e1 \in Nat
H0: $0 = $0
H3: exists e' : exp, step e2 e'
H2: value e1
n1: nat
He1: e1 = n1
exists e' : exp, step (e1 ^+^ e2) e' subst.e2: exp
H1: $0 |-- e2 \in Nat
n1: nat
H: $0 |-- n1 \in Nat
H0: $0 = $0
H3: exists e' : exp, step e2 e'
H2: value n1
exists e' : exp, step (n1 ^+^ e2) e'
        destruct H3.e2: exp
H1: $0 |-- e2 \in Nat
n1: nat
H: $0 |-- n1 \in Nat
H0: $0 = $0
x: exp
H3: step e2 x
H2: value n1
exists e' : exp, step (n1 ^+^ e2) e' eexists.e2: exp
H1: $0 |-- e2 \in Nat
n1: nat
H: $0 |-- n1 \in Nat
H0: $0 = $0
x: exp
H3: step e2 x
H2: value n1
step (n1 ^+^ e2) ?e' apply Plus2; eauto.
    -e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: $0 = $0 ->
value e2 \/ (exists e' : exp, step e2 e')
IHhas_ty1: $0 = $0 ->
value e1 \/ (exists e' : exp, step e1 e')
value (e1 @ e2) \/
(exists e' : exp, step (e1 @ e2) e') right.e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: $0 = $0 ->
value e2 \/ (exists e' : exp, step e2 e')
IHhas_ty1: $0 = $0 ->
value e1 \/ (exists e' : exp, step e1 e')
exists e' : exp, step (e1 @ e2) e' specialize (IHhas_ty1 H0).e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: $0 = $0 ->
value e2 \/ (exists e' : exp, step e2 e')
IHhas_ty1: value e1 \/ (exists e' : exp, step e1 e')
exists e' : exp, step (e1 @ e2) e' specialize (IHhas_ty2 H0).e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
IHhas_ty1: value e1 \/ (exists e' : exp, step e1 e')
exists e' : exp, step (e1 @ e2) e'
      destruct IHhas_ty1.e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
H2: value e1
exists e' : exp, step (e1 @ e2) e'
e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
H2: exists e' : exp, step e1 e'
exists e' : exp, step (e1 @ e2) e'
      2: {e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
H2: exists e' : exp, step e1 e'
exists e' : exp, step (e1 @ e2) e' destruct H2.e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
x: exp
H2: step e1 x
exists e' : exp, step (e1 @ e2) e' eexists.e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
x: exp
H2: step e1 x
step (e1 @ e2) ?e' apply App1; eauto. }e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
IHhas_ty2: value e2 \/ (exists e' : exp, step e2 e')
H2: value e1
exists e' : exp, step (e1 @ e2) e'
      destruct IHhas_ty2.e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
H3: value e2
H2: value e1
exists e' : exp, step (e1 @ e2) e'
e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
H3: exists e' : exp, step e2 e'
H2: value e1
exists e' : exp, step (e1 @ e2) e'
      +e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
H3: value e2
H2: value e1
exists e' : exp, step (e1 @ e2) e' specialize (val_fun e1 _ _ H H2) as [x1 [u1 Hf1]].e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
H3: value e2
H2: value e1
x1: var
u1: exp
Hf1: e1 = \ x1, u1
exists e' : exp, step (e1 @ e2) e' subst.e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
x1: var
u1: exp
H: $0 |-- \ x1, u1 \in t1 --> t2
H0: $0 = $0
H3: value e2
H2: value (\ x1, u1)
exists e' : exp, step ((\ x1, u1) @ e2) e'
        eexists.e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
x1: var
u1: exp
H: $0 |-- \ x1, u1 \in t1 --> t2
H0: $0 = $0
H3: value e2
H2: value (\ x1, u1)
step ((\ x1, u1) @ e2) ?e' apply Beta; auto.
      +e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
H3: exists e' : exp, step e2 e'
H2: value e1
exists e' : exp, step (e1 @ e2) e' destruct H3.e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
x: exp
H3: step e2 x
H2: value e1
exists e' : exp, step (e1 @ e2) e' eexists.e1, e2: exp
t1, t2: type
H1: $0 |-- e2 \in t1
H: $0 |-- e1 \in t1 --> t2
H0: $0 = $0
x: exp
H3: step e2 x
H2: value e1
step (e1 @ e2) ?e' apply App2; eauto.
  Qed.

This could also be proved by induction on e (left as exercise).

The other half of the type soundness property is the preservation of types during reduction. For this part, we'll need to develop some technical machinery for reasoning about variables and substitution. Working from top to bottom (from the high-level property we are actually interested in to the lowest-level technical lemmas that are needed by various cases of the more interesting proofs), the story goes like this:

The preservation theorem is proved by induction on a typing derivation. There is one interesting case: the Beta-reduction. Its definition uses the substitution operation. 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 (well-typed) term for a variable in a term preserves the type of the term. The proof requires looking at all the different cases in the definition of substitition. This time, for the variables case, we discover that we need to deduce from the fact that a term x has type T in the empty context the fact that x has type T in every context. For this we prove a...
weakening lemma, showing that typing is preserved under "extensions" to the typing context.

To make Coq happy, of course, we need to formalize the story in the opposite order, starting with weakening...

Inclusion between typing contexts is preserved by adding the same new mapping to both.

  Lemma weakening_override : forall (G G' : type_map) x t,
    (forall x' t', G $? x' = Some t' -> G' $? x' = Some t')
    -> (forall x' t', G $+ (x, t) $? x' = Some t'
                      -> G' $+ (x, t) $? x' = Some t').forall (G G' : type_map) (x : var) (t : type),
(forall (x' : var) (t' : type),
 G $? x' = Some t' -> G' $? x' = Some t') ->
forall (x' : var) (t' : type),
(G $+ (x, t)) $? x' = Some t' ->
(G' $+ (x, t)) $? x' = Some t'
  Proof.forall (G G' : type_map) (x : var) (t : type),
(forall (x' : var) (t' : type),
 G $? x' = Some t' -> G' $? x' = Some t') ->
forall (x' : var) (t' : type),
(G $+ (x, t)) $? x' = Some t' ->
(G' $+ (x, t)) $? x' = Some t'
    intros G G' x t H x' t' H0.G, G': type_map
x: var
t: type
H: forall (x' : var) (t' : type),
G $? x' = Some t' -> G' $? x' = Some t'
x': var
t': type
H0: (G $+ (x, t)) $? x' = Some t'
(G' $+ (x, t)) $? x' = Some t'
    destruct (x ==v x'); simpl.G, G': type_map
x: var
t: type
H: forall (x' : var) (t' : type),
G $? x' = Some t' -> G' $? x' = Some t'
x': var
t': type
H0: (G $+ (x, t)) $? x' = Some t'
e: x = x'
(G' $+ (x, t)) $? x' = Some t'
G, G': type_map
x: var
t: type
H: forall (x' : var) (t' : type),
G $? x' = Some t' -> G' $? x' = Some t'
x': var
t': type
H0: (G $+ (x, t)) $? x' = Some t'
n: x <> x'
(G' $+ (x, t)) $? x' = Some t'
    -G, G': type_map
x: var
t: type
H: forall (x' : var) (t' : type),
G $? x' = Some t' -> G' $? x' = Some t'
x': var
t': type
H0: (G $+ (x, t)) $? x' = Some t'
e: x = x'
(G' $+ (x, t)) $? x' = Some t' subst.G, G': type_map
t: type
H: forall (x' : var) (t' : type),
G $? x' = Some t' -> G' $? x' = Some t'
x': var
t': type
H0: (G $+ (x', t)) $? x' = Some t'
(G' $+ (x', t)) $? x' = Some t' rewrite tmap_gss.G, G': type_map
t: type
H: forall (x' : var) (t' : type),
G $? x' = Some t' -> G' $? x' = Some t'
x': var
t': type
H0: (G $+ (x', t)) $? x' = Some t'
Some t = Some t' rewrite tmap_gss in H0.G, G': type_map
t: type
H: forall (x' : var) (t' : type),
G $? x' = Some t' -> G' $? x' = Some t'
x': var
t': type
H0: Some t = Some t'
Some t = Some t' auto.
    -G, G': type_map
x: var
t: type
H: forall (x' : var) (t' : type),
G $? x' = Some t' -> G' $? x' = Some t'
x': var
t': type
H0: (G $+ (x, t)) $? x' = Some t'
n: x <> x'
(G' $+ (x, t)) $? x' = Some t' rewrite tmap_gso; auto.G, G': type_map
x: var
t: type
H: forall (x' : var) (t' : type),
G $? x' = Some t' -> G' $? x' = Some t'
x': var
t': type
H0: (G $+ (x, t)) $? x' = Some t'
n: x <> x'
G' $? x' = Some t' rewrite tmap_gso in H0; auto.
  Qed.

This lemma lets us propagate a typing derivation into a new context that includes the old one.

  Lemma weakening : forall G e t,
      (G |-- e \in t)
    -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
      -> G' |-- e \in t.forall (G : type_map) (e : exp) (t : type),
(G |-- e \in t) ->
forall G' : type_map,
(forall (x : var) (t0 : type),
 G $? x = Some t0 -> G' $? x = Some t0) ->
G' |-- e \in t
  Proof.forall (G : type_map) (e : exp) (t : type),
(G |-- e \in t) ->
forall G' : type_map,
(forall (x : var) (t0 : type),
 G $? x = Some t0 -> G' $? x = Some t0) ->
G' |-- e \in t
    intros G e t H.G: type_map
e: exp
t: type
H: G |-- e \in t
forall G' : type_map,
(forall (x : var) (t : type),
 G $? x = Some t -> G' $? x = Some t) ->
G' |-- e \in t
    induction H; intros.G: type_map
x: var
t: type
H: G $? x = Some t
G': type_map
H0: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- x \in t
G: type_map
n: nat
G': type_map
H: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- n \in Nat
G: type_map
e1, e2: exp
H: G |-- e1 \in Nat
H0: G |-- e2 \in Nat
IHhas_ty1: forall G' : type_map,
(forall (x : var) (t : type),
 G $? x = Some t -> G' $? x = Some t) ->
G' |-- e1 \in Nat
IHhas_ty2: forall G' : type_map,
(forall (x : var) (t : type),
 G $? x = Some t -> G' $? x = Some t) ->
G' |-- e2 \in Nat
G': type_map
H1: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- e1 ^+^ e2 \in Nat
G: type_map
x: var
e1: exp
t1, t2: type
H: G $+ (x, t1) |-- e1 \in t2
IHhas_ty: forall G' : type_map,
(forall (x0 : var) (t : type),
 (G $+ (x, t1)) $? x0 = Some t ->
 G' $? x0 = Some t) -> 
G' |-- e1 \in t2
G': type_map
H0: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- \ x, e1 \in t1 --> t2
G: type_map
e1, e2: exp
t1, t2: type
H: G |-- e1 \in t1 --> t2
H0: G |-- e2 \in t1
IHhas_ty1: forall G' : type_map,
(forall (x : var) (t : type),
 G $? x = Some t -> G' $? x = Some t) ->
G' |-- e1 \in t1 --> t2
IHhas_ty2: forall G' : type_map,
(forall (x : var) (t : type),
 G $? x = Some t -> G' $? x = Some t) ->
G' |-- e2 \in t1
G': type_map
H1: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- e1 @ e2 \in t2
    -G: type_map
x: var
t: type
H: G $? x = Some t
G': type_map
H0: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- x \in t apply H0 in H.G: type_map
x: var
t: type
G': type_map
H: G' $? x = Some t
H0: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- x \in t constructor.G: type_map
x: var
t: type
G': type_map
H: G' $? x = Some t
H0: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' $? x = Some t auto.
    -G: type_map
n: nat
G': type_map
H: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- n \in Nat constructor.
    -G: type_map
e1, e2: exp
H: G |-- e1 \in Nat
H0: G |-- e2 \in Nat
IHhas_ty1: forall G' : type_map,
(forall (x : var) (t : type),
 G $? x = Some t -> G' $? x = Some t) ->
G' |-- e1 \in Nat
IHhas_ty2: forall G' : type_map,
(forall (x : var) (t : type),
 G $? x = Some t -> G' $? x = Some t) ->
G' |-- e2 \in Nat
G': type_map
H1: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- e1 ^+^ e2 \in Nat constructor; auto.
    -G: type_map
x: var
e1: exp
t1, t2: type
H: G $+ (x, t1) |-- e1 \in t2
IHhas_ty: forall G' : type_map,
(forall (x0 : var) (t : type),
 (G $+ (x, t1)) $? x0 = Some t ->
 G' $? x0 = Some t) -> 
G' |-- e1 \in t2
G': type_map
H0: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- \ x, e1 \in t1 --> t2 constructor.G: type_map
x: var
e1: exp
t1, t2: type
H: G $+ (x, t1) |-- e1 \in t2
IHhas_ty: forall G' : type_map,
(forall (x0 : var) (t : type),
 (G $+ (x, t1)) $? x0 = Some t ->
 G' $? x0 = Some t) -> 
G' |-- e1 \in t2
G': type_map
H0: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' $+ (x, t1) |-- e1 \in t2 apply IHhas_ty.G: type_map
x: var
e1: exp
t1, t2: type
H: G $+ (x, t1) |-- e1 \in t2
IHhas_ty: forall G' : type_map,
(forall (x0 : var) (t : type),
 (G $+ (x, t1)) $? x0 = Some t ->
 G' $? x0 = Some t) -> 
G' |-- e1 \in t2
G': type_map
H0: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
forall (x0 : var) (t : type),
(G $+ (x, t1)) $? x0 = Some t ->
(G' $+ (x, t1)) $? x0 = Some t
      apply weakening_override.G: type_map
x: var
e1: exp
t1, t2: type
H: G $+ (x, t1) |-- e1 \in t2
IHhas_ty: forall G' : type_map,
(forall (x0 : var) (t : type),
 (G $+ (x, t1)) $? x0 = Some t ->
 G' $? x0 = Some t) -> 
G' |-- e1 \in t2
G': type_map
H0: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
forall (x' : var) (t' : type),
G $? x' = Some t' -> G' $? x' = Some t' auto.
    -G: type_map
e1, e2: exp
t1, t2: type
H: G |-- e1 \in t1 --> t2
H0: G |-- e2 \in t1
IHhas_ty1: forall G' : type_map,
(forall (x : var) (t : type),
 G $? x = Some t -> G' $? x = Some t) ->
G' |-- e1 \in t1 --> t2
IHhas_ty2: forall G' : type_map,
(forall (x : var) (t : type),
 G $? x = Some t -> G' $? x = Some t) ->
G' |-- e2 \in t1
G': type_map
H1: forall (x : var) (t : type),
G $? x = Some t -> G' $? x = Some t
G' |-- e1 @ e2 \in t2 econstructor; auto.
  Qed.

  Corollary empty_weakening:
    forall tm e t,
      ($0 |-- e \in t) ->
      tm |-- e \in t.forall (tm : type_map) (e : exp) (t : type),
($0 |-- e \in t) -> tm |-- e \in t
  Proof.forall (tm : type_map) (e : exp) (t : type),
($0 |-- e \in t) -> tm |-- e \in t
    intros tm e t H.tm: type_map
e: exp
t: type
H: $0 |-- e \in t
tm |-- e \in t eapply weakening; eauto.tm: type_map
e: exp
t: type
H: $0 |-- e \in t
forall (x : var) (t : type),
$0 $? x = Some t -> tm $? x = Some t
    intros x t0 H0.tm: type_map
e: exp
t: type
H: $0 |-- e \in t
x: var
t0: type
H0: $0 $? x = Some t0
tm $? x = Some t0 unfold empty_map, tmap_get in H0.tm: type_map
e: exp
t: type
H: $0 |-- e \in t
x: var
t0: type
H0: None = Some t0
tm $? x = Some t0
    inversion H0.
  Qed.

Replacing a variable with a properly typed term preserves typing.

  Lemma substitution : forall G x t' e t e',
      ((G $+ (x, t')) |-- e \in t) ->
      ($0 |-- e' \in t') ->
      G |-- (subst e' x e) \in t.forall (G : type_map) (x : var) (t' : type) (e : exp)
  (t : type) (e' : exp),
(G $+ (x, t') |-- e \in t) ->
($0 |-- e' \in t') -> G |-- subst e' x e \in t
  Proof.forall (G : type_map) (x : var) (t' : type) (e : exp)
  (t : type) (e' : exp),
(G $+ (x, t') |-- e \in t) ->
($0 |-- e' \in t') -> G |-- subst e' x e \in t
    intros G x t' e t e' H.G: type_map
x: var
t': type
e: exp
t: type
e': exp
H: G $+ (x, t') |-- e \in t
($0 |-- e' \in t') -> G |-- subst e' x e \in t
    remember (G $+ (x, t')) as G'.G: type_map
x: var
t': type
e: exp
t: type
e': exp
G': var -> option type
HeqG': G' = G $+ (x, t')
H: G' |-- e \in t
($0 |-- e' \in t') -> G |-- subst e' x e \in t
    generalize dependent G.x: var
t': type
e: exp
t: type
e': exp
G': var -> option type
H: G' |-- e \in t
forall G : type_map,
G' = G $+ (x, t') ->
($0 |-- e' \in t') -> G |-- subst e' x e \in t
    induction H; intros; simpl; eauto; subst.x: var
t': type
e': exp
x0: var
t: type
G0: type_map
H: (G0 $+ (x, t')) $? x0 = Some t
H0: $0 |-- e' \in t'
G0 |-- if x0 ==v x then e' else x0 \in t
x: var
t': type
e': exp
x0: var
e1: exp
t1, t2: type
G0: type_map
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x0, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H: (G0 $+ (x, t')) $+ (x0, t1) |-- e1 \in t2
H0: $0 |-- e' \in t'
G0
|-- \ x0, (if x0 ==v x then e1 else subst e' x e1) \in
t1 --> t2
    -x: var
t': type
e': exp
x0: var
t: type
G0: type_map
H: (G0 $+ (x, t')) $? x0 = Some t
H0: $0 |-- e' \in t'
G0 |-- if x0 ==v x then e' else x0 \in t destruct (x0 ==v x).x: var
t': type
e': exp
x0: var
t: type
G0: type_map
H: (G0 $+ (x, t')) $? x0 = Some t
H0: $0 |-- e' \in t'
e: x0 = x
G0 |-- e' \in t
x: var
t': type
e': exp
x0: var
t: type
G0: type_map
H: (G0 $+ (x, t')) $? x0 = Some t
H0: $0 |-- e' \in t'
n: x0 <> x
G0 |-- x0 \in t
      +x: var
t': type
e': exp
x0: var
t: type
G0: type_map
H: (G0 $+ (x, t')) $? x0 = Some t
H0: $0 |-- e' \in t'
e: x0 = x
G0 |-- e' \in t subst.x: var
t': type
e': exp
t: type
G0: type_map
H: (G0 $+ (x, t')) $? x = Some t
H0: $0 |-- e' \in t'
G0 |-- e' \in t rewrite tmap_gss in H.x: var
t': type
e': exp
t: type
G0: type_map
H: Some t' = Some t
H0: $0 |-- e' \in t'
G0 |-- e' \in t inversion H.x: var
t': type
e': exp
t: type
G0: type_map
H: Some t' = Some t
H0: $0 |-- e' \in t'
H2: t' = t
G0 |-- e' \in t subst.x: var
e': exp
t: type
G0: type_map
H0: $0 |-- e' \in t
H: Some t = Some t
G0 |-- e' \in t
        eapply empty_weakening; eauto.
      +x: var
t': type
e': exp
x0: var
t: type
G0: type_map
H: (G0 $+ (x, t')) $? x0 = Some t
H0: $0 |-- e' \in t'
n: x0 <> x
G0 |-- x0 \in t rewrite tmap_gso in H; auto.
    -x: var
t': type
e': exp
x0: var
e1: exp
t1, t2: type
G0: type_map
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x0, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H: (G0 $+ (x, t')) $+ (x0, t1) |-- e1 \in t2
H0: $0 |-- e' \in t'
G0
|-- \ x0, (if x0 ==v x then e1 else subst e' x e1) \in
t1 --> t2 destruct (x0 ==v x).x: var
t': type
e': exp
x0: var
e1: exp
t1, t2: type
G0: type_map
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x0, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H: (G0 $+ (x, t')) $+ (x0, t1) |-- e1 \in t2
H0: $0 |-- e' \in t'
e: x0 = x
G0 |-- \ x0, e1 \in t1 --> t2
x: var
t': type
e': exp
x0: var
e1: exp
t1, t2: type
G0: type_map
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x0, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H: (G0 $+ (x, t')) $+ (x0, t1) |-- e1 \in t2
H0: $0 |-- e' \in t'
n: x0 <> x
G0 |-- \ x0, subst e' x e1 \in t1 --> t2
      +x: var
t': type
e': exp
x0: var
e1: exp
t1, t2: type
G0: type_map
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x0, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H: (G0 $+ (x, t')) $+ (x0, t1) |-- e1 \in t2
H0: $0 |-- e' \in t'
e: x0 = x
G0 |-- \ x0, e1 \in t1 --> t2 subst.x: var
t': type
e', e1: exp
t1, t2: type
G0: type_map
H: (G0 $+ (x, t')) $+ (x, t1) |-- e1 \in t2
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H0: $0 |-- e' \in t'
G0 |-- \ x, e1 \in t1 --> t2 constructor.x: var
t': type
e', e1: exp
t1, t2: type
G0: type_map
H: (G0 $+ (x, t')) $+ (x, t1) |-- e1 \in t2
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H0: $0 |-- e' \in t'
G0 $+ (x, t1) |-- e1 \in t2
        eapply weakening; eauto.x: var
t': type
e', e1: exp
t1, t2: type
G0: type_map
H: (G0 $+ (x, t')) $+ (x, t1) |-- e1 \in t2
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H0: $0 |-- e' \in t'
forall (x0 : var) (t : type),
((G0 $+ (x, t')) $+ (x, t1)) $? x0 = Some t ->
(G0 $+ (x, t1)) $? x0 = Some t
        intros x0 t H1.x: var
t': type
e', e1: exp
t1, t2: type
G0: type_map
H: (G0 $+ (x, t')) $+ (x, t1) |-- e1 \in t2
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H0: $0 |-- e' \in t'
x0: var
t: type
H1: ((G0 $+ (x, t')) $+ (x, t1)) $? x0 = Some t
(G0 $+ (x, t1)) $? x0 = Some t rewrite tmap_shadow in H1.x: var
t': type
e', e1: exp
t1, t2: type
G0: type_map
H: (G0 $+ (x, t')) $+ (x, t1) |-- e1 \in t2
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H0: $0 |-- e' \in t'
x0: var
t: type
H1: (G0 $+ (x, t1)) $? x0 = Some t
(G0 $+ (x, t1)) $? x0 = Some t auto.
      +x: var
t': type
e': exp
x0: var
e1: exp
t1, t2: type
G0: type_map
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x0, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H: (G0 $+ (x, t')) $+ (x0, t1) |-- e1 \in t2
H0: $0 |-- e' \in t'
n: x0 <> x
G0 |-- \ x0, subst e' x e1 \in t1 --> t2 apply HtAbs.x: var
t': type
e': exp
x0: var
e1: exp
t1, t2: type
G0: type_map
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x0, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H: (G0 $+ (x, t')) $+ (x0, t1) |-- e1 \in t2
H0: $0 |-- e' \in t'
n: x0 <> x
G0 $+ (x0, t1) |-- subst e' x e1 \in t2 apply IHhas_ty; auto.x: var
t': type
e': exp
x0: var
e1: exp
t1, t2: type
G0: type_map
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x0, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H: (G0 $+ (x, t')) $+ (x0, t1) |-- e1 \in t2
H0: $0 |-- e' \in t'
n: x0 <> x
(G0 $+ (x, t')) $+ (x0, t1) =
(G0 $+ (x0, t1)) $+ (x, t')
        apply functional_extensionality.x: var
t': type
e': exp
x0: var
e1: exp
t1, t2: type
G0: type_map
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x0, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H: (G0 $+ (x, t')) $+ (x0, t1) |-- e1 \in t2
H0: $0 |-- e' \in t'
n: x0 <> x
forall x1 : var,
((G0 $+ (x, t')) $+ (x0, t1)) x1 =
((G0 $+ (x0, t1)) $+ (x, t')) x1
        intros x1.x: var
t': type
e': exp
x0: var
e1: exp
t1, t2: type
G0: type_map
IHhas_ty: forall G : type_map,
(G0 $+ (x, t')) $+ (x0, t1) = G $+ (x, t') ->
($0 |-- e' \in t') ->
G |-- subst e' x e1 \in t2
H: (G0 $+ (x, t')) $+ (x0, t1) |-- e1 \in t2
H0: $0 |-- e' \in t'
n: x0 <> x
x1: var
((G0 $+ (x, t')) $+ (x0, t1)) x1 =
((G0 $+ (x0, t1)) $+ (x, t')) x1 rewrite tmap_permute_ext; auto.
Qed.

The actual preservation lemma:

  Lemma preservation : forall e1 e2,
    step e1 e2
    -> forall t, ($0 |-- e1 \in t)
      -> $0 |-- e2 \in t.forall e1 e2 : exp,
step e1 e2 ->
forall t : type, ($0 |-- e1 \in t) -> $0 |-- e2 \in t
  Proof.forall e1 e2 : exp,
step e1 e2 ->
forall t : type, ($0 |-- e1 \in t) -> $0 |-- e2 \in t
    intros e1 e2 H.e1, e2: exp
H: step e1 e2
forall t : type, ($0 |-- e1 \in t) -> $0 |-- e2 \in t
    remember empty_map as Gamma.e1, e2: exp
H: step e1 e2
Gamma: type_map
HeqGamma: Gamma = $0
forall t : type,
(Gamma |-- e1 \in t) -> Gamma |-- e2 \in t
    induction H; intros; simpl; subst.x: var
e, v: exp
H: value v
t: type
H0: $0 |-- (\ x, e) @ v \in t
$0 |-- subst v x e \in t
n1, n2: nat
t: type
H: $0 |-- n1 ^+^ n2 \in t
$0 |-- n1 + n2 \in t
e1, e1', e2: exp
H: step e1 e1'
IHstep: forall t : type,
($0 |-- e1 \in t) -> $0 |-- e1' \in t
t: type
H0: $0 |-- e1 @ e2 \in t
$0 |-- e1' @ e2 \in t
v, e2, e2': exp
H: value v
H0: step e2 e2'
IHstep: forall t : type,
($0 |-- e2 \in t) -> $0 |-- e2' \in t
t: type
H1: $0 |-- v @ e2 \in t
$0 |-- v @ e2' \in t
e1, e1', e2: exp
H: step e1 e1'
IHstep: forall t : type,
($0 |-- e1 \in t) -> $0 |-- e1' \in t
t: type
H0: $0 |-- e1 ^+^ e2 \in t
$0 |-- e1' ^+^ e2 \in t
v, e2, e2': exp
H: value v
H0: step e2 e2'
IHstep: forall t : type,
($0 |-- e2 \in t) -> $0 |-- e2' \in t
t: type
H1: $0 |-- v ^+^ e2 \in t
$0 |-- v ^+^ e2' \in t
    2-6: match goal with
         | [ H: has_ty _ _ _ |- _ ] =>
             inversion H; subst; econstructor; eauto
      end.x: var
e, v: exp
H: value v
t: type
H0: $0 |-- (\ x, e) @ v \in t
$0 |-- subst v x e \in t
    inversion H0; subst.x: var
e, v: exp
H: value v
t: type
H0: $0 |-- (\ x, e) @ v \in t
t1: type
H4: $0 |-- \ x, e \in t1 --> t
H6: $0 |-- v \in t1
$0 |-- subst v x e \in t inversion H4; subst.x: var
e, v: exp
H: value v
t: type
H0: $0 |-- (\ x, e) @ v \in t
t1: type
H4: $0 |-- \ x, e \in t1 --> t
H6: $0 |-- v \in t1
H3: $0 $+ (x, t1) |-- e \in t
$0 |-- subst v x e \in t
    eapply substitution; eauto.
  Qed.

Multi-step Soundness

Putting progress and preservation together, we see that a well-typed term can never reach a stuck state.

  Inductive trc {A:Type} {R:A -> A -> Prop}: A -> A -> Prop :=
  | TrcRefl : forall x, trc x x
  | TrcFront : forall x y z
    (STEP: R x y)
    (STAR: trc y z),
      trc x z.

  Local Hint Resolve TrcRefl TrcFront : core.

  Notation "R ^*" := (@trc _ R) (at level 0).

  Corollary multi_step_soundness :
    forall t t' T,
      ($0 |-- t \in T) ->
      step^* t t' ->
      unstuck t'.forall (t t' : exp) (T : type),
($0 |-- t \in T) -> (step) ^* t t' -> unstuck t'
  Proof.forall (t t' : exp) (T : type),
($0 |-- t \in T) -> (step) ^* t t' -> unstuck t'
    intros t t' T HT P.t, t': exp
T: type
HT: $0 |-- t \in T
P: (step) ^* t t'
unstuck t' induction P.T: type
x: exp
HT: $0 |-- x \in T
unstuck x
T: type
x: exp
HT: $0 |-- x \in T
y, z: exp
STEP: step x y
P: (step) ^* y z
IHP: ($0 |-- y \in T) -> unstuck z
unstuck z
    -T: type
x: exp
HT: $0 |-- x \in T
unstuck x apply progress in HT.T: type
x: exp
HT: unstuck x
unstuck x auto.
    -T: type
x: exp
HT: $0 |-- x \in T
y, z: exp
STEP: step x y
P: (step) ^* y z
IHP: ($0 |-- y \in T) -> unstuck z
unstuck z apply IHP.T: type
x: exp
HT: $0 |-- x \in T
y, z: exp
STEP: step x y
P: (step) ^* y z
IHP: ($0 |-- y \in T) -> unstuck z
$0 |-- y \in T
      eapply preservation; eauto.
  Qed.

Subject Expansion

The preservation theorem is often called subject reduction, because it tells us what happens when the "subject" of the typing relation is reduced.

Another property of some type systems is called Subject Expansion. Informally, it means that, if t steps to t' and $0 |-- t' \in T, then $0 |-- t \in T.

Is that the case for STLC?

Theorem not_subject_expansion:
  exists t t' T,
    step t t' /\
      ($0 |-- t' \in T) /\
      ~ ($0 |-- t \in T).exists (t t' : exp) (T : type),
  step t t' /\ ($0 |-- t' \in T) /\ ~ ($0 |-- t \in T)
Proof.exists (t t' : exp) (T : type),
  step t t' /\ ($0 |-- t' \in T) /\ ~ ($0 |-- t \in T)
  exists ((\"x", 0) @ (\"y", 0 @ 1)).exists (t' : exp) (T : type),
  step ((\ "x", 0) @ (\ "y", 0 @ 1)) t' /\
  ($0 |-- t' \in T) /\
  ~ ($0 |-- (\ "x", 0) @ (\ "y", 0 @ 1) \in T)
  exists (0).exists T : type,
  step ((\ "x", 0) @ (\ "y", 0 @ 1)) 0 /\
  ($0 |-- 0 \in T) /\
  ~ ($0 |-- (\ "x", 0) @ (\ "y", 0 @ 1) \in T)
  exists Nat.step ((\ "x", 0) @ (\ "y", 0 @ 1)) 0 /\
($0 |-- 0 \in Nat) /\
~ ($0 |-- (\ "x", 0) @ (\ "y", 0 @ 1) \in Nat)
  repeat split.step ((\ "x", 0) @ (\ "y", 0 @ 1)) 0
$0 |-- 0 \in Nat
~ ($0 |-- (\ "x", 0) @ (\ "y", 0 @ 1) \in Nat)
  -step ((\ "x", 0) @ (\ "y", 0 @ 1)) 0 constructor.value (\ "y", 0 @ 1) constructor.
  -$0 |-- 0 \in Nat constructor.
  -~ ($0 |-- (\ "x", 0) @ (\ "y", 0 @ 1) \in Nat) unfold not.($0 |-- (\ "x", 0) @ (\ "y", 0 @ 1) \in Nat) -> False intros H.H: $0 |-- (\ "x", 0) @ (\ "y", 0 @ 1) \in Nat
False
    inversion H; subst.H: $0 |-- (\ "x", 0) @ (\ "y", 0 @ 1) \in Nat
t1: type
H3: $0 |-- \ "x", 0 \in t1 --> Nat
H5: $0 |-- \ "y", 0 @ 1 \in t1
False
    inversion H5; subst.H: $0 |-- (\ "x", 0) @ (\ "y", 0 @ 1) \in Nat
t0, t2: type
H5: $0 |-- \ "y", 0 @ 1 \in t0 --> t2
H3: $0 |-- \ "x", 0 \in (t0 --> t2) --> Nat
H6: $0 $+ ("y", t0) |-- 0 @ 1 \in t2
False
    inversion H6; subst.H: $0 |-- (\ "x", 0) @ (\ "y", 0 @ 1) \in Nat
t0, t2: type
H5: $0 |-- \ "y", 0 @ 1 \in t0 --> t2
H3: $0 |-- \ "x", 0 \in (t0 --> t2) --> Nat
H6: $0 $+ ("y", t0) |-- 0 @ 1 \in t2
t1: type
H4: $0 $+ ("y", t0) |-- 0 \in t1 --> t2
H8: $0 $+ ("y", t0) |-- 1 \in t1
False
    inversion H4; subst.
Qed.

End Stlc.

We now go back to untyped lambda calculus without natural numbers and prove that we can encode natural numbers.

Module Ulc.

  Inductive exp : Set :=
  | Var (x : var)
  | Abs (x : var) (body : exp)
  | App (e1 e2 : exp).

  Fixpoint subst (rep : exp) (x : var) (e : exp) : exp :=
    match e with
    | Var y => if y ==v x then rep else Var y
    | Abs y e1 => Abs y (if y ==v x then e1 else subst rep x e1)
    | App e1 e2 => App (subst rep x e1) (subst rep x e2)
    end.

This time, for a change, we'll define big-step semantics.

  Inductive eval : exp -> exp -> Prop :=
  | BigAbs : forall x e,
    eval (Abs x e) (Abs x e)
  | BigApp : forall e1 x e1' e2 v2 v,
    eval e1 (Abs x e1')
    -> eval e2 v2
    -> eval (subst v2 x e1') v
    -> eval (App e1 e2) v.

Note that we omit a Var case, since variable terms can't be closed, and therefore they aren't meaningful as top-level programs.

  Inductive value : exp -> Prop :=
  | Value : forall x e, value (Abs x e).

  Local Hint Constructors eval value : core.

Every value executes to itself, and eval only produces values.

  Theorem value_eval : forall v,
    value v
    -> eval v v.forall v : exp, value v -> eval v v
  Proof.forall v : exp, value v -> eval v v
    intros v H.v: exp
H: value v
eval v v inversion H.v: exp
H: value v
x: var
e: exp
H0: Abs x e = v
eval (Abs x e) (Abs x e) auto.
  Qed.

  Local Hint Resolve value_eval : core.

  Theorem eval_value : forall e v,
    eval e v
    -> value v.forall e v : exp, eval e v -> value v
  Proof.forall e v : exp, eval e v -> value v
    intros e v H.e, v: exp
H: eval e v
value v induction H; auto.
  Qed.

  Local Hint Resolve eval_value : core.

  Coercion Var : var >-> exp.
  Notation "\ x , e" := (Abs x e) (at level 50).
  Infix "@" := App (at level 49, left associativity).

Church numerals

Here are two curious definitions.

  Definition zero := \"f", \"x", "x".
  Definition plus1 := \"n", \"f", \"x", "f" @ ("n" @ "f" @ "x").

We can build up any natural number n as plus1^n @ zero. Let's prove that, in fact, these definitions constitute a workable embedding of the natural numbers in lambda-calculus.

A term plus^n @ zero evaluates to something very close to what this function returns.

  Fixpoint canonical' (n : nat) : exp :=
    match n with
    | O => "x"
    | S n' => "f" @ ((\"f", \"x", canonical' n') @ "f" @ "x")
    end.

This missing piece is this wrapper.

  Definition canonical n := \"f", \"x", canonical' n.

Exercise: Represents

Let's formalize our definition of what it means to represent a number.

  Definition represents (e : exp) (n : nat) :=
    eval e (canonical n).

  Theorem zero_ok : represents zero 0.represents zero 0

Solution

  Proof.represents zero 0
    unfold zero, represents, canonical.eval (\ "f", (\ "x", "x"))
  (\ "f", (\ "x", canonical' 0))
    simpl.eval (\ "f", (\ "x", "x")) (\ "f", (\ "x", "x"))
    econstructor.
  Qed.

  Theorem plus1_ok :
    forall e n, represents e n ->
           represents (plus1 @ e) (S n).forall (e : exp) (n : nat),
represents e n -> represents (plus1 @ e) (S n)

Solution

  Proof.forall (e : exp) (n : nat),
represents e n -> represents (plus1 @ e) (S n)
    unfold plus1, represents, canonical; simpl.forall (e : exp) (n : nat),
eval e (\ "f", (\ "x", canonical' n)) ->
eval
  ((\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
   e)
  (\ "f",
   (\ "x",
    "f" @ ((\ "f", (\ "x", canonical' n)) @ "f" @ "x")))
    econstructor.e: exp
n: nat
H: eval e (\ "f", (\ "x", canonical' n))
eval
  (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
  (\ ?x, ?e1')
e: exp
n: nat
H: eval e (\ "f", (\ "x", canonical' n))
eval e ?v2
e: exp
n: nat
H: eval e (\ "f", (\ "x", canonical' n))
eval (subst ?v2 ?x ?e1')
  (\ "f",
   (\ "x",
    "f" @ ((\ "f", (\ "x", canonical' n)) @ "f" @ "x")))
    econstructor.e: exp
n: nat
H: eval e (\ "f", (\ "x", canonical' n))
eval e ?v2
e: exp
n: nat
H: eval e (\ "f", (\ "x", canonical' n))
eval
  (subst ?v2 "n"
     (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
  (\ "f",
   (\ "x",
    "f" @ ((\ "f", (\ "x", canonical' n)) @ "f" @ "x")))
    eassumption.e: exp
n: nat
H: eval e (\ "f", (\ "x", canonical' n))
eval
  (subst (\ "f", (\ "x", canonical' n)) "n"
     (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
  (\ "f",
   (\ "x",
    "f" @ ((\ "f", (\ "x", canonical' n)) @ "f" @ "x")))
    simpl.e: exp
n: nat
H: eval e (\ "f", (\ "x", canonical' n))
eval
  (\ "f",
   (\ "x",
    "f" @ ((\ "f", (\ "x", canonical' n)) @ "f" @ "x")))
  (\ "f",
   (\ "x",
    "f" @ ((\ "f", (\ "x", canonical' n)) @ "f" @ "x")))
    econstructor.
  Qed.

Exercise: add

What's basically going on here? The representation of number n is N such that, for any function f: N(f) = f^n. That is, we represent a number as its repeated-composition operator. So, given a number, we can use it to repeat any operation. In particular, to implement addition, we can just repeat plus1!

  Definition add := \"n", \"m", "n" @ plus1 @ "m".

  Example add_1_2 : exists v,
      eval (add @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v
      /\ eval (plus1 @ (plus1 @ (plus1 @ zero))) v.exists v : exp,
  eval
    (add @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero)))
    v /\ eval (plus1 @ (plus1 @ (plus1 @ zero))) v

Solution

  Proof.exists v : exp,
  eval
    (add @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero)))
    v /\ eval (plus1 @ (plus1 @ (plus1 @ zero))) v
    eexists; split.eval (add @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero)))
  ?v
eval (plus1 @ (plus1 @ (plus1 @ zero))) ?v
    repeat (econstructor; simpl).eval (plus1 @ (plus1 @ (plus1 @ zero)))
  (\ "f",
   (if "f" ==v "n"
    then \ "x", "f" @ ("n" @ "f" @ "x")
    else
     (fix subst
        (rep : exp) (x : var) (e : exp) {struct e} :
          exp :=
        match e with
        | Var y => if y ==v x then rep else y
        | \ y, e1 =>
            \ y,
            (if y ==v x then e1 else subst rep x e1)
        | e1 @ e2 => subst rep x e1 @ subst rep x e2
        end)
       (\ "f",
        (\ "x",
         "f" @
         ((\ "f",
           (\ "x",
            "f" @ ((\ "f", (\ "x", "x")) @ "f" @ "x"))) @
          "f" @ "x"))) "n"
       (\ "x", "f" @ ("n" @ "f" @ "x"))))
    repeat econstructor.
  Qed.

Exercise: Substitution of m

By the way: since canonical' doesn't mention variable m, substituting for m has no effect. This fact will come in handy shortly.

  Lemma subst_m_canonical' : forall n m,
    subst m "m" (canonical' n) = canonical' n.forall (n : nat) (m : exp),
subst m "m" (canonical' n) = canonical' n

Solution

  Proof.forall (n : nat) (m : exp),
subst m "m" (canonical' n) = canonical' n
    intros n.n: nat
forall m : exp,
subst m "m" (canonical' n) = canonical' n
    induction n; intros; simpl; auto.n: nat
IHn: forall m : exp, subst m "m" (canonical' n) = canonical' n
m: exp
"f" @
((\ "f", (\ "x", subst m "m" (canonical' n))) @ "f" @
 "x") =
"f" @ ((\ "f", (\ "x", canonical' n)) @ "f" @ "x")
    rewrite IHn.n: nat
IHn: forall m : exp, subst m "m" (canonical' n) = canonical' n
m: exp
"f" @ ((\ "f", (\ "x", canonical' n)) @ "f" @ "x") =
"f" @ ((\ "f", (\ "x", canonical' n)) @ "f" @ "x") auto.
  Qed.

Exercise: add_ok

This inductive proof is the workhorse for the next result, so let's skip ahead there.

  Lemma add_ok' : forall n m,
eval
  (subst (\ "f", (\ "x", canonical' m)) "x"
     (subst (\ "n", (\ "f", (\ "x", "f" @ (("n" @ "f") @ "x")))) "f"
        (canonical' n))) (canonical (n + m)).forall n m : nat,
eval
  (subst (\ "f", (\ "x", canonical' m)) "x"
     (subst
        (\ "n",
         (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
        "f" (canonical' n))) (canonical (n + m))

Solution

  Proof.forall n m : nat,
eval
  (subst (\ "f", (\ "x", canonical' m)) "x"
     (subst
        (\ "n",
         (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
        "f" (canonical' n))) (canonical (n + m))
    intros n.n: nat
forall m : nat,
eval
  (subst (\ "f", (\ "x", canonical' m)) "x"
     (subst
        (\ "n",
         (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
        "f" (canonical' n))) (canonical (n + m)) induction n; simpl; auto.n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", canonical' m)) "x"
(subst (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) "f"
(canonical' n))) (canonical (n + m))
forall m : nat,
eval
  ((\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
   ((\ "f", (\ "x", canonical' n)) @
    (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
    (\ "f", (\ "x", canonical' m))))
  (canonical (S (n + m)))
    econstructor; eauto.n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", canonical' m)) "x"
(subst (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) "f"
(canonical' n))) (canonical (n + m))
m: nat
eval
  ((\ "f", (\ "x", canonical' n)) @
   (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
   (\ "f", (\ "x", canonical' m))) ?v2
n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", canonical' m)) "x"
(subst (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) "f"
(canonical' n))) (canonical (n + m))
m: nat
eval
  (subst ?v2 "n"
     (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
  (canonical (S (n + m)))
    -n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", canonical' m)) "x"
(subst (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) "f"
(canonical' n))) (canonical (n + m))
m: nat
eval
  ((\ "f", (\ "x", canonical' n)) @
   (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
   (\ "f", (\ "x", canonical' m))) ?v2 econstructor; eauto.n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", canonical' m)) "x"
(subst (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) "f"
(canonical' n))) (canonical (n + m))
m: nat
eval
  ((\ "f", (\ "x", canonical' n)) @
   (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))))
  (\ "x",
   subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f" (canonical' n))
      econstructor; eauto.
    -n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", canonical' m)) "x"
(subst (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) "f"
(canonical' n))) (canonical (n + m))
m: nat
eval
  (subst (canonical (n + m)) "n"
     (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
  (canonical (S (n + m))) simpl.n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", canonical' m)) "x"
(subst (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) "f"
(canonical' n))) (canonical (n + m))
m: nat
eval
  (\ "f",
   (\ "x", "f" @ (canonical (n + m) @ "f" @ "x")))
  (canonical (S (n + m))) econstructor.
  Qed.

  Theorem add_ok : forall n ne m me,
      represents ne n
      -> represents me m
      -> represents (add @ ne @ me) (n + m).forall (n : nat) (ne : exp) (m : nat) (me : exp),
represents ne n ->
represents me m -> represents (add @ ne @ me) (n + m)

Solution

  Proof.forall (n : nat) (ne : exp) (m : nat) (me : exp),
represents ne n ->
represents me m -> represents (add @ ne @ me) (n + m)
    unfold represents; simpl.forall (n : nat) (ne : exp) (m : nat) (me : exp),
eval ne (canonical n) ->
eval me (canonical m) ->
eval (add @ ne @ me) (canonical (n + m))
    intros n ne m me H H0.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (add @ ne @ me) (canonical (n + m))
    econstructor; eauto.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (add @ ne) (\ ?x, ?e1')
n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (subst (canonical m) ?x ?e1') (canonical (n + m))
    -n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (add @ ne) (\ ?x, ?e1') econstructor; eauto.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval add (\ ?x0, ?e1'0)
n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (subst (canonical n) ?x0 ?e1'0) (\ ?x, ?e1')
      +n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval add (\ ?x0, ?e1'0) econstructor; eauto.
      +n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  (subst (canonical n) "n" (\ "m", "n" @ plus1 @ "m"))
  (\ ?x, ?e1') econstructor; eauto.
    -n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  (subst (canonical m) "m"
     (if "m" ==v "n"
      then "n" @ plus1 @ "m"
      else
       (fix subst
          (rep : exp) (x : var) (e : exp) {struct e} :
            exp :=
          match e with
          | Var y => if y ==v x then rep else y
          | \ y, e1 =>
              \ y,
              (if y ==v x then e1 else subst rep x e1)
          | e1 @ e2 => subst rep x e1 @ subst rep x e2
          end) (canonical n) "n" ("n" @ plus1 @ "m")))
  (canonical (n + m)) simpl.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  ((\ "f",
    (\ "x", subst (canonical m) "m" (canonical' n))) @
   (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
   canonical m) (canonical (n + m)) econstructor; eauto.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  ((\ "f",
    (\ "x", subst (canonical m) "m" (canonical' n))) @
   (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))))
  (\ ?x, ?e1')
n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (subst (canonical m) ?x ?e1') (canonical (n + m))
      2: apply add_ok'.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  ((\ "f",
    (\ "x", subst (canonical m) "m" (canonical' n))) @
   (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))))
  (\ "x",
   subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f" (canonical' n))
      econstructor; eauto.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  (subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f"
     (\ "x", subst (canonical m) "m" (canonical' n)))
  (\ "x",
   subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f" (canonical' n))
      rewrite subst_m_canonical'.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  (subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f" (\ "x", canonical' n))
  (\ "x",
   subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f" (canonical' n))
      econstructor; eauto.
  Qed.

Exercise: mult_ok

Let's repeat the same exercise for multiplication.

  Definition mult := \"n", \"m", "n" @ (add @ "m") @ zero.

  Example mult_1_2 : exists v,
      eval (mult @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v
      /\ eval (plus1 @ (plus1 @ zero)) v.exists v : exp,
  eval
    (mult @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero)))
    v /\ eval (plus1 @ (plus1 @ zero)) v

Solution

  Proof.exists v : exp,
  eval
    (mult @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero)))
    v /\ eval (plus1 @ (plus1 @ zero)) v
    eexists; split.eval
  (mult @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero)))
  ?v
eval (plus1 @ (plus1 @ zero)) ?v
    -eval
  (mult @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero)))
  ?v repeat (econstructor; simpl).
    -eval (plus1 @ (plus1 @ zero))
  (\ "f",
   (if "f" ==v "n"
    then \ "x", "f" @ ("n" @ "f" @ "x")
    else
     (fix subst
        (rep : exp) (x : var) (e : exp) {struct e} :
          exp :=
        match e with
        | Var y => if y ==v x then rep else y
        | \ y, e1 =>
            \ y,
            (if y ==v x then e1 else subst rep x e1)
        | e1 @ e2 => subst rep x e1 @ subst rep x e2
        end)
       (\ "f",
        (if "f" ==v "n"
         then \ "x", "f" @ ("n" @ "f" @ "x")
         else
          \ "x",
          (if "x" ==v "n"
           then "f" @ ("n" @ "f" @ "x")
           else
            (if "f" ==v "n"
             then \ "f", (\ "x", "x")
             else "f") @
            ((if "n" ==v "n"
              then \ "f", (\ "x", "x")
              else "n") @
             (if "f" ==v "n"
              then \ "f", (\ "x", "x")
              else "f") @
             (if "x" ==v "n"
              then \ "f", (\ "x", "x")
              else "x"))))) "n"
       (\ "x", "f" @ ("n" @ "f" @ "x")))) repeat econstructor.
  Qed.

  Lemma mult_ok' : forall n m,
eval
  (subst (\ "f", (\ "x", "x")) "x"
     (subst
        (\ "m",
          ((\ "f", (\ "x", canonical' m)) @
             (\ "n", (\ "f",
                       (\ "x", "f" @ (("n" @ "f") @ "x"))))) @ "m")
        "f" (canonical' n))) (canonical (n * m)).forall n m : nat,
eval
  (subst (\ "f", (\ "x", "x")) "x"
     (subst
        (\ "m",
         (\ "f", (\ "x", canonical' m)) @
         (\ "n",
          (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
         "m") "f" (canonical' n))) (canonical (n * m))

Solution

  Proof.forall n m : nat,
eval
  (subst (\ "f", (\ "x", "x")) "x"
     (subst
        (\ "m",
         (\ "f", (\ "x", canonical' m)) @
         (\ "n",
          (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
         "m") "f" (canonical' n))) (canonical (n * m))
    intros n.n: nat
forall m : nat,
eval
  (subst (\ "f", (\ "x", "x")) "x"
     (subst
        (\ "m",
         (\ "f", (\ "x", canonical' m)) @
         (\ "n",
          (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
         "m") "f" (canonical' n))) (canonical (n * m)) induction n; intros; simpl.m: nat
eval (\ "f", (\ "x", "x")) (canonical 0)
n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  ((\ "m",
    (\ "f", (\ "x", canonical' m)) @
    (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
    "m") @
   ((\ "f", (\ "x", canonical' n)) @
    (\ "m",
     (\ "f", (\ "x", canonical' m)) @
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
     "m") @ (\ "f", (\ "x", "x"))))
  (canonical (m + n * m))
    {m: nat
eval (\ "f", (\ "x", "x")) (canonical 0) auto. }n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  ((\ "m",
    (\ "f", (\ "x", canonical' m)) @
    (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
    "m") @
   ((\ "f", (\ "x", canonical' n)) @
    (\ "m",
     (\ "f", (\ "x", canonical' m)) @
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
     "m") @ (\ "f", (\ "x", "x"))))
  (canonical (m + n * m))
    econstructor; eauto.n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  ((\ "f", (\ "x", canonical' n)) @
   (\ "m",
    (\ "f", (\ "x", canonical' m)) @
    (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
    "m") @ (\ "f", (\ "x", "x"))) ?v2
n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  (subst ?v2 "m"
     ((\ "f", (\ "x", canonical' m)) @
      (\ "n",
       (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
      "m")) (canonical (m + n * m))
    {n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  ((\ "f", (\ "x", canonical' n)) @
   (\ "m",
    (\ "f", (\ "x", canonical' m)) @
    (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
    "m") @ (\ "f", (\ "x", "x"))) ?v2 repeat (econstructor; eauto). }n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  (subst (canonical (n * m)) "m"
     ((\ "f", (\ "x", canonical' m)) @
      (\ "n",
       (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
      "m")) (canonical (m + n * m))
    econstructor; simpl; eauto.n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  ((\ "f",
    (\ "x",
     (fix subst
        (rep : exp) (x : var) (e : exp) {struct e} :
          exp :=
        match e with
        | Var y => if y ==v x then rep else y
        | \ y, e1 =>
            \ y,
            (if y ==v x then e1 else subst rep x e1)
        | e1 @ e2 => subst rep x e1 @ subst rep x e2
        end) (canonical (n * m)) "m" (canonical' m))) @
   (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))))
  (\ ?x, ?e1')
n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval (subst (canonical (n * m)) ?x ?e1')
  (canonical (m + n * m))
    2: {n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval (subst (canonical (n * m)) ?x ?e1')
  (canonical (m + n * m)) apply add_ok'. }n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  ((\ "f",
    (\ "x",
     (fix subst
        (rep : exp) (x : var) (e : exp) {struct e} :
          exp :=
        match e with
        | Var y => if y ==v x then rep else y
        | \ y, e1 =>
            \ y,
            (if y ==v x then e1 else subst rep x e1)
        | e1 @ e2 => subst rep x e1 @ subst rep x e2
        end) (canonical (n * m)) "m" (canonical' m))) @
   (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))))
  (\ "x",
   subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f" (canonical' m))
    econstructor; eauto.n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  (subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f"
     (\ "x",
      (fix subst
         (rep : exp) (x : var) (e : exp) {struct e} :
           exp :=
         match e with
         | Var y => if y ==v x then rep else y
         | \ y, e1 =>
             \ y,
             (if y ==v x then e1 else subst rep x e1)
         | e1 @ e2 => subst rep x e1 @ subst rep x e2
         end) (canonical (n * m)) "m" (canonical' m)))
  (\ "x",
   subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f" (canonical' m))
    simpl.n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  (\ "x",
   subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f"
     ((fix subst
         (rep : exp) (x : var) (e : exp) {struct e} :
           exp :=
         match e with
         | Var y => if y ==v x then rep else y
         | \ y, e1 =>
             \ y,
             (if y ==v x then e1 else subst rep x e1)
         | e1 @ e2 => subst rep x e1 @ subst rep x e2
         end) (canonical (n * m)) "m" (canonical' m)))
  (\ "x",
   subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f" (canonical' m))
    rewrite subst_m_canonical'.n: nat
IHn: forall m : nat,
eval
(subst (\ "f", (\ "x", "x")) "x"
(subst
(\ "m",
(\ "f", (\ "x", canonical' m)) @
(\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @ "m") "f"
(canonical' n))) (canonical (n * m))
m: nat
eval
  (\ "x",
   subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f" (canonical' m))
  (\ "x",
   subst
     (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x"))))
     "f" (canonical' m))
    econstructor; eauto.
  Qed.

  Theorem mult_ok : forall n ne m me,
      represents ne n
      -> represents me m
      -> represents (mult @ ne @ me) (n * m).forall (n : nat) (ne : exp) (m : nat) (me : exp),
represents ne n ->
represents me m -> represents (mult @ ne @ me) (n * m)

Solution

  Proof.forall (n : nat) (ne : exp) (m : nat) (me : exp),
represents ne n ->
represents me m -> represents (mult @ ne @ me) (n * m)
    unfold represents; simpl.forall (n : nat) (ne : exp) (m : nat) (me : exp),
eval ne (canonical n) ->
eval me (canonical m) ->
eval (mult @ ne @ me) (canonical (n * m))
    econstructor; eauto.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (mult @ ne) (\ ?x, ?e1')
n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (subst (canonical m) ?x ?e1') (canonical (n * m))
    -n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (mult @ ne) (\ ?x, ?e1') econstructor; eauto.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval mult (\ ?x0, ?e1'0)
n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (subst (canonical n) ?x0 ?e1'0) (\ ?x, ?e1')
      {n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval mult (\ ?x0, ?e1'0) econstructor; eauto. }n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  (subst (canonical n) "n"
     (\ "m", "n" @ (add @ "m") @ zero)) (\ ?x, ?e1')
      econstructor; eauto.
    -n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  (subst (canonical m) "m"
     (if "m" ==v "n"
      then "n" @ (add @ "m") @ zero
      else
       (fix subst
          (rep : exp) (x : var) (e : exp) {struct e} :
            exp :=
          match e with
          | Var y => if y ==v x then rep else y
          | \ y, e1 =>
              \ y,
              (if y ==v x then e1 else subst rep x e1)
          | e1 @ e2 => subst rep x e1 @ subst rep x e2
          end) (canonical n) "n"
         ("n" @ (add @ "m") @ zero)))
  (canonical (n * m)) simpl.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  ((\ "f",
    (\ "x", subst (canonical m) "m" (canonical' n))) @
   ((\ "n", (\ "m", "n" @ plus1 @ "m")) @ canonical m) @
   (\ "f", (\ "x", "x"))) (canonical (n * m))
      econstructor; eauto.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  ((\ "f",
    (\ "x", subst (canonical m) "m" (canonical' n))) @
   ((\ "n", (\ "m", "n" @ plus1 @ "m")) @ canonical m))
  (\ ?x, ?e1')
n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (subst (\ "f", (\ "x", "x")) ?x ?e1')
  (canonical (n * m))
      2:{n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (subst (\ "f", (\ "x", "x")) ?x ?e1')
  (canonical (n * m)) apply mult_ok'. }n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  ((\ "f",
    (\ "x", subst (canonical m) "m" (canonical' n))) @
   ((\ "n", (\ "m", "n" @ plus1 @ "m")) @ canonical m))
  (\ "x",
   subst
     (\ "m",
      (\ "f", (\ "x", canonical' m)) @
      (\ "n",
       (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
      "m") "f" (canonical' n))
      econstructor; eauto.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  ((\ "n", (\ "m", "n" @ plus1 @ "m")) @ canonical m)
  ?v2
n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  (subst ?v2 "f"
     (\ "x", subst (canonical m) "m" (canonical' n)))
  (\ "x",
   subst
     (\ "m",
      (\ "f", (\ "x", canonical' m)) @
      (\ "n",
       (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
      "m") "f" (canonical' n))
      2:{n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  (subst ?v2 "f"
     (\ "x", subst (canonical m) "m" (canonical' n)))
  (\ "x",
   subst
     (\ "m",
      (\ "f", (\ "x", canonical' m)) @
      (\ "n",
       (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
      "m") "f" (canonical' n)) simpl.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  (\ "x",
   subst ?v2 "f"
     (subst (canonical m) "m" (canonical' n)))
  (\ "x",
   subst
     (\ "m",
      (\ "f", (\ "x", canonical' m)) @
      (\ "n",
       (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
      "m") "f" (canonical' n)) rewrite subst_m_canonical'.n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval (\ "x", subst ?v2 "f" (canonical' n))
  (\ "x",
   subst
     (\ "m",
      (\ "f", (\ "x", canonical' m)) @
      (\ "n",
       (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
      "m") "f" (canonical' n)) econstructor; eauto. }n: nat
ne: exp
m: nat
me: exp
H: eval ne (canonical n)
H0: eval me (canonical m)
eval
  ((\ "n", (\ "m", "n" @ plus1 @ "m")) @ canonical m)
  (\ "m",
   (\ "f", (\ "x", canonical' m)) @
   (\ "n", (\ "f", (\ "x", "f" @ ("n" @ "f" @ "x")))) @
   "m")
      econstructor; eauto.
  Qed.
End Ulc.