Lambda-calculus in 50 lines of Coq (call-by-name).

LC.v

(* Untyped lambda calculus *)

(* Terms with free variables in [V]. *)
Inductive term {V : Type} : Type :=
| Var : V -> term
| App : term -> term -> term
| Lam : @term (unit + V) -> term
.

Arguments term : clear implicits.

Fixpoint rename {V W : Type} (t : term V) (r : V -> W) : term W :=
  match t with
  | Var v => Var (r v)
  | App t1 t2 => App (rename t1 r) (rename t2 r)
  | Lam t0 => Lam (rename t0 (fun v' =>
                                match v' with
                                | inl _ => inl tt
                                | inr v => inr (r v)
                                end))
  end.

Fixpoint subst {V W : Type} (t : term V) (s : V -> term W) : term W :=
  match t with
  | Var v => s v
  | App t1 t2 => App (subst t1 s) (subst t2 s)
  | Lam t0 => Lam (subst t0 (fun v' =>
                               match v' with
                               | inl _ => Var (inl tt)
                               | inr v => rename (s v) inr
                               end))
  end.

(* Call-by-name reduction step.
   [None] when [t] is in head normal form. *)
Fixpoint cbn_step {V : Type} (t : term V) : option (term V) :=
  match t with
  | App (Lam t0) t2 =>
    Some (subst t0 (fun v' =>
                match v' with
                | inl _ => t2
                | inr v => Var v
                end))
  | App t1 t2 =>
    match cbn_step t1 with
    | None => None
    | Some t1' => Some (App t1' t2)
    end
  | Lam _ | Var _ => None
  end.

(* Examples *)

Definition Id {V} : term V :=
  Lam (Var (inl tt)).

Example Id_id : forall t, @cbn_step Empty_set (App Id t) = Some t.
Proof. reflexivity. Qed.

Example Id_hnf : @cbn_step Empty_set Id = None.
Proof. reflexivity. Qed.

Definition Omega {V} : term V :=
  let omega := Lam (
                 let x := Var (inl tt) in
                 App x x) in
  App omega omega.

Example Omega_self : @cbn_step Empty_set Omega = Some Omega.
Proof. reflexivity. Qed.