用定义明确的归纳定义的递归函数进行计算 [英] Compute with a recursive function defined by well-defined induction
问题描述
当我使用 Function 在Coq中定义非结构递归函数时，当要求进行特定计算时，生成的对象的行为会很奇怪。实际上，... 指令中的 Eval计算不是直接给出结果，而是返回一个相当长的表达式（通常为170000行）。似乎Coq无法评估所有内容，因此返回的是简化的（但很长的）表达式，而不仅仅是返回值。
When I use Function to define a non-structurally recursive function in Coq, the resulting object behaves strangely when a specific computation is asked. Indeed, instead of giving directly the result, the Eval compute in ... directive return a rather long (typically 170 000 lines) expression. It seems that Coq cannot evaluate everything, and therefore returns a simplified (but long) expression instead of just a value.
问题似乎出在我证明功能产生的义务。首先，我认为问题出在我使用的不透明术语上，然后将所有引理转换为透明常数。顺便说一句，有没有办法列出某个术语中出现的不透明术语？还是将不透明的引理转换成透明的引理的任何其他方法？
The problem seems to come from the way I prove the obligations generated by Function. First, I thought the problem came from the opaque terms I used, and I converted all the lemmas to transparent constants. By the way, is there a way to list the opaque terms appearing in a term ? Or any other way to turn opaque lemmas into transparent ones ?
我随后指出，问题更确切地说是来自所使用顺序的依据。但是我得到了奇怪的结果。
I then remarked that the problem came more precisely from the proof that the order used is well-founded. But I got strange results.
例如，我通过重复应用<$ c在自然数上定义 log2 $ c> div2 。定义如下：
For example, I define log2 on the natural numbers by repeatedly applying div2. Here is the definition:
Function log2 n {wf lt n} :=
match n with
| 0 => 0
| 1 => 0
| n => S (log2 (Nat.div2 n))
end.
我有两项举证责任。第一个方法检查 n 在递归调用中是否尊重关系 lt 并可以很容易地证明。
I get two proof obligations. The first one checks that n respects the relation lt in the recursive calls and can be proved easily.
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 。
The second one checks that lt is a well-founded order. This is already proved in the standard library. The corresponding lemma is Coq.Arith.Wf_nat.lt_wf.
如果使用此证明，则所得函数的行为一般。 日志24 10中的评估计算。返回 3 。
If I use this proof, the resulting function behaves normally. Eval compute in log24 10. returns 3.
但是，如果我想自己做证明，就不会总是得到这种行为。首先，如果我以 Qed 而不是 Defined 结束证明，那么计算的结果（即使是小数）是一个复杂的表达式，而不是单个数字。因此，我使用 Defined 并尝试仅使用透明引理。
But if I want to do the proof myself, I do not always get this behaviour. First, if I end the proof with Qed instead of Defined, the result of the computation (even on small numbers) is a complex expression and not a single number. So I use Defined and try to use only transparent lemmas.
Lemma lt_wf2 : well_founded lt.
Proof.
unfold well_founded. intros n.
apply (lemma1 n). clear n.
intros. constructor. apply H.
Defined.
在这里，lemma1证明了对自然数的充分归纳。再一次，我可以使用已经存在的引理，例如 lt_wf_ind ， lt_wf_rec ， lt_wf_rec1 位于 Coq.Arith.Wf_nat 中，甚至位于 well_founded_ind lt_wf 中。第一个不起作用，似乎是因为它不透明。其他三个工作。
Here, lemma1 is a proof of the well-founded induction on the natural numbers. Here again, I can use already existing lemmas, such as lt_wf_ind, lt_wf_rec, lt_wf_rec1 located in Coq.Arith.Wf_nat, or even well_founded_ind lt_wf. The first one does not work, it seems this is because it is opaque. The three others work.
我试图使用自然数 nat_ind 的标准归纳法直接证明这一点。这样得出：
I tried to prove it directly using the standard induction on the natural numbers, nat_ind. This gives:
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 具有相同的奇怪行为。而且该证明似乎只使用透明对象，所以也许问题不存在。
With this proof (and some variants of it), log2 has the same strange behaviour. And this proof seems to use only transparent objects, so maybe the problem is not there.
我如何定义 Function 返回特定值上可理解的结果吗？
How can I define a Function that returns understandable results on specific values ?
推荐答案
我设法找出了引起麻烦的地方： 反转H2。在 lemma1 中。事实证明，我们不需要案例分析和直觉即可完成证明（它不匹配 H2 ）：
I've managed to pin-point the place that causes troubles: it's inversion H2. in lemma1. It turns out we don't need that case-analysis and intuition can finish the proof (it doesn't pattern-match on 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 。
If we use lemma1 with this proof, the computation of log2 10 results in 3.
顺便说一下，这是我的 lt_wf2 版本（它也可以让我们计算）：
By the way, here is my version of lt_wf2 (it lets us compute as well):
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.
我相信
在愤怒中使用Coq的评估机制 Xavier Leroy的博客文章解释了这种行为。
I believe the Using Coq's evaluation mechanisms in anger blog post by Xavier Leroy explains this kind of behavior.
它消除了两头之间相等的证明，然后再遍历了两头，最后决定是产生左角还是产生右角。这使得最终结果的左/右数据部分取决于证明项，而证明项通常不会减少！
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 和
In our case we eliminate the proof of inequality (inversion H2.) in the proof of lemma1 and the Function mechanism makes our computations depend on a proof term. Hence, the evaluator can't proceed when n > 1.
以及体内倒置H1的原因。引理不影响计算的原因是对于 n = 0 和 n = 1 ， log2 n 在 match 表达式中定义为基本情况。
And the reason inversion H1. in the body of the lemma doesn't influence computations is that for n = 0 and n = 1, log2 n is defined within the match expression as base cases.
关于这一点，让我举一个例子，说明我们可以防止对任何值 n 和<$ c进行 log2 n 的评估我们选择的$ c> n + 1 ，其中 n> 1 和无处不在！
To illustrate this point, let me show an example when we can prevent evaluation of log2 n on any values n and n + 1 of our choice, where n > 1 and nowhere else!
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 s的计算都可能导致堆栈溢出或分段错误，因为Coq警告我们：
If you use this modified lemma in the definition of log2 you'll see that it computes everywhere except n = 4 and n = 5. Well, almost everywhere -- computations with large nats can result in stack overflow or segmentation fault, as Coq warns us:
警告：在nat中使用
大数字时，会发生堆栈溢出或分段错误（观察到的阈值可能从5000到70000
，具体取决于
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 工作，即使对于上述有缺陷的证明，我们也可以修改 log2 像这样
And to make log2 work for n = 4 and n = 5 even for the above "flawed" proof, we could amend log2 like this
Function log2 n {wf lt n} :=
match n with
| 0 => 0
| 1 => 0
| 4 => 2
| 5 => 2
| n => S (log2 (Nat.div2 n))
end.
最后添加必要的证明。
由于
函数机制实际上使用了有充分基础的证明，因此它必须透明并且不能依赖于证明对象的模式匹配。 lt_wf 引理来计算递减的终止保护。如果我们查看由 Eval 产生的术语（在评估未能产生 nat 的情况下），会看到以下内容：
The "well-founded" proof must be transparent and can't rely on pattern-matching on proof objects because the
Function mechanism actually uses the lt_wf lemma to compute the decreasing termination guard. If we look at the term produced by Eval (in a case where evaluation fails to produce a nat), we'll see something along these lines:
fix Ffix (x : nat) (x0 : Acc (fun x0 x1 : nat => S x0 <= x1) x) {struct x0}
很容易看到 x0：道具，因此将功能程序 log2 提取到OCaml中时会被擦除，但是Coq的内部评估机制必须用它来确保终止。
It's easy to see that x0 : Prop, so it gets erased when extracting the functional program log2 into, say OCaml, but Coq's internal evaluation mechanism have to use it to ensure termination.
这篇关于用定义明确的归纳定义的递归函数进行计算的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
