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?