Coq：如何证明具有元素存在的列表的存在？

Question

假设我有说明元素可用性的公理：

Axiom FLP_Lemma3_p1: forall cfg, bivalent cfg -> exists msg, bivalent (run cfg [msg]).

如何证明属性同样适用于无限大的列表？

Theorem FLP_Lemma3: forall cfg, bivalent cfg -> forall m, exists s, length s > m -> bivalent (run cfg s).

其中 msg 是 nat，s 是一个 list 的 nats。

Answer 1

证明如下：

Theorem FLP_Lemma3: forall cfg, bivalent cfg -> forall m, exists s, length s > m -> bivalent (run cfg s).
Proof.
  intros. destruct (FLP_Lemma3_p1 cfg H) as [msg B].
  exists [msg]. intros. apply B.
Qed.

想法是用你的引理来获得见证，但是由于引理提供了{msg | bivalent (run cfg [msg])}，你需要把它分成两部分。您可以使用 destruct 立即执行此操作，或者首先使用 pose proof (FLP_Lemma3_p1 cfg H) as L. 引入 witness 然后销毁 L.

现在再注意一下，你试图证明的这个引理似乎有点没用。

您是否打算证明：

Theorem FLP_Lemma3: forall cfg, bivalent cfg -> forall m, exists s, length s > m /\ bivalent (run cfg s).

因为这会更有趣，但根据您的公理无法证明，因为您对 msg.

的长度一无所知

Coq：如何证明具有元素存在的列表的存在？

Coq: how to prove existence of list having existence of an element?

coq