coq - Coq - 如何证明 eqb_neq？

Question

我试图证明eqb_neq：

Theorem eqb_neq : forall x y : nat,
  x =? y = false <-> x <> y.

这是我目前的证明状态：

在证明过程中，我到达了最后一步，我只需要证明附加辅助定理：

Theorem eqb_false_helper : forall n m : nat,
    n <> m -> S n <> S m.

我尝试了多种策略，但现在我什至不确定是否可以证明这个辅助定理。

我不确定如何使用归纳法证明基本情况：

我还能尝试什么？任何提示eqb_neq或辅助定理？

谢谢

Answer 1

如果您只是展开 not，那么您的辅助定理实际上非常简单：

Theorem eqb_false_helper : forall n m : nat,
    n <> m -> S n <> S m.
Proof.
unfold not; intros.
apply H; injection H0; intro; assumption.
Qed.

你实际上只需要证明那个S n = S m -> False，你假设那个n = m -> False，因此你可以证明那个S n = S m -> n = m，这就是注入假设S n = S m。