Coq中如何通过构造实例完成存在性命题的证明

你要完成这个证明核心是用exists策略明确给出你要构造的存在量词的证据，具体操作如下：

• 首先你需要先声明my_func以及它满足的性质，示例声明如下：

Parameter my_func : nat -> nat.
Axiom my_func_zero : my_func 0 = 0.

• 接下来证明针对my_func的实例化定理时，直接用exists 0给出存在项的证据即可，完整证明流程如下：

Theorem my_thm_for_myfunc : exists t: nat, my_func t = 0.
Proof.
  exists 0. (* 告诉Coq我们选t=0作为存在的证据 *)
  apply my_func_zero. (* 直接调用已知的my_func 0=0的性质完成证明 *)
Qed.

• 如果你需要的是对任意满足n 0 = 0的函数n都成立的通用版本，可以这么写：

Theorem my_thm_general (n: nat -> nat) (H: n 0 = 0) : exists t: nat, n t = 0.
Proof.
  exists 0.
  exact H.
Qed.

逻辑说明 #

Coq 遵循构造主义的证明逻辑，要证明exists x : A, P x，就必须显式给出一个具体的A类型的项t，再证明t满足性质P。exists策略的作用就是把你给出的t填充到存在量词的位置，剩下的证明目标就变成了证明P t，用你已知的条件完成这部分证明即可。

内容的提问来源于stack exchange，提问作者Musher Soccoli