如何在Coq中使用定义？添加基于存在量词定义的假设

你已经有假设P x y，且R x定义为exists y, P x y，要把R x作为假设加入上下文，核心是用已有P x y构造出R x的证明项，而不是直接引用R x这个Prop。以下是两种可行方法：

方法1：用assert显式引入并证明 #

先声明要引入R x作为假设，再用现有假设完成证明：

(* 假设你的P x y对应的假设名为H *)
assert (H_R : R x).
- exists y. exact H.

assert会生成一个子目标让你证明R x，这里直接用exists y指定见证，再用exact H给出P x y的证明即可，完成后H_R : R x就会加入上下文。

方法2：直接构造证明项并用pose proof引入 #

如果你不想生成子目标，可以直接构造R x的证明项，再用pose proof绑定到变量：

(* H是你现有的P x y假设 *)
pose proof (ex_intro (fun y => P x y) y H) as H_R.

ex_intro是Coq中存在量词的引入规则，参数分别是：存在命题的谓词（这里可简写为_让Coq自动推断）、见证y、以及P x y的证明H。执行后H_R : R x会直接出现在上下文里。

更简洁的写法（利用Coq的自动推断）：

pose proof (exists y, H) as H_R.

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