在Coq 中关于 [Co-] 归纳类型的教程中,第 10 页。在图 47 中,定义了一个递归函数,其中每个递归步骤使用一个格式良好的命题来表明递归终止。
调用 with 的函数使用wherex
进行递归调用,因此它应该终止。x-y
y<>0
我无法将它输入到 Coq 中而不会出现错误。Coq 抱怨调用中的递归参数并不小,而教程声称确实如此。
我错过了什么?
我稍微重写了代码以使其更短,但我也尝试了论文中的逐字定义。
首先我们证明它x-y
可以从 x 访问。
Require Import Omega.
Definition minus_decrease:
forall x y, Acc lt x -> x<>0 -> y<>0 -> Acc lt (x-y).
intros x y H Hx Hy.
case H; intro Ha; apply Ha.
omega.
Qed.
接下来,当尝试定义函数时,像这样
Definition div_aux :=
fix div_aux (x y:nat) (H:Acc lt x) {struct H}: nat :=
match eq_nat_dec x 0 with
|left _ => 0
|right _ =>
match eq_nat_dec y 0 with
|left _ => 0
|right v => S (div_aux (x-y) y (minus_decrease x y H _ v))
end
end.
然后 Coq 拒绝了,说
对 div_aux 的递归调用的主要参数等于“minus_decrease xy H ?156 v”,而不是“H”的子项。
注意如何div_aux x ...
用 递归调用自身div_aux (x-y) ...
,并(minus_decrease ...)
返回一个类型的术语Acc lt (x-y)
我如何使用Acc
来表明这个函数实际上终止了?