当我用来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 …该Eval compute命令并不总是评估为简单表达式.考虑一下代码:
Require Import Coq.Lists.List.
Require Import Coq.Arith.Peano_dec.
Import ListNotations.
Inductive I : Set := a : nat -> I | b : nat -> nat -> I.
Lemma I_eq_dec : forall x y : I, {x = y}+{x <> y}.
Proof.
repeat decide equality.
Qed.
并且,如果我执行以下命令:
Eval compute in (if (In_dec eq_nat_dec 10 [3;4;5]) then 1 else 2).
Coq告诉我结果是2.但是,当我执行以下表达式时:
Eval compute in (if (In_dec I_eq_dec (a 2) [(a 1);(a 2)]) then 1 else 2).
我得到一个长表达式,其中In-predicate似乎展开,但没有给出结果. …
我正在（为我自己）写一篇关于如何在 Coq 中进行有根据的递归的解释。（参见 Coq'Art 书，第 15.2 章）。首先，我创建了一个基于 的示例函数，nat效果很好，但后来我又为 做了一次Z，当我使用Compute它来评估它时，它并没有一直减少到一个Z值。为什么？
这是我的示例（我将文本放在注释中，以便可以将整个内容复制粘贴到编辑器中）：
(* 有根据的递归测试 *)
(* TL;DR: 要进行有根据的递归，首先创建“函数”，然后使用 Acc_iter（用于可访问关系的迭代器）创建递归函数 *)
(* 作为示例，计算从 1 到 n 的级数之和，如下图所示：
修复 fn := （如果 n = 0 则 0 否则 n + f (n-1)）
现在，我们不要对n 使用结构递归。
相反，我们对 n 使用有充分根据的递归，使用小于 ('lt') 关系是有充分根据的。函数 f 终止，因为递归调用是在结构上较小的项（在递减的 Acc 链中）上进行的。*)
(* 首先我们为 nat 做这件事 *)
Require Import Arith.Arith.
Require Import Program.Utils. (* for 'dec' *)
Require Import Wellfounded.
(* 从关系成立的证明中，我们可以得到其域中的特定元素是可访问的证明。
亲爱的读者，这里的 …