Why does substitution terminate?

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?

• This seems to be mostly a (good) technical question about theorem proving in Coq. I think it's better to move it to Stackoverflow. – Anton Trunov Dec 12 '17 at 23:39
• It might be easier to differentiate between arbitrary substitution and renaming a variable. – Derek Elkins Dec 13 '17 at 0:34
• That did the trick, @DerekElkins! I'll post an answer to my question in a second! – Mathias Vorreiter Pedersen Dec 13 '17 at 9:24

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.