在Coq中建立良好的递归 [英] Well founded recursion in Coq
问题描述
我试图在Coq中编写一个用于计算自然除法的函数,但由于它不是结构性递归,因此在定义它时遇到了一些麻烦。
I am trying to write a function for computing natural division in Coq and I am having some trouble defining it since it is not structural recursion.
我的代码是:
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,它说
As you can see, Coq does not like my function div, it says
错误:无法猜测
fix
的递减参数。
如何在Coq中提供此功能的终止证明?我可以证明如果n> O ^ n <= m->(m-n)< m。
How can I supply in Coq a termination proof for this function? I can prove that if n>O ^ n<=m -> (m-n) < m.
推荐答案
在这种情况下,最简单的策略可能是使用 Program
扩展名和措施
。然后,您必须提供一个证明,根据度量,递归调用中使用的参数小于顶级参数。
The simplest strategy in this case is probably to use the Program
extension together with a measure
. You will then have to provide a proof that the arguments used in the recursive call are smaller than the top level ones according to the 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 *)
这篇关于在Coq中建立良好的递归的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!