使用定义明确的归纳法定义的递归函数进行计算
Compute with a recursive function defined by well-defined induction
当我使用 Function 在 Coq 中定义一个非结构递归函数时，生成的对象在询问特定计算时表现异常。实际上，Eval compute in ... 指令 return 不是直接给出结果，而是一个相当长（通常为 170 000 行）的表达式。似乎 Coq 无法评估所有内容，因此 return 是一个简化的（但很长）表达式，而不仅仅是一个值。
问题似乎出在我证明Function产生的义务的方式上。首先，我认为问题出在我使用的不透明术语上，我将所有引理都转换为透明常量。顺便问一下，有没有办法列出出现在术语中的不透明术语？或者任何其他方式将不透明的引理变成透明的引理？
然后我评论说问题更准确地来自证明所使用的顺序是有根据的。但是我得到了奇怪的结果。
例如，我通过重复应用div2在自然数上定义log2。这是定义：
Function log2 n {wf lt n} :=
match n with
| 0 => 0
| 1 => 0
| n => S (log2 (Nat.div2 n))
end.
我有两项证明义务。第一个检查 n 在递归调用中遵守关系 lt 并且可以很容易地证明。
forall n n0 n1 : nat, n0 = S n1 -> n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1)
intros. apply Nat.lt_div2. apply le_n_S. apply le_0_n.
第二个检查 lt 是一个有根据的命令。这已经在标准库中得到证明。对应的引理是Coq.Arith.Wf_nat.lt_wf.
如果我使用这个证明，生成的函数运行正常。 Eval compute in log24 10. returns 3.
但是如果我想自己做证明，我并不总是得到这种行为。首先，如果我以 Qed 而不是 Defined 结束证明，计算结果（即使是小数）是一个复杂的表达式，而不是一个单一的数字。所以我使用 Defined 并尝试只使用透明引理。
Lemma lt_wf2 : well_founded lt.
Proof.
unfold well_founded. intros n.
apply (lemma1 n). clear n.
intros. constructor. apply H.
Defined.
这里，引理1是对自然数的有根据的归纳法的证明。在这里，我可以再次使用已经存在的引理，例如位于 Coq.Arith.Wf_nat 中的 lt_wf_ind、lt_wf_rec、lt_wf_rec1，甚至 well_founded_ind lt_wf。第一个不起作用，这似乎是因为它是不透明的。其他三个工作。
我试图用自然数上的标准归纳法直接证明它，nat_ind。这给出：
Lemma lemma1 : forall n (P:nat -> Prop),
(forall n, (forall p, p < n -> P p) -> P n) -> P n.
Proof.
intros n P H. pose proof (nat_ind (fun n => forall p, p < n -> P p)).
simpl in H0. apply H0 with (n:=S n).
- intros. inversion H1.
- intros. inversion H2.
+ apply H. exact H1.
+ apply H1. assumption.
- apply le_n.
Defined.
有了这个证明（以及它的一些变体），log2 有同样奇怪的行为。而且这个证明好像只用了透明物体，所以问题可能不存在。
我如何定义 Function return 特定值的可理解结果？
在 Coq 中由有根据的递归定义的函数的归约行为通常不是很好，即使你声明你的证明是透明的。这样做的原因是，有充分根据的论证通常需要用复杂的证明项来完成。由于这些证明项最终出现在有根据的递归定义中，"simplifying" 正如您注意到的那样，您的函数将使所有这些证明项出现。
更容易依靠自定义策略和引理来减少以这种方式定义的函数。首先，我建议 Program Fixpoint 而不是 Function，因为后者要老得多而且（我认为）维护得不太好。因此，您最终会得到这样的定义：
Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Coq.Program.Wf.
Require Import Coq.Program.Tactics.
Program Fixpoint log2 n {wf lt n} :=
match n with
| 0 => 0
| 1 => 0
| n => S (log2 (Nat.div2 n))
end.
Next Obligation.
admit.
Qed.
现在，您只需要使用 program_simpl 策略来简化对 log2 的调用。这是一个例子：
Lemma foo : log2 4 = 2.
Proof.
program_simpl.
Qed.
我已经设法找出导致问题的地方：它是 lemma1 中的 inversion H2.。事实证明我们不需要那个案例分析并且 intuition 可以完成证明（它不在 H2 上进行模式匹配）：
Lemma lemma1 : forall n (P:nat -> Prop),
(forall n, (forall p, p < n -> P p) -> P n) -> P n.
Proof.
intros n P H. pose proof (nat_ind (fun n => forall p, p < n -> P p)).
simpl in H0. apply H0 with (n:=S n).
- intros. inversion H1.
- intros. intuition.
- apply le_n.
Defined.
如果我们在这个证明中使用 lemma1，log2 10 的计算结果是 3。
顺便说一下，这是我的 lt_wf2 版本（它也让我们计算）：
Lemma lt_wf2 : well_founded lt.
Proof.
unfold well_founded; intros n.
induction n; constructor; intros k Hk.
- inversion Hk.
- constructor; intros m Hm.
apply IHn; omega.
(* OR: apply IHn, Nat.lt_le_trans with (m := k); auto with arith. *)
Defined.
我相信
Using Coq's evaluation mechanisms in anger Xavier Leroy 的博客 post 解释了这种行为。
it eliminates the proof of equality between the heads before recursing over the tails and finally deciding whether to produce a left or a right. This makes the left/right data part of the final result dependent on a proof term, which in general does not reduce!
在我们的例子中，我们在 lemma1 的证明中消除了不等式 (inversion H2.) 的证明，而 Function 机制使我们的计算依赖于证明项。因此，当 n > 1 时，评估者无法继续。
引理主体中的 inversion H1. 不影响计算的原因是对于 n = 0 和 n = 1，log2 n 是在 match 表达式作为基本案例。
为了说明这一点，让我举一个例子，我们可以防止对 log2 n 对我们选择的任何值 n 和 n + 1 求值，其中 n > 1 别处!
Lemma lt_wf2' : well_founded lt.
Proof.
unfold well_founded; intros n.
induction n; constructor; intros k Hk.
- inversion Hk. (* n = 0 *)
- destruct n. intuition. (* n = 1 *)
destruct n. intuition. (* n = 2 *)
destruct n. intuition. (* n = 3 *)
destruct n. inversion Hk; intuition. (* n = 4 and n = 5 - won't evaluate *)
(* n > 5 *)
constructor; intros m Hm; apply IHn; omega.
Defined.
如果您在 log2 的定义中使用这个修改后的引理，您会发现它在除 n = 4 和 n = 5 之外的任何地方都可以计算。好吧，几乎无处不在——大 nat 的计算会导致 堆栈溢出 或分段错误，正如 Coq 警告我们的那样：
Warning: Stack overflow or segmentation fault happens when working with
large numbers in nat (observed threshold may vary from 5000 to 70000
depending on your system limits and on the command executed).
并且为了使 log2 对 n = 4 和 n = 5 甚至对上述 "flawed" 证明有效，我们可以像这样修改 log2
Function log2 n {wf lt n} :=
match n with
| 0 => 0
| 1 => 0
| 4 => 2
| 5 => 2
| n => S (log2 (Nat.div2 n))
end.
在最后添加必要的证明。
"well-founded" 证明必须是透明的，不能依赖证明对象上的模式匹配，因为 Function 机制实际上使用 lt_wf 引理来计算递减终止保护。如果我们查看由 Eval 生成的术语（在评估未能生成 nat 的情况下），我们将看到以下内容：
fix Ffix (x : nat) (x0 : Acc (fun x0 x1 : nat => S x0 <= x1) x) {struct x0}
很容易看出x0 : Prop，所以在将功能程序log2提取到OCaml中时它被擦除，但是Coq的内部评估机制必须使用它来确保终止。
当我使用 Function 在 Coq 中定义一个非结构递归函数时，生成的对象在询问特定计算时表现异常。实际上，Eval compute in ... 指令 return 不是直接给出结果，而是一个相当长（通常为 170 000 行）的表达式。似乎 Coq 无法评估所有内容，因此 return 是一个简化的（但很长）表达式，而不仅仅是一个值。
问题似乎出在我证明Function产生的义务的方式上。首先，我认为问题出在我使用的不透明术语上，我将所有引理都转换为透明常量。顺便问一下，有没有办法列出出现在术语中的不透明术语？或者任何其他方式将不透明的引理变成透明的引理？
然后我评论说问题更准确地来自证明所使用的顺序是有根据的。但是我得到了奇怪的结果。
例如，我通过重复应用div2在自然数上定义log2。这是定义：
Function log2 n {wf lt n} :=
match n with
| 0 => 0
| 1 => 0
| n => S (log2 (Nat.div2 n))
end.
我有两项证明义务。第一个检查 n 在递归调用中遵守关系 lt 并且可以很容易地证明。
forall n n0 n1 : nat, n0 = S n1 -> n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1)
intros. apply Nat.lt_div2. apply le_n_S. apply le_0_n.
第二个检查 lt 是一个有根据的命令。这已经在标准库中得到证明。对应的引理是Coq.Arith.Wf_nat.lt_wf.
如果我使用这个证明，生成的函数运行正常。 Eval compute in log24 10. returns 3.
但是如果我想自己做证明，我并不总是得到这种行为。首先，如果我以 Qed 而不是 Defined 结束证明，计算结果（即使是小数）是一个复杂的表达式，而不是一个单一的数字。所以我使用 Defined 并尝试只使用透明引理。
Lemma lt_wf2 : well_founded lt.
Proof.
unfold well_founded. intros n.
apply (lemma1 n). clear n.
intros. constructor. apply H.
Defined.
这里，引理1是对自然数的有根据的归纳法的证明。在这里，我可以再次使用已经存在的引理，例如位于 Coq.Arith.Wf_nat 中的 lt_wf_ind、lt_wf_rec、lt_wf_rec1，甚至 well_founded_ind lt_wf。第一个不起作用，这似乎是因为它是不透明的。其他三个工作。
我试图用自然数上的标准归纳法直接证明它，nat_ind。这给出：
Lemma lemma1 : forall n (P:nat -> Prop),
(forall n, (forall p, p < n -> P p) -> P n) -> P n.
Proof.
intros n P H. pose proof (nat_ind (fun n => forall p, p < n -> P p)).
simpl in H0. apply H0 with (n:=S n).
- intros. inversion H1.
- intros. inversion H2.
+ apply H. exact H1.
+ apply H1. assumption.
- apply le_n.
Defined.
有了这个证明（以及它的一些变体），log2 有同样奇怪的行为。而且这个证明好像只用了透明物体，所以问题可能不存在。
我如何定义 Function return 特定值的可理解结果？
在 Coq 中由有根据的递归定义的函数的归约行为通常不是很好，即使你声明你的证明是透明的。这样做的原因是，有充分根据的论证通常需要用复杂的证明项来完成。由于这些证明项最终出现在有根据的递归定义中，"simplifying" 正如您注意到的那样，您的函数将使所有这些证明项出现。
更容易依靠自定义策略和引理来减少以这种方式定义的函数。首先，我建议 Program Fixpoint 而不是 Function，因为后者要老得多而且（我认为）维护得不太好。因此，您最终会得到这样的定义：
Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Coq.Program.Wf.
Require Import Coq.Program.Tactics.
Program Fixpoint log2 n {wf lt n} :=
match n with
| 0 => 0
| 1 => 0
| n => S (log2 (Nat.div2 n))
end.
Next Obligation.
admit.
Qed.
现在，您只需要使用 program_simpl 策略来简化对 log2 的调用。这是一个例子：
Lemma foo : log2 4 = 2.
Proof.
program_simpl.
Qed.
我已经设法找出导致问题的地方：它是 lemma1 中的 inversion H2.。事实证明我们不需要那个案例分析并且 intuition 可以完成证明（它不在 H2 上进行模式匹配）：
Lemma lemma1 : forall n (P:nat -> Prop),
(forall n, (forall p, p < n -> P p) -> P n) -> P n.
Proof.
intros n P H. pose proof (nat_ind (fun n => forall p, p < n -> P p)).
simpl in H0. apply H0 with (n:=S n).
- intros. inversion H1.
- intros. intuition.
- apply le_n.
Defined.
如果我们在这个证明中使用 lemma1，log2 10 的计算结果是 3。
顺便说一下，这是我的 lt_wf2 版本（它也让我们计算）：
Lemma lt_wf2 : well_founded lt.
Proof.
unfold well_founded; intros n.
induction n; constructor; intros k Hk.
- inversion Hk.
- constructor; intros m Hm.
apply IHn; omega.
(* OR: apply IHn, Nat.lt_le_trans with (m := k); auto with arith. *)
Defined.
我相信 Using Coq's evaluation mechanisms in anger Xavier Leroy 的博客 post 解释了这种行为。
it eliminates the proof of equality between the heads before recursing over the tails and finally deciding whether to produce a left or a right. This makes the left/right data part of the final result dependent on a proof term, which in general does not reduce!
在我们的例子中，我们在 lemma1 的证明中消除了不等式 (inversion H2.) 的证明，而 Function 机制使我们的计算依赖于证明项。因此，当 n > 1 时，评估者无法继续。
引理主体中的 inversion H1. 不影响计算的原因是对于 n = 0 和 n = 1，log2 n 是在 match 表达式作为基本案例。
为了说明这一点，让我举一个例子，我们可以防止对 log2 n 对我们选择的任何值 n 和 n + 1 求值，其中 n > 1 别处!
Lemma lt_wf2' : well_founded lt.
Proof.
unfold well_founded; intros n.
induction n; constructor; intros k Hk.
- inversion Hk. (* n = 0 *)
- destruct n. intuition. (* n = 1 *)
destruct n. intuition. (* n = 2 *)
destruct n. intuition. (* n = 3 *)
destruct n. inversion Hk; intuition. (* n = 4 and n = 5 - won't evaluate *)
(* n > 5 *)
constructor; intros m Hm; apply IHn; omega.
Defined.
如果您在 log2 的定义中使用这个修改后的引理，您会发现它在除 n = 4 和 n = 5 之外的任何地方都可以计算。好吧，几乎无处不在——大 nat 的计算会导致 堆栈溢出 或分段错误，正如 Coq 警告我们的那样：
Warning: Stack overflow or segmentation fault happens when working with large numbers in nat (observed threshold may vary from 5000 to 70000 depending on your system limits and on the command executed).
并且为了使 log2 对 n = 4 和 n = 5 甚至对上述 "flawed" 证明有效，我们可以像这样修改 log2
Function log2 n {wf lt n} :=
match n with
| 0 => 0
| 1 => 0
| 4 => 2
| 5 => 2
| n => S (log2 (Nat.div2 n))
end.
在最后添加必要的证明。
"well-founded" 证明必须是透明的，不能依赖证明对象上的模式匹配，因为
Function 机制实际上使用 lt_wf 引理来计算递减终止保护。如果我们查看由 Eval 生成的术语（在评估未能生成 nat 的情况下），我们将看到以下内容：
fix Ffix (x : nat) (x0 : Acc (fun x0 x1 : nat => S x0 <= x1) x) {struct x0}
很容易看出x0 : Prop，所以在将功能程序log2提取到OCaml中时它被擦除，但是Coq的内部评估机制必须使用它来确保终止。