如何处理Coq证明中`false = true`的目标情况？

你当前在证明andb_true_iff引理时，卡在了目标false = true，以下是几种不用destruct b1的解决思路：

1. 直接应用自定义的false_true引理 #

你的false_true: (false = true) -> False引理可以通过先将目标转为False，再应用引理来使用：

exfalso.  (* 将目标从 `false = true` 转为 `False` *)
apply false_true.  (* 此时需要提供 `false = true` 的证明，直接用 reflexivity *)
reflexivity.

或者更简洁的链式写法：

exfalso; apply false_true; reflexivity.

2. 直接对假设H使用discriminate #

当前假设H: b1 && false = true本身就是矛盾的——无论b1是true还是false，b1 && false的结果都是false，不可能等于true。直接对H用discriminate就能一步完成证明：

discriminate H.

3. 使用inversion策略分析假设 #

inversion策略可以分析等式的构造结构，对H使用会直接发现矛盾：

inversion H.

4. 利用contradiction策略 #

contradiction会自动寻找上下文中的矛盾，这里它能识别出H和目标之间的冲突：

contradiction.

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