从 nat 到 bool 的不等式的简单（r）证明

Question

在做 Software Foundations 的练习时，我需要一个由下面的定理 not_eq_nat__beq_nat_false 表示的推导。在各种策略和标准定理上挣扎了一段时间后，我放弃了，决定使用下面的定理。

不过我仍然觉得应该有一种更简单的方法来证明这一点。例如它的对偶 eq_nat__beq_nat_true 就简单多了。

Require Export Arith.
Require Export Arith.EqNat.

Theorem ex_falso_quodlibet : forall (P:Prop), False -> P.
Proof.
  intros P contra.
  inversion contra.
Qed.

Theorem not_eq_nat__beq_nat_false: forall n m : nat
, n <> m -> (n =? m) = false
.
Proof.
  intros.
  unfold not in H.
  destruct (n =? m) eqn:beqval; try reflexivity.
  apply ex_falso_quodlibet. apply H.
  apply beq_nat_true; assumption.
Qed.

Theorem eq_nat__beq_nat_true: forall n m : nat
, n = m -> (n =? m) = true
.
Proof.
  intros.
  rewrite H. symmetry. apply beq_nat_refl.
Qed.

我的猜测是使用 sumbool 是解决方案。这么简单的事怎么能轻易证明呢？

根据 Vinz 的回答，以下是我要找的内容。

Theorem not_eq_nat__beq_nat_false: forall n m : nat
, n <> m -> (n =? m) = false
.
Proof.
  intros.
  apply beq_nat_false_iff. assumption.
Qed.

Theorem eq_nat__beq_nat_true: forall n m : nat
, n = m -> (n =? m) = true
.
Proof.
  intros.
  apply beq_nat_true_iff. assumption.
Qed.

确实很简单。

Answer 1

我看到你正在使用 std 引理，例如 beq_nat_true，那么你可以使用 beq_nat_false_iff。否则，如果没有来自标准库的任何引理，我会进行归纳：

Theorem not_eq_nat__beq_nat_false: forall n m : nat
, n <> m -> beq_nat n m = false
.
Proof.
  induction n as [ | n hi]; intros [ | m] h; simpl in *; try reflexivity.
  - now elim h.
  - now apply hi; intro heq; apply h; rewrite heq.
Qed.

从 nat 到 bool 的不等式的简单（r）证明

A simple(r) proof from inequality on nat to bool

coq