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

其实对于你的助记定理来说很简单，如果你只展开不 。

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.