存在假设的策略
Tactic for existential hypothesis
假设我们有一个命题 P1 n，并且它成立 exists n。此外，我们有一个命题 P2，其中 P1 n 意味着 P2 对于任何 n。我们如何证明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，但我不确定如何从那里继续。
您可以消除 some_p1 以获得证人 n 和假设 Hn。
Theorem p2 : P2.
case some_p1 ; intros n Hn. apply (p1_implies_p2 _ Hn).
Qed.
为了完整起见，如果使用 SSReflect 证明语言，Pierre 的证明思路将如下所示：
Theorem p2 : P2.
Proof. move: some_p1 => [n p1n]. exact: (p1_implies_p2 p1n). Qed.
请注意，为 p1_implies_p2 提供第二个参数 p1n 就足够了，因为省略的第一个 n 可以由 Coq 推断。
假设我们有一个命题 P1 n，并且它成立 exists n。此外，我们有一个命题 P2，其中 P1 n 意味着 P2 对于任何 n。我们如何证明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，但我不确定如何从那里继续。
您可以消除 some_p1 以获得证人 n 和假设 Hn。
Theorem p2 : P2.
case some_p1 ; intros n Hn. apply (p1_implies_p2 _ Hn).
Qed.
为了完整起见，如果使用 SSReflect 证明语言，Pierre 的证明思路将如下所示：
Theorem p2 : P2.
Proof. move: some_p1 => [n p1n]. exact: (p1_implies_p2 p1n). Qed.
请注意，为 p1_implies_p2 提供第二个参数 p1n 就足够了，因为省略的第一个 n 可以由 Coq 推断。