在Coq的有根据的递归

Question

我正在尝试编写一个函数来计算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 - >(mn)<m.

Answer 1

在这种情况下最简单的策略可能是将Program扩展与a一起使用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 *)