在Coq中定义Ackermann时出错 [英] Error in defining Ackermann in Coq
问题描述
我正在尝试在Coq中定义Ackermann-Peters函数，但收到一条我不理解的错误消息。如您所见，我将Ackermann的参数 a，b 打包为一对 ab ；我提供了一个排序，为参数定义了排序功能。然后，我使用 Function 表单定义Ackermann本身，并为其提供 ab 参数的排序功能。
I am trying to define the Ackermann-Peters function in Coq, and I'm getting an error message that I don't understand. As you can see, I'm packaging the arguments a, b of Ackermann in a pair ab; I provide an ordering defining an ordering function for the arguments. Then I use the Function form to define Ackermann itself, providing it with the ordering function for the ab argument.
Require Import Recdef.
Definition ack_ordering (ab1 ab2 : nat * nat) :=
match (ab1, ab2) with
|((a1, b1), (a2, b2)) =>
(a1 > a2) \/ ((a1 = a2) /\ (b1 > b2))
end.
Function ack (ab : nat * nat) {wf ack_ordering} : nat :=
match ab with
| (0, b) => b + 1
| (a, 0) => ack (a-1, 1)
| (a, b) => ack (a-1, ack (a, b-1))
end.
我得到的是以下错误消息：
What I get is the following error message:
错误：没有此类变量或假设：
ack。
我不确定是什么困扰着Coq，但是在网上搜索后，我发现一个建议是，使用由顺序或度量定义的递归函数可能会出现问题，其中递归调用发生在比赛。但是，使用投影 fst 和 snd 和 if-then-else 生成了另一条错误消息。有人可以建议如何在Coq中定义Ackermann吗？
I'm not sure what bothers Coq, but searching the internet, I found a suggestion there may be a problem with using a recursive function defined with an ordering or a measure, where the recursive call occurs within a match. However, using the projections fst and snd and an if-then-else generated a different error message. Can someone please suggest how to define Ackermann in Coq?
推荐答案
好像是 Function 无法解决此问题。但是，它的堂兄 Program Fixpoint 可以。
It seems like Function can't solve this problem. However, its cousin Program Fixpoint can.
让我们先定义一些处理基础良好的引理：
Let's define some lemmas treating well-foundedness first:
Require Import Coq.Program.Wf.
Require Import Coq.Arith.Arith.
Definition lexicographic_ordering (ab1 ab2 : nat * nat) : Prop :=
match ab1, ab2 with
| (a1, b1), (a2, b2) =>
(a1 < a2) \/ ((a1 = a2) /\ (b1 < b2))
end.
(* this is defined in stdlib, but unfortunately it is opaque *)
Lemma lt_wf_ind :
forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof. intro p; intros; elim (lt_wf p); auto with arith. Defined.
(* this is defined in stdlib, but unfortunately it is opaque too *)
Lemma lt_wf_double_ind :
forall P:nat -> nat -> Prop,
(forall n m,
(forall p (q:nat), p < n -> P p q) ->
(forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
Proof.
intros P Hrec p. pattern p. apply lt_wf_ind.
intros n H q. pattern q. apply lt_wf_ind. auto.
Defined.
Lemma lexicographic_ordering_wf : well_founded lexicographic_ordering.
Proof.
intros (a, b); pattern a, b; apply lt_wf_double_ind.
intros m n H1 H2.
constructor; intros (m', n') [G | [-> G]].
- now apply H1.
- now apply H2.
Defined.
现在我们可以定义Ackermann-Péter函数：
Now we can define the Ackermann-Péter function:
Program Fixpoint ack (ab : nat * nat) {wf lexicographic_ordering ab} : nat :=
match ab with
| (0, b) => b + 1
| (S a, 0) => ack (a, 1)
| (S a, S b) => ack (a, ack (S a, b))
end.
Next Obligation.
inversion Heq_ab; subst. left; auto. Defined.
Next Obligation.
apply lexicographic_ordering_wf. Defined.
一些简单的测试表明我们可以使用 ack ：
Some simple tests demonstrating that we can compute with ack:
Example test1 : ack (1, 2) = 4 := eq_refl.
Example test2 : ack (3, 4) = 125 := eq_refl. (* this may take several seconds *)
使用M. Sozeau和C. Mangin的 Equations 插件可以定义此函数方式：
Using the Equations plugin by M. Sozeau and C. Mangin it is possible to define the function this way:
From Equations Require Import Equations Subterm.
Equations ack (p : nat * nat) : nat :=
ack p by rec p (lexprod _ _ lt lt) :=
ack (pair 0 n) := n + 1;
ack (pair (S m) 0) := ack (m, 1);
ack (pair (S m) (S n)) := ack (m, ack (S m, n)).
不幸的是，无法使用（，） issue＃81 而导致的对的$ c>表示法。该代码取自Equation的测试套件： ack.v 。
Unfortunately, it's not possible to use the ( , ) notation for pairs due to issue #81. The code is taken from Equation's test suite: ack.v.
这篇关于在Coq中定义Ackermann时出错的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
