Coq不识别命题公式代入命题变量的简单操作问题求助

你遇到的问题不是Coq的怪异行为，是你的证明策略选择错误：

• 你要证的substritwo本质是trident定义代入变量后的直接展开，本身是成立的，但你在证明时过早执行了split、rewrite triexpand和一系列destruct操作，直接把蕴含式左侧的三个denseover强前提拆碎丢弃了，最后只留下孤立的H : b假设，自然无法推出包含自由变量a的析取式a \/ (a <-> b)。
• 你现在遇到的不可证子目标是错误证明步骤生成的冗余子目标，和原引理本身的正确性无关。

这个引理只是定义的展开等价，不需要复杂的证明操作，直接展开trident后应用自反性即可完成证明：

Lemma substritwo : forall a b : Prop,
   (trident (a <-> b) a b)
<->
   (
    (
         (denseover (a <-> b) (a \/ b)) 
      /\ (denseover a (b \/ (a <-> b)))
      /\ (denseover b (a \/ (a <-> b)))
    ) -> ((a <-> b) \/ a \/ b)
   ).
Proof.
  unfold trident.
  reflexivity.
Qed.

如果你确实需要手动推理证明过程，不要提前拆前提或者重写结论，先调用intros把所有denseover相关的前提全部引入上下文后，再用intuition配合tauto也可以完成证明，不会出现你遇到的不可证子目标。

内容的提问来源于stack exchange，提问作者მამუკა ჯიბლაძე