时间戳

首页 > 解决方案 > 在 Coq 中证明矛盾

coq - 在 Coq 中证明矛盾

问题描述

我试图用 来证明一个简单的引理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

标签： coqproof

解决方案

当假设不同的构造函数之间相等时（在这种情况下H : false = true），您可以使用discriminate.

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

推荐阅读