使Coq中的两个任意变量相同

Question

我有以下coq代码：

Theorem filter_exercise : forall (X : Type) (l lf : list X) (test : X -> bool)
(x : X),
filter test l = x :: lf ->
test x = true.
Proof.
intros X l lf test x eq.
induction l as [|l' l].
- inversion eq.
- inversion eq as [H].

这给了我：

X : Type
l' : X
l, lf : list X
test : X -> bool
x : X
eq : filter test (l' :: l) = x :: lf
testEq : test x = false
IHl : filter test l = x :: lf -> false = true
============================
filter test l = (if test l' then l' :: filter test l else filter test l)

在这里，如果我可以说，因为test x = false以及x和l'都是X类型的普遍量化变量，那么我就完成了证明。

然而，这是一个语义争论，我不知道如何在Coq中做到这一点。我是不是走错了路？

编辑

对于子孙后代来说，这就是我最终获得的解决方案：

Theorem filter_exercise : forall (X : Type) (l lf : list X) (test : X -> bool)
(x : X),
filter test l = x :: lf ->
test x = true.
Proof.
intros X l lf test x eq.
induction l as [|l' l].
- inversion eq.
- simpl in eq. destruct (test l') eqn:testl'.
+ inversion eq. rewrite <- H0. apply testl'.
+ apply IHl. apply eq.
Qed.

Answer 1

我不知道你说的"语义论证"；，但这种证明策略是不正确的，无论是在纸面上还是在Coq中。例如，考虑以下语句：

Lemma faulty : forall n m : nat, even n -> even m.
Proof. Admitted.

根据您的逻辑，如果n是偶数，那么m也应该是偶数，因为两者都是nat类型的通用量化变量。然而，正是，因为它们是普遍量化的，所以它们可以实例化为nat的不同值，从而产生明显矛盾的陈述。例如，如果我们用2和1实例化faulty，我们应该能够得出1是偶数的结论，这不是真的。

Answer 2

您关于test x = false -> test l' = false的论点不成立，因为变量x和l都是通用量化的，因此可以有任何值。在你的假设中，你可以在两个变量之间有一个特定的关系，但除了关系filter test (l' :: l) = x :: lf之外，情况并非如此，它告诉你x可能是l的一个元素，它没有被测试过滤(但它也可能是l’(。

您不应该在这里使用inversion，因为您的问题非常简单。然而，你想进行诱导是可以的：

• 首先尝试简化几个假设
• 然后看看是否有不同的情况需要处理，并在需要时使用destruct(关于这个问题中test l'的值(
• 那么你应该能够解决问题(你可能不得不使用的最复杂的策略是injection(