Non-trivially recursive functions termination

[radeusgd]

Coq requires Fixpoint's recursion to be structural to maintain the termination requirements.

When writing substitution with normal names (not DeBruijn indices), I needed to rename variables bound by lambdas to avoid capture of free variables during the substitution.

I tried the following code:

Fixpoint fresh (term: Term) : label :=
  match term with
  | Val (Lit n) => 0
  | Val (Lam x T t) => max x (fresh t + 1)
  | Var x => x + 1
  | App t1 t2 => max (fresh t1) (fresh t2)
  end.

Definition fresh2 (t1: Term) (t2: Term) := (max (fresh t1) (fresh t2)) + 1.

Fixpoint renameVars (term: Term) (old: label) (new: label): Term :=
  match term with
  | Val (Lit n) => term
  | Val (Lam x T t) =>
    if Nat.eq_dec x old then Val (Lam new T (renameVars t old new))
    else Val (Lam x T (renameVars t old new))
  | Var x =>
    if Nat.eq_dec x old then Var new
    else term
  | App t1 t2 => App (renameVars t1 old new) (renameVars t2 old new)
end.

Program Fixpoint substitute (term: Term) (varname: label) (varterm: Term) : Term :=
  match term with
  | Val (Lit n) => term
  | Val (Lam x T t) =>
    if Nat.eq_dec x varname then term
    else
      let freshx := fresh2 varterm t in
      let t' := renameVars t x freshx in
      Val (Lam freshx T (substitute t' varname varterm))
  | Var x =>
    if Nat.eq_dec x varname then varterm
    else term
  | App t1 t2 => App (substitute t1 varname varterm) (substitute t2 varname varterm)
  end.

Unfortunately Coq was unable to prove termination, as I call substitute recursively with an argument that is a result of calling renameVars. renameVars returns a term with the same structure (thus the same size), but that's not a trivial observation (Coq seems to be able to unfold simple definitions, but cannot prove this automatically for recursive functions).

[radeusgd]

Afterwards I used a different variant of Fixpoint:

Inductive Null.
Require Coq.Program.Wf.
Program Fixpoint substitute (term: Term) (varname: label) (varterm: Term) {size term} : Term :=
  match term with
  | Val (Lit n) => term
  | Val (Lam x T t) =>
    if Nat.eq_dec x varname then term
    else
      let freshx := fresh2 varterm t in
      let t' := renameVars t x freshx in
      Val (Lam freshx T (substitute t' varname varterm))
  | Var x =>
    if Nat.eq_dec x varname then varterm
    else term
  | App t1 t2 => App (substitute t1 varname varterm) (substitute t2 varname varterm)
  end.
Next Obligation.
  exact Null.
Qed.

I hint Coq that size of the term will be decreasing. It generates one proof obligation:

  varname : label
  varterm : Term
  ============================
  Type

Which looks pretty strange, but it can be proven by putting any type there (for example a completely unrelated empty type I defined above). I am unsure what type is a right one to put there or why this obligation is even generated (as it seems to be trivially provable?), but it looks like it doesn't affect the resulting code.

In the end the conclusion is that it is better to avoid writing such complex functions if possible, as proving any properties of them will become much harder. This function will not be needed when moving to DeBruijn indices with autosubst.