-2

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

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.

谢谢，

4

2 回答 2

1

你的第一个引理似乎不太可能：我们知道存在一个持有 iff的b这样的。但是，我们不知道是否成立，因此似乎很难证明。您也许可以将您的陈述视为：P bb \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。如果您在 中拆分列表l，l1, l2则如下所示：

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}的Type版本在哪里exists x, P x。

于 2016-09-16T07:21:27.593 回答
-1

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

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

于 2016-09-16T07:08:16.817 回答