如何在 Coq/ 中对 BinNums.Z 进行归纳

Question

我正在尝试做一个像这样的简单函数

Fixpoint find_0 (n : BinNums.Z) :=
  match n with
    Z0 => n
  | Zpos p => find_0 p
  | Zneg q => find_0 q
  end.

但是 p 是 positive 而不是 Z 所以这是错误的类型。

如果我尝试

Fixpoint find_0 (n : BinNums.Z) :=
  match n with
    Z0 => n
  | Zpos p => find_0 (n - 1)
  | Zneg q => find_0 (n + 1)
  end.

那么 Coq 无法验证这是强归一化，错误

Recursive definition of find_0 is ill-formed.
In environment
find_0 : BinNums.Z -> BinNums.Z
n : BinNums.Z
p : positive
Recursive call to find_0 has principal argument equal to 
"n - 1" instead of a subterm of "n".
Recursive definition is:
"fun n : BinNums.Z =>
 match n with
 | 0 => n
 | Z.pos _ => find_0 (n - 1)
 | BinInt.Z.neg _ => find_0 (n + 1)%Z
 end".

遇到这种情况怎么办？

此致

Answer 1

自Bignums.Z的定义：

Inductive Z : Set :=
    Z0 : Z
  | Zpos : positive -> Z
  | Zneg : positive -> Z.

不是递归的，你不能在它上面写递归函数。相反，您编写一个简单的非递归 Definition 来处理 Bignums.Z 的构造函数，并在那里调用您定义的递归函数。在正片上单独定义正片所需的函数也是一种很好的风格。

Answer 2

Coq 中的每个递归函数都必须清楚地具有 递减方面。对于许多归纳类型，这种递减方面自然是由这种归纳类型的递归结构提供的。如果查看 positive 的定义，您会看到：

Inductive positive : Set :=
xI : positive -> positive | xO : positive -> positive | xH : positive.

当类型为正的对象p符合模式xO q时，q明显小于p，如果只是作为一条数据（这里因为xO的约定意思是乘以2，所以q在数值上也比p)小。

查看 Z 的数据类型时，您会发现没有递归，因此没有可见的递减模式，其中较小的对象也属于 Z 类型，因此您不能使用 Fixpoint 方法编写递归函数。

但是，存在 Coq 的扩展，称为 Equations，可以编写您想要的函数。诀窍在于您仍然需要解释在递归调用期间某些东西正在减少。这需要一个额外的对象，一个已知没有无限路径的关系。这种关系称为有根据的。这里我们将使用的关系称为 Zwf.

From Equations Require Import Equations.
Require Import ZArith Zwf Lia.

#[export]Instance Zwf_wf (base : Z) : WellFounded (Zwf base).
Proof.
constructor; apply Zwf_well_founded.
Qed.

Equations find0 (x : Z) : Z by wf (Z.abs x) (Zwf 0) :=
  find0 Z0 := Z0; find0 (Zpos p) := find0 (Zpos p - 1);
  find0 (Zneg p) := find0 (Zneg p + 1).
Next Obligation.
set (x := Z.pos p); change (Zwf 0 (Z.abs (x - 1)) (Z.abs x)).
unfold Zwf. lia.
Qed.
Next Obligation.
set (x := Z.neg p); change (Zwf 0 (Z.abs (x + 1)) (Z.abs x)).
unfold Zwf. lia.
Qed.

比使用 Fixpoint 的直接递归函数要多一点工作，因为我们需要解释我们使用的是一个有根据的关系，确保 Equations 扩展能找到信息（这是脚本Instance部分的目的。然后，我们还需要证明每次递归调用都满足减少属性。这里，减少的是整数的绝对值的数值。

Equations 工具将为您提供一组定理，以帮助推理 find0 函数。特别是，定理 find0_equation1、find0_equation2 和 find0_equation3 确实表示我们定义了一个函数，该函数遵循您想要的算法。

如何在 Coq/ 中对 BinNums.Z 进行归纳

How to do induction on BinNums.Z in Coq/

coq