这两个证明是等价的吗？

Question

我刚刚完成这里的练习：https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html; however I came up with 2 different proofs for following exercise https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html#andb_true_elim2，我想知道

我的第一次尝试是完全没有意义的吗？虽然它有效，但它需要引入假设 H : b && false = true，这显然是错误的。 我怎么还不停的介绍这种说法呢？

Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c.
  destruct c.
  reflexivity.
  intro H.
  rewrite <- H.
  destruct b.
  reflexivity.
  reflexivity.
  Qed.

第二次尝试：没有可疑的假设，并且有效。

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c.
  destruct b eqn:Eb.
  intro H.
  rewrite <- H.
  reflexivity.
  destruct c.
  reflexivity.
  discriminate.
  Qed.

既然 Coq 对这两个证明都很满意，那么它们同样好（我对此表示怀疑）?

Answer 1

有一个 False 假设在 Coq 中很常见并且根本没有问题。事实上，如果你看一个命题的否定P，它被定义为P -> False。换句话说，您可以从 P.

得出矛盾

甚至还有策略exfalso，只要你提供False的证明，就可以证明任何目标。这意味着如果您有相互矛盾的假设，那么您可以得出结论。

这是一个更短的证明：

Theorem andb_true_elim2 :
  forall b c : bool,
    andb b c = true ->
    c = true.
Proof.
  intros b c h.
  destruct b.
  - simpl in h. (* h : c = true *)
    exact h.
  - simpl in h. (* h : false = true *)
    discriminate h.
Qed.

我使用策略 discriminate 来关闭目标，因为看到 false = true 是不可能的，因为它们是 bool.

的两个不同的构造函数

这两个证明是等价的吗？

Are those two proofs equivalent?

coq