1

在Coq 中关于 [Co-] 归纳类型的教程中，第 10 页。在图 47 中，定义了一个递归函数，其中每个递归步骤使用一个格式良好的命题来表明递归终止。

调用 with 的函数使用wherex进行递归调用，因此它应该终止。x-yy<>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来表明这个函数实际上终止了？

4

1 回答 1

3

错误似乎是我用Qed.而不是Defined. 以下作品结束了定义。

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.
Defined.


Fixpoint div_aux (x y:nat) (H:Acc lt x) {struct H}: nat.
Proof.
  refine (if eq_nat_dec x 0
          then 0
          else if eq_nat_dec y 0
               then y
               else S (div_aux (x-y) y _)).
  apply (minus_decrease _ _ H _H _H0).
Qed.
于 2014-11-26T15:54:46.133 回答