我该如何处理这个`false = true`情况？

Question

我正在尝试证明以下引理。

Inductive bool : Type :=
  | true
  | false.

Lemma andb_true_iff : forall b1 b2 : bool,
  b1 && b2 = true <-> b1 = true /\ b2 = true.
Proof.
  intros.
  split.
  - intros. split.
    + destruct b1.
      * reflexivity.
      * discriminate.
    + destruct b2.
      * reflexivity.
      * simpl. 

现在我明白了

1 goal
b1 : bool
H : b1 && false = true
______________________________________(1/1)
false = true

这是非常荒谬的，因为

false = true

从来都不是真的。然而，我不能歧视这个目标。

好吧，也许我们应该证明

H

是 False，这是准确的

false = true

。我们不能拒绝证明我们认为错误的目标。但是，为什么我连这个目标都不能重写为

False

呢？是因为我们还没有证明吗？所以我证明以下

Lemma false_true: (false = true) -> False.
Proof.
  intros.
  simpl in H.
  discriminate H.
Qed.

并且似乎

Lemma false_true

不能应用于这个目标。相反，我知道我可以编写以下引理来执行重写

Lemma false_true2: (false = true) = False.
Proof. Admitted.

但是，我认为

false_true

和

false_true2

在某种程度上非常相似。有什么办法可以不用用

false_true2

重写，而直接应用

false_true

吗？

或者我必须写以下内容才能申请吗？

Lemma false_true3: False -> (false = true).
Proof.
  intros.
  destruct H.
Qed.

==注意==

我已经通过破坏

b1

解决了这个问题。但是，我想知道有什么办法可以解决

false = true

，因为它对我来说看起来很奇怪。

Answer 1

如果你在目标中无法证明某些东西，但假设中存在矛盾，例如 False，那么你可以忽略目标，并使用矛盾，因为“ex falso quodlibet”，来自 False 遵循任何内容。

在 Coq 的逻辑中，虚假通常表示为假设您有一个空集中的值、一个不可能创建的值，或者具有不同构造函数的两个值相同（后者是 false，因为构造函数被定义为单射）。

证明通常是通过考虑可能导致这些（不可能的）值最终成为假设的情况来完成的，并且由于实现这一点的方法为零，因此您没有任何情况需要考虑，并且目标已得到证明。

例如，如果您的假设中有一个术语

H : False

，您可以直接执行

destruct H

。如果您有

false = true

（这是

bool

类型值的两个不同构造函数），那么您可以使用

inversion

。

另请查看如何从错误的假设中证明错误？

顺便请注意，

false

（值）与

False

（类型或命题）不同，

且无法证明

(false = true) = False

。不过你可以证明

false = true <-> False

。