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

Question

当我用来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.

在这里,引理1证明了对自然数的有根据的归纳.在这里,我可以使用已有的引理,如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返回特定值的可理解结果？

Answer 1

我已经成功地找出了引起麻烦的地方：它inversion H2.在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.

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

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

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

inversion H1.引理主体中不影响计算的原因是 forn = 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。好吧，几乎在任何地方——使用大nats 的计算都可能导致堆栈溢出或分段错误，正如 Coq 警告我们的那样：

警告：在 nat 中处理大量数字时，会发生堆栈溢出或分段错误（观察到的阈值可能在 5000 到 70000 之间变化，具体取决于您的系统限制和执行的命令）。

为了使上述“有缺陷”的证明有效，我们可以log2这样修改n = 4n = 5log2

Function log2 n {wf lt n} :=
  match n with
  | 0 => 0
  | 1 => 0
  | 4 => 2
  | 5 => 2
  | n => S (log2 (Nat.div2 n))
  end.

最后添加必要的证明。

“有充分根据的”证明必须是透明的，并且不能依赖于证明对象的模式匹配，因为该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 的内部评估机制必须使用它来确保终止。