如何在Coq中利用命题等价性重写目标以完成证明？

可行方案 #

你的目标和假设FoS1仅存在p1与p2的差异，而H是两者的全域等价性，完全可以通过等价替换快速完成证明，以下是几种高效方案：

方案1：全域重写后直接匹配假设 #

默认rewrite不会自动遍历嵌套的量词结构，加上!可触发全域范围内的重写，把FoS1里所有p1替换为p2：

rewrite !H in FoS1.
assumption.

方案2：让auto自动应用等价性 #

把等价性假设H添加到auto的提示库，让它自动完成替换和匹配：

Hint Rewrite H : core.
auto.

或者用autorewrite一步到位：

autorewrite with core; assumption.

方案3：拆分合取式后逐个处理 #

如果上述方法因环境配置不生效，可拆分合取式后分别重写，逻辑更直观：

destruct FoS1 as [FoS1_l FoS1_r].
split.
- rewrite H in FoS1_l; assumption.
- rewrite H in FoS1_r; assumption.

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