Coq 中建立良好的递归答案

【问题标题】：Well founded recursion in CoqCoq 中建立良好的递归
【发布时间】：2015-10-23 12:36:27
【问题描述】：

我正在尝试在 Coq 中编写一个用于计算自然除法的函数，但我在定义它时遇到了一些麻烦，因为它不是结构递归。

我的代码是：

Inductive N : Set :=
  | O : N
  | S : N -> N.

Inductive Bool : Set :=
  | True : Bool
  | False : Bool.

Fixpoint sum (m :N) (n : N) : N :=
match m with
  | O => n
  | S x => S ( sum x n)
end.

Notation "m + n" := (sum m n) (at level 50, left associativity).

Fixpoint mult (m :N) (n : N) : N :=
match m with
  | O => O
  | S x => n + (mult x n)
end.

Notation "m * n" := (mult m n) (at level 40, left associativity).

Fixpoint pred (m : N) : N :=
match m with
  | O => S O
  | S x => x
end.

Fixpoint resta (m:N) (n:N) : N :=
match n with
  | O => m
  | S x => pred (resta m x)
end.
Notation "m - x" := (resta m x) (at level 50, left associativity).

Fixpoint leq_nat (m : N) (n : N) : Bool :=
match m with
  | O => True
  | S x => match n with 
    | O => False
    | S y => leq_nat x y
  end
end.

Notation "m <= n" := (leq_nat m n) (at level 70).

Fixpoint div (m : N) (n : N) : N :=
match n with
  | O => O
  | S x => match m <= n with
    | False => O
    | True => pred (div (m-n) n)
  end
end.

如你所见，Coq 不喜欢我的函数 div，它说

错误：无法猜测 fix 的递减参数。

如何在 Coq 中为此函数提供终止证明？我可以证明如果 n>O ^ n (m-n)

【问题讨论】：

标签： math coq proof totality

【解决方案1】：

在这种情况下，最简单的策略可能是将Program 扩展名与measure 一起使用。然后，您必须提供证据证明递归调用中使用的参数小于根据度量的顶级参数。

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

Fixpoint toNat (m : N) : nat :=
match m with O => 0 | S n => 1 + (toNat n) end.

Program Fixpoint div (m : N) (n : N) {measure (toNat m)}: N :=
match n with
  | O => O
  | S x => match m <= n with
    | False => O
    | True => pred (div (m-n) n)
  end
end.
Next Obligation.
(* your proof here *)

【讨论】：

【解决方案2】：

虽然gallais 的回答绝对是一般的方法，但我应该指出，我们可以将 Coq 中自然数的除法定义为一个简单的定点。在这里，为了简单起见，我使用标准库中nat 的定义。

Fixpoint minus (n m : nat) {struct n} : nat :=
   match n, m with
   | S n', S m' => minus n' m'
   |    _,    _ => n
   end.

Definition leq (n m : nat) : bool :=
  match minus n m with
  | O => true
  | _ => false
  end.

Fixpoint div (n m : nat) {struct n} : nat :=
  match m with
  | O => O
  | S m' =>
    if leq (S m') n then
      match n with
      | O => O (* Impossible *)
      | S n' => S (div (minus n' m') (S m'))
      end
    else O
  end.

Compute div 6 3.
Compute div 7 3.
Compute div 9 3.

minus 的定义本质上是标准库中的定义。请注意，在该定义的第二个分支上，我们返回 n。由于这个技巧，Coq 的终止检查器可以检测到 minus n' m' 在结构上小于 S n'，这允许我们执行对 div 的递归调用。

实际上还有一种更简单的方法，虽然有点难以理解：您可以检查除数是否更小并一步执行递归调用。

(* Divide n by m + 1 *)
Fixpoint div'_aux n m {struct n} :=
  match minus n m with
  | O    => O
  | S n' => S (div'_aux n' m)
  end.

Definition div' n m :=
  match m with
  | O    => O (* Arbitrary *)
  | S m' => div'_aux n m'
  end.

Compute div' 6 3.
Compute div' 7 3.
Compute div' 9 3.

再一次，由于minus 函数的形式，Coq 的终止检查器知道div'_aux 的第二个分支中的n' 是递归调用的有效参数。另请注意，div'_aux 除以 m + 1。

当然，这一切都依赖于一个聪明的技巧，需要详细了解终止检查器。一般来说，你必须求助于有根据的递归，正如加莱所展示的那样。

【讨论】：