coq - 如何在 Coq 中编写以下形式的函数？

Question

f x = f (g subtermOfX)

只有当函数的 arg 是传递的 arg 的直接子项时才允许递归，以便 Coq 可以看到它实际上终止了吗？

Answer 1

如果函数 g 保留作为子项的属性，则可以编写这样的函数 f。

一些标准函数具有此属性，例如pred, sub:

From Coq Require Import Arith List.
Import ListNotations.

Fixpoint foo (x : nat) : nat :=
  match x with
  | O => 42
  | S x' => foo (pred x'). (* foo (x' - 1) works too *)
  end.

另一方面，一些(标准)函数没有这个属性，但可以重写以弥补这个缺陷。例如。标准的 tl 函数不保留 subterm 属性，因此以下操作失败:

Fail Fixpoint bar (xs : list nat) : list nat :=
  match xs with
  | [] => []
  | x :: xs' => bar (tl xs')
  end.

但是如果我们像这样重新定义 tail 函数

Fixpoint new_tl {A : Type} (xs : list A) :=
  match xs with
  | [] => xs           (* `tl` returns `[]` here *) 
  | _ :: xs' => xs'
  end.

我们可以恢复所需的属性:

Fixpoint bar (xs : list nat) : list nat :=
  match xs with
  | [] => []
  | x :: xs' => bar (new_tl xs')
  end.

tl 和new_tl 的唯一区别是，在输入列表为空的情况下，tl 返回[]，但 new_tl 返回原始列表。