我如何表明，如果假设不暗示，那就与说命题等于false（COQ）一样？

Question

我想证明两个字符不等。我的环境目前看起来像这样：

H: c1 = c2 -> not
_____________________
Goal: (c1 =? c2)%char = false

它不允许我应用H或重写H来解决目标，而H不可逆转。目标直接源于假设，那么我该如何证明这一点？我需要助手引理吗？

Answer 1

看起来您的假设中有一个错别字h？
您是指不是（C1 = C2）（或c1＆lt;＆gt; c2，还是c1 = c2 - ＆gt; false）？

如果是这样，您可以应用标准库的引理：

Search (_ =? _)%char. 

Goal forall c1 c2: ascii,
    c1 <> c2 -> (c1 =? c2)%char = false.
Proof.
  intros c1 c2; apply eqb_neq.
Qed.

也可能有趣的是，查看eqb_neq的证明，以了解如何证明这种引理。