4
$\begingroup$

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?

$\endgroup$
3
  • 1
    $\begingroup$ This seems to be mostly a (good) technical question about theorem proving in Coq. I think it's better to move it to Stackoverflow. $\endgroup$ Dec 12, 2017 at 23:39
  • 2
    $\begingroup$ It might be easier to differentiate between arbitrary substitution and renaming a variable. $\endgroup$ Dec 13, 2017 at 0:34
  • $\begingroup$ That did the trick, @DerekElkins! I'll post an answer to my question in a second! $\endgroup$ Dec 13, 2017 at 9:24

1 Answer 1

2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.