问题描述
我们正在努力验证具有三个功能的系统，如下所示。但是，我们不知道如何进一步进行这样的证明。 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 个函数的规范/属性。