Coq中使用intros模式时能否保留sigT依赖对原假设整体变量？

问题描述 #

我有一个涉及依赖对（sigT）的定理，其目标如下：

--------------------------------------------
forall x : {x : G | P x}, mult1 sub_e x = x

当我执行intros [x Px].命令后，上下文中会新增如下内容：

x : G
Px : P x

我希望能够保留该依赖对的整体变量，目前我需要额外执行set (x_pair := exist P x Px).才能将其加入上下文，得到如下上下文：

x : G
Px : P x
x_pair := exist P x Px : {x : G | P x}

请问是否可以不使用额外命令就实现这一需求？

解答 #

可以直接通过intros的引入模式实现，不需要额外执行set命令，写法如下：

intros (x_pair as [x Px]).

执行该命令后会直接生成你需要的上下文：同时保留析构出的x、Px，以及整体依赖对变量x_pair。

这种语法是Coq引入模式的通用用法，对所有归纳类型的析构都生效，比如析构普通序对时也可以用intros (ab as [a b])同时保留整体序对变量和内部的两个字段。

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