推理适用于 Coq 中 nat 列表的函数答案

【问题标题】：Reasoning over functions applied to lists of nat in Coq推理适用于 Coq 中 nat 列表的函数
【发布时间】：2021-02-11 07:36:04
【问题描述】：

我们正在努力验证具有如下三个功能的系统。但是，我们不知道如何进一步处理这样的证明。 Coq 函数的实际定义可以共享。请指导我们。

Parameter weights : nat -> list nat -> nat -> nat.
Parameter schedule: nat -> list nat -> list nat. 
Parameter count: nat -> list nat -> nat.

Lemma high_weight_jobs: forall (s1 s2 jobs: nat) (S: list nat), 
  jobs > 0 ->
  length S > 0 ->
  weights s1 S 0 > weights s2 S 0 -> 
  count s1 (schedule jobs S) > count s2 (schedule jobs S).
Proof.
 intros.
 induction S as [ | h tl IHS].
 + simpl in *. inversion H0.
 + 
 Admitted.

【问题讨论】：

你的定理结论不是从你给出的前提中得出的。您必须添加有关这些功能的更多信息。另外，请不要使用大写的 S 来表示 list nat，这会使代码更难阅读，因为按照约定，S 代表 nat 的构造函数。
@larsr 鉴于函数“计划”正在使用“权重”，我认为不需要更多假设。如果您知道建议添加更多信息或假设的反例，请分享。

标签： list coq proof reasoning

【解决方案1】：

您应该首先考虑需要证明这三个函数的哪些属性。根据这 3 个函数的定义来证明 3 个函数的组合属性通常不是一个好主意。首先证明 3 个单独函数的属性，然后根据这些单独的函数属性证明组合属性。

您可以先将这些属性声明为公理，然后看看它们是否确实足以证明您想要的东西，然后再证明它们。我发现这种方法有时更有效，因为我有时会重新编写语句，以便它们在证明中更方便。

我也常用模块来抽象函数的定义，只用函数的指定属性来证明派生的属性。通过这种方式，您可以从函数的实际实现中抽象出这些属性。如果您以后需要以某种方式扩展其中一个功能，这将很有帮助。如果所有属性仍然成立，则派生证明不会受到影响。如果你根据定义做证明，任何这样的证明很可能会随着函数的变化而中断。

为了进一步讨论，我建议您说明您认为需要证明这一点的 3 个函数的规范/属性。

【讨论】：

@M Soegtrop 你是对的，这将是正确的方法。您能否建议一些腋窝但很容易证明的引理，这将使我们能够证明主要引理？
如果不知道你的函数应该做什么，就无法回答这个问题。也许你可以从简单的英文描述你的函数应该做什么开始。
P.S.：上面你问了一个反例：count 可以是总是返回零的函数。那么你的引理显然不成立。
@M Soegtrop 在我们的定义中，当count 给出0 时，函数weights 也返回0，因此我们可以通过对假设weights s1 S 0 > weights s2 S 0 -> 的反转来结束这种情况。
给出可以证明一个反例错误的条件并没有多大帮助。您需要说明允许您证明您的陈述的条件。如果这对您有帮助，请想一个反例，它满足上述条件，但仍不满足您的陈述。然后想想你需要什么条件才能使这个反例出错。重复这一点，直到你再也找不到任何反例为止。然后我们也许可以讨论一个证明。