Why does substitution terminate?

Question

I'm formalizing some properties of lambda calculus in Coq and I have some problems proving termination of substitution. My terms are defined as:

Inductive Term :=
  TVar: nat -> Term
| TAbs: nat -> Term -> Term
| TApp: Term -> Term -> Term.

and I have a way of generating fresh variables using a function

fresh: Term -> nat

satisfying:

Lemma fresh_is_fresh:
  forall t,
    ~ FV t (fresh t).

and similarly a function fresh2: Term -> Term -> nat for obtaining a fresh identifier wrt. two terms.

I now want to define a standard notion of capture avoiding substitution:

Fixpoint substitute (t1:Term) (t2:Term) (x:nat): Term :=
  match t1 with
  | TVar y =>
    if beq_nat x y then t2 else TVar y
  | TApp t11 t12 =>
    TApp (substitute t11 t2 x) (substitute t12 t2 x)
  | TAbs y t =>
    if beq_nat x y then
      TAbs x t
    else TAbs (fresh2 t t1) (substitute (substitute t (TVar y) (fresh2 t t1)) t2 x)
  end.

Obviously, Coq cannot see that this definition is terminating, so I need to provide a custom measure, so that the code is something like the following:

Program Fixpoint substitute (t1:Term) (t2:Term) (x:nat) {measure ???}: Term :=
  match t1 with
  | TVar y =>
    if beq_nat x y then t2 else TVar y
  | TApp t11 t12 =>
    TApp (substitute t11 t2 x) (substitute t12 t2 x)
  | TAbs y t =>
    if beq_nat x y then
      TAbs x t
    else TAbs (fresh2 t t1) (substitute (substitute t (TVar y) (fresh2 t t1)) t2 x)
  end.

Now my question is: What is the correct measure to use here? And how I do use it to prove the obligations which arise using this measure?

Answer 1

Derek Elkins' comment solved my problem! Here's the solution I came up with:

We create a seperate renaming function rename: Term -> nat -> nat -> Term, which assumes that the name to rename with is fresh. This makes it trivially terminating.

Fixpoint rename (t:Term) (x y : nat): Term :=
  match t with
  | TVar z =>
    if beq_nat y z then TVar x
    else TVar z
  | TApp t1 t2 =>
    TApp (rename t1 x y) (rename t2 x y)
  | TAbs z t =>
    if beq_nat y z then
      TAbs z t
    else
      TAbs z (rename t x y)
  end.

we then define a (somewhat arbitrary) measure of a term:

Fixpoint size (t:Term): nat :=
  match t with
    TVar _ => 1
  | TApp t1 t2 => size t1 + size t2
  | TAbs x t => 2 + size t
  end.

and we can easily prove that renaming preserves this measure:

Lemma rename_preserves_size:
  forall t x y,
    size t = size (rename t x y).

this lemma is used in the final case of substitition in order to prove that the term rename t y' y has the same size as t and thus the call substitute (rename t y' y) t2 x happens on a strictly smaller term.

Now all I need to prove that this is correct.