证明Coq中存在矛盾

Question

我试图用Coq证明一个简单的引理，我在排除一个不可行的情况时遇到了一些麻烦。这是我的引理：

Theorem helper : forall (a b : bool),
  ((negb a) = (negb b)) -> (a = b).
Proof.
  intros a b.
  intros H.
  destruct a.
  - destruct b.
    + reflexivity.
    + (** this case is trivially true *)

相关的子目标很简单，因为假设H是假的。我如何告诉Coq？

1 subgoal
H : negb true = negb false
______________________________________(1/1)
true = false

Answer 1

如果存在不同构造函数之间相等的假设（在本例中为H : false = true），则可以使用discriminate.

在其他情况下，当您将False作为假设时，您可以使用contradiction.