如何在Coq证明中简化假设A ∨ A为A？

嘿，这个问题一点都不傻！很多刚接触Coq的小伙伴都会碰到这类逻辑化简的小困扰，我来给你分享几个实用的方法：

• 直接调用自动化策略：Coq的tauto或者firstorder这类策略能自动处理这种简单的逻辑重言式。如果你的假设是H: A ∨ A，直接在证明里敲tauto.或者firstorder.，不仅能把H化简成A，甚至可能直接帮你完成后续的目标推导。

• 用标准库的现成定理：Coq标准库里有个叫or_idempotent的定理，它的逻辑就是A ∨ A ↔ A（双向等价）。你可以用apply or_idempotent in H.这句命令，直接把假设H从A ∨ A转换成A，一步到位，完全不会拆分目标，非常高效。

• 手动推导（适合理解原理）：如果你想搞明白背后的逻辑，也可以手动操作——虽然destruct H会生成两个目标，但因为两个分支都是A，你可以在每个分支里用assumption或者auto快速解决。不过这种方法会多一步操作，不如前面两种省事。

给你举个具体的例子，用or_idempotent的写法：

Lemma simplify_or : forall A : Prop, A ∨ A → A.
Proof.
  intros A H.
  apply or_idempotent in H.
  exact H.
Qed.

要是用自动化策略的话，会更简洁：

Lemma simplify_or : forall A : Prop, A ∨ A → A.
Proof.
  intros A H.
  tauto.
Qed.

备注：内容来源于stack exchange，提问作者Lepticed