Interpreting the untyped lambda calculus in Coq (cf. https://gist.github.com/gallais/303cfcfe053fbc63eb61 for Agda)

UntypedLambda.v

Inductive Fin : nat -> Type :=
  | Zero : forall n, Fin (S n)
  | Succ : forall n, Fin n -> Fin (S n)
.

Arguments Zero [n].
Arguments Succ [n] k.

Inductive Expr (n : nat) : Type :=
  | Var : Fin n -> Expr n
  | Lam : Expr (S n) -> Expr n
  | App : Expr n -> Expr n -> Expr n
.

Arguments Var [n] k.
Arguments Lam [n] b.
Arguments App [n] f t.

Definition Renaming (m n : nat) := Fin m -> Fin n.

Definition extendRenaming {m n : nat} :
  Renaming m n -> Renaming (S m) (S n).
intros rho k; remember (S m); destruct k.
 - apply Zero.
 - apply Succ, rho.
   inversion Heqn0; subst; assumption.
Defined.

Fixpoint rename {m n : nat}
  (t : Expr m) (rho : Renaming m n)
  {struct t} : Expr n :=
match t with
  | Var k   => Var (rho k)
  | Lam b   => Lam (rename b (extendRenaming rho))
  | App f t => App (rename f rho) (rename t rho)
end.

Definition Substitution (m n : nat) := Fin m -> Expr n.

Definition extendSubstitution {m n : nat} :
  Substitution m n -> Substitution (S m) (S n).
intros rho k; remember (S m); destruct k.
 - apply Var, Zero.
 - inversion Heqn0; subst.
   eapply rename.
   + apply rho; assumption.
   + intro j; apply Succ, j.
Defined.

Fixpoint substitute {m n : nat}
  (t : Expr m) (rho : Substitution m n) : Expr n :=
match t with
  | Var k   => rho k
  | Lam b   => Lam (substitute b (extendSubstitution rho))
  | App f t => App (substitute f rho) (substitute t rho)
end.

Definition beta {m : nat} (t : Expr (S m)) (u : Expr m)
  : Expr m.
apply (substitute t).
intro k; remember (S m); destruct k; inversion Heqn; subst.
 - exact u.
 - apply Var, k.
Defined.

Definition option_or {A : Type} (l r : option A) : option A :=
match l with
  | None   => r
  | Some _ => l
end.

Fixpoint reduce {m : nat} (t : Expr m) : option (Expr m) :=
match t with
  | Var _         => None
  | Lam b         => option_map (@Lam _) (reduce b)
  | App (Lam f) t => Some (beta f t)
  | App f t       => option_or (option_map (fun f => App f t) (reduce f))
                               (option_map (App f) (reduce t))
end.

CoInductive Delay (A : Type) : Type :=
  | Now   : A -> Delay A
  | Later : Delay A -> Delay A
.

Arguments Now [A] a.
Arguments Later [A] d.

CoFixpoint run {m : nat} (t : Expr m) : Delay (Expr m) :=
match reduce t with
  | Some t' => Later (run t')
  | None    => Now t
end.

Definition delta : Expr 0 := Lam (App (Var Zero) (Var Zero)).
Definition omega : Expr 0 := App delta delta.

Definition infinite_loop := run omega.

Fixpoint extract {A : Type} (n : nat) (da : Delay A) : option A :=
match n with
  | O   => None
  | S m =>
    match da with
      | Later da' => extract m da'
      | Now a     => Some a
    end
end.

Lemma infinite_loop_is_infinite : forall n, extract n infinite_loop = None.
Proof.
induction n.
 - reflexivity.
 - simpl; apply IHn.
Qed.