对应用于 Coq 中 nat 列表的函数进行推理

如何解决对应用于 Coq 中 nat 列表的函数进行推理

我们正在努力验证具有三个功能的系统，如下所示。但是，我们不知道如何进一步进行这样的证明。 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.

解决方法

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

您可以先陈述诸如公理之类的性质，看看它们是否确实足以证明您想要什么，然后再证明它们。我发现这种方法有时更有效，因为我有时会重新表述陈述，以便它们在证明中更方便。

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

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