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

如何解决使两个任意变量在Coq中相同

我有以下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.

解决方法

我不确定您所说的“语义论证”是什么意思，但是这种证明策略是不正确的，无论是书面形式还是Coq形式。例如，考虑以下语句：

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

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

,

您的论点test x = false -> test l' = false不正确，因为变量x和l都被普遍量化，因此可以具有任何值。您可能只是在假设中两个变量之间有特定的关系，但事实并非如此，除了关系filter test (l' :: l) = x :: lf之外，它告诉您x可能是l的元素，尚未经过检验过滤（但也可能是l'）。

这里不应该使用inversion，因为您的问题确实很简单。您的想法是进行归纳是很好的：

• 首先尝试简化一些假设。
• 然后查看是否有不同情况要处理，并在需要时使用destruct（在此问题中为test l'的值）
• 那么您应该能够解决问题（您可能必须使用的最复杂的策略是injection）