Coq 变量存在于列表中

Question

我在证明列表中存在的变量时遇到问题。我怎样才能证明这样的事情：

Lemma exists_in_list_helper: forall (X : Type) (a : X) (P : X -> Prop),
        (exists b : X, In b [a] -> P b) ->
        P a.
Proof.
Admitted.

我还有一个问题。我如何对列表中的值进行案例分析（如果它存在于列表的这一部分中）？这是我要证明的主要引理。任何帮助表示赞赏：

Lemma in_list: forall (X : Type) (a : X) l (P : X -> Prop),
        (a :: l <> [] /\ exists b : X, In b (a :: l) -> P b) ->
        (P a /\ l = []) \/
        (P a /\ l <> [] /\ exists b : X, In b l -> P b) \/
        (P a /\ l <> [] /\ forall b : X, In b l -> ~ P b) \/
        (~ P a /\ l <> [] /\ exists b : X, In b l -> P b).
Proof.

谢谢，

Answer 1

对于第一个，我想说你可能还需要这样一个事实，即 X 上的相等性是可判定的：要么 a = b 和你可以替代，要么 a <> b 和你得到一个矛盾，但你需要能够进行这样的案例分析。

对于第二个，您可以删除 a :: l <> [] 部分，它始终为真，不会给您任何信息。而且我很确定你也需要可判定的平等（出于同样的原因）。

Answer 2

你的第一个引理似乎不太可能：我们知道存在 b 使得 P b 成立当且仅当 b \in [a]。但是，我们不知道 b \in [a] 是否成立，因此似乎很难证明。您也许可以将您的陈述视为：

Lemma exists_in_list_helper (X : Type) (a : X) (P : X -> Prop) :
        (exists b : X, a = b -> P b) ->
        P a.

然后，它不会紧跟a = b。您可能需要一个引理，例如：

Lemma in1 T (x y : T) : In x [y] <-> x = y.
Proof.
split; intros H.
+ now apply in_inv in H; case H.
+ now rewrite H; constructor.
Qed.

关于你的第二个问题，我不确定我是否完全理解你引理的意图。通常，一个人想要：

forall x l, x \in l \/ x \notin l

但这需要对 x 类型的等式的可判定性，参见引理 in_dec。如果你在 l1, l2 中拆分一个列表 l，那么它将遵循：

x \in l1 ++ l2 <-> x \in l1 \/ x \in l2

允许案例推理。 math-comp 的 path.v 给出了更多有趣的工具，它允许以一种方便的方式推导：

x \in l -> { l1, l2 & l = l1 ++ [x] ++ l2 }

其中 { x & P x} 是 exists x, P x 的 Type 版本。

Coq 变量存在于列表中

Coq variable exists in list

coq

formal-verification