# Simply-Typed Lambda Calculus

Reduction is weak, deterministic, and CBV. Weak means that reduction does not descent into lambda abstractions. Only closed beta redexes are reduced.

Set Implicit Arguments.
Require Import EqNat.
Tactic Notation "inv" hyp(A) := inversion A ; subst ; clear A.

Abstract Syntax

Inductive var : Type :=
| Var : nat -> var.

Inductive ty : Type :=
| Nat : ty (* nat *)
| Fun : ty -> ty -> ty. (* function type *)

Inductive tm : Type :=
| tmV : var -> tm (* variable *)
| tmL : var -> ty -> tm -> tm (* lambda *)
| tmA : tm -> tm -> tm . (* application *)

Inductive free (x : var) : tm -> Prop :=
| freeV : free x (tmV x)
| freeL y T t : x<>y -> free x t -> free x (tmL y T t)
| freeA t1 t2 : free x t1 \/ free x t2 -> free x (tmA t1 t2).

Boolean Equality on Variables

Definition beq_var (x y : var) : bool :=
match x, y with Var x', Var y' => beq_nat x' y' end.

Lemma beq_var_eq b x y :
b = beq_var x y -> if b then x=y else x<>y.

Proof. destruct x, y ; simpl ; intros A ; destruct b.
apply beq_nat_eq in A. congruence.
symmetry in A. apply beq_nat_false in A. congruence. Qed.

Typing

Definition context : Type := var -> option ty.
Definition empty : context := fun _ => None.
Definition update (g : context) (x : var) (T : ty) : context :=
fun y => if beq_var x y then Some T else g y.

Inductive type : context -> tm -> ty -> Prop :=
| typeV g x T : g x = Some T -> type g (tmV x) T
| typeL g x S t T : type (update g x S) t T -> type g (tmL x S t) (Fun S T)
| typeA g t1 t2 S T : type g t1 (Fun S T) -> type g t2 S -> type g (tmA t1 t2) T.

Lemma type_free g t T x :
type g t T -> free x t -> exists S, g x = Some S.

Proof. intros A B. induction A ; inv B.
(* V *) now eauto.
(* L *) apply IHA in H3. destruct H3 as [S0 C].
unfold update in C. remember (beq_var x0 x) as b.
destruct b ; apply beq_var_eq in Heqb. congruence. now eauto.
(* A *) inv H0 ; auto. Qed.

Lemma type_empty t T x :
type empty t T -> free x t -> False.

Proof. intros A B. destruct (type_free A B) as [S C]. inv C. Qed.

Lemma type_invariance t g g' T :
(forall x, free x t -> g x = g' x) -> type g t T -> type g' t T.

Proof with now auto using free.
intros A B ; revert g' A ; induction B ; intros g' A.
(* V *) constructor. rewrite A in H...
(* L *) constructor. apply IHB. intros y C.
unfold update. remember (beq_var x y) as b.
destruct b ; apply beq_var_eq in Heqb...
(* A *) apply typeA with (S:=S)... Qed.

Lemma type_unique g t T1 T2 :
type g t T1 -> type g t T2 -> T1 = T2.

Proof. intros A ; revert T2 ; induction A ; intros T2 B ; inv B.
(* V *) congruence.
(* L *) now f_equal ; auto.
(* A *) apply IHA1 in H2 ; apply IHA2 in H4 ; congruence. Qed.

Substitution, capturing

Fixpoint subst (t : tm) (x : var) (s : tm) : tm :=
match t with
| tmV y => if beq_var x y then s else t
| tmL y T t' => if beq_var x y then t else tmL y T (subst t' x s)
| tmA t1 t2 => tmA (subst t1 x s) (subst t2 x s)
end.

Lemma substitution g t T x s S :
type (update g x S) t T -> type empty s S -> type g (subst t x s) T.

Proof. revert g T ; induction t ; simpl ; intros g T A B ; inv A.
(* x *) unfold update in H1. remember (beq_var x v) as b.
destruct b ; apply beq_var_eq in Heqb.
inv H1. apply type_invariance with (g:= empty) ; auto.
now intros y C ; exfalso ; eauto using type_empty.
now eauto using type.
(* L *) remember (beq_var x v) as b ; destruct b
; apply beq_var_eq in Heqb ; constructor.
subst v.
apply type_invariance with (g := update (update g x S) x t) ; auto.
intros y C. unfold update. remember (beq_var x y) as b.
destruct b ; apply beq_var_eq in Heqb ; congruence.
apply IHt ; auto.
apply type_invariance with (g := update (update g x S) v t) ; auto.
intros y C. unfold update.
remember (beq_var x y) as c ; remember (beq_var v y) as d.
destruct c , d ; apply beq_var_eq in Heqc ; apply beq_var_eq in Heqd
; congruence.
(* A *) eauto using type. Qed.

Reduction

Inductive value : tm -> Prop :=
| valueL x T t : value (tmL x T t).

Inductive step : tm -> tm -> Prop :=
| stepA x T t s : value s -> step (tmA (tmL x T t) s) (subst t x s)
| stepDAL t1 t1' t2 : step t1 t1' -> step (tmA t1 t2) (tmA t1' t2)
| stepDAR x T t t2 t2' : step t2 t2' -> step (tmA (tmL x T t) t2) (tmA (tmL x T t) t2').

Lemma value_normal t t' :
value t -> step t t' -> False.

Proof. intros A. revert t' ; induction A ; intros t' B ; inv B. Qed.

Lemma preservation t T t' :
type empty t T -> step t t' -> type empty t' T.

Proof. intros A B ; revert T A ; induction B ; intros T' A ; inv A.
(* A *) inv H3. now eauto using substitution.
(* ADL *) now eauto using type.
(* ADR *) eauto using type. Qed.

Lemma progress t T :
type empty t T -> value t \/ exists t', step t t'.

Proof. intros A ; remember empty as g ; induction A ; subst g.
(* V *) now inv H.
(* L *) now auto using value.
(* A *) right ; intuition ; inv H0 ; eauto using step.
inv H1 ; eauto using step. Qed.