Coq中有根据的递归
Well founded recursion in Coq
我正在尝试在 Coq 中编写一个用于计算自然 division 的函数,但我在定义它时遇到了一些问题,因为它不是结构递归。
我的代码是:
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,它说
Error: Cannot guess decreasing argument of fix
.
我如何在 Coq 中为这个函数提供终止证明?我可以证明如果 n>O ^ n<=m -> (m-n) < m.
在这种情况下,最简单的策略可能是将 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 *)
虽然 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
的定义本质上是标准库中的定义。请注意该定义的第二个分支,我们 return 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
.
当然,这整个事情依赖于一个聪明的技巧,需要详细了解终止检查器。一般来说,你必须求助于有充分根据的递归,正如加莱所展示的那样。
我正在尝试在 Coq 中编写一个用于计算自然 division 的函数,但我在定义它时遇到了一些问题,因为它不是结构递归。
我的代码是:
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,它说
Error: Cannot guess decreasing argument of
fix
.
我如何在 Coq 中为这个函数提供终止证明?我可以证明如果 n>O ^ n<=m -> (m-n) < m.
在这种情况下,最简单的策略可能是将 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 *)
虽然 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
的定义本质上是标准库中的定义。请注意该定义的第二个分支,我们 return 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
.
当然,这整个事情依赖于一个聪明的技巧,需要详细了解终止检查器。一般来说,你必须求助于有充分根据的递归,正如加莱所展示的那样。