使用由明确定义的归纳定义的递归函数进行计算

当我使用Function在 Coq 中定义一个非结构递归函数，当要求进行特定计算时，生成的对象会表现得很奇怪。事实上，不是直接给出结果，而是Eval compute in ...指令返回一个相当长（通常为 170 000 行）的表达式。 Coq 似乎无法计算所有内容，因此返回一个简化（但很长）的表达式，而不仅仅是一个值。

问题似乎出在我证明由Function。首先，我认为问题出在我使用的不透明术语上，我将所有引理转换为透明常量。顺便问一下，有没有办法列出术语中出现的不透明术语？或者有其他方法可以将不透明引理变成透明引理吗？

然后我指出，问题更准确地来自于所使用的顺序是有根据的证明。但我得到了奇怪的结果。

例如，我定义log2重复应用自然数div2。这是定义：

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.回报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.

这里，lemma1 是自然数上有根据的归纳法的证明。在这里，我再次可以使用已经存在的引理，例如lt_wf_ind, lt_wf_rec, lt_wf_rec1位于Coq.Arith.Wf_nat， 甚至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返回特定值的可理解结果？

我已经成功地找出了造成麻烦的地方：它inversion H2. in lemma1。事实证明我们不需要案例分析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.

我相信在愤怒中使用 Coq 的评估机制Xavier Leroy 的博客文章解释了这种行为。

在递归尾部并最终决定是产生左还是右之前，它消除了头之间的相等性证明。这使得最终结果的左/右数据部分取决于证明项，而证明项通常不会减少！

在我们的例子中，我们消除了不平等的证明（inversion H2.) 的证明lemma1和Function机制使我们的计算依赖于证明项。因此，当 n > 1 时，评估器无法继续。

以及原因inversion H1.在引理的主体中不影响计算的是n = 0 and n = 1, log2 n被定义在match表达式作为基本情况。

为了说明这一点，让我举一个例子，当我们可以阻止评估log2 n对任何值n and n + 1我们的选择，其中n > 1 and 无处!

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 and n = 5。好吧，几乎无处不在——大型计算nats 可以导致堆栈溢出或分段错误，正如 Coq 警告我们的那样：

警告：使用时会发生堆栈溢出或分段错误 nat 中的大量数字（观察到的阈值可能从 5000 到 70000 不等） 取决于您的系统限制和执行的命令）。

并让log2为。。。工作n = 4 and n = 5即使对于上述“有缺陷”的证明，我们也可以修改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.

最后添加必要的证明。

---

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 : Prop，所以在提取功能程序时它会被删除log2比如说 OCaml，但是 Coq 的内部评估机制必须使用它来确保终止。