存在主义假设的策略

Question

假设我们有一个命题P1 n，并且它成立存在n。此外，我们有一个命题P2，其中P1 n对于任何n意味着P2。我们如何证明P2？

Parameter P1 : nat -> Prop.
Axiom some_p1 : exists n, P1 n.

Parameter P2 : Prop.
Axiom p1_implies_p2 : forall n, P1 n -> P2.

Theorem p2 : P2.

我尝试了

Proof.
  eapply p1_implies_p2.

这给了我目标 P1 ?n，但我不确定如何从那里继续。

Answer 1

您可以消除some_p1以获得证人n和假设Hn。

Theorem p2 : P2.
  case some_p1 ; intros n Hn.  apply (p1_implies_p2 _ Hn).
Qed.

Answer 2

为了完整起见，如果您使用 SSReflect 证明语言，Pierre 的证明思路将如下所示：

Theorem p2 : P2.
Proof. move: some_p1 => [n p1n]. exact: (p1_implies_p2 p1n). Qed.

请注意，为 p1_implies_p2 提供第二个参数 p1n 就足够了，因为省略了第一个参数一，n，可以由 Coq 推断。