假设，我有一个自然数，不能为零。当我们加上这个数时到另一个函数，其输出也是自然数。我必须证明这两个等于零的值相加的结果是错误的。我不应该探讨f，因为在非零项中加任何东西，等于零就是错误的陈述。
`H：（m =？0）=假
（f + m =？0）=假`
Require Import Lia.
rewrite !Nat.eqb_neq; lia.
我很抱歉出现这个问题。从历史上看，Coq中有关等式的大多数推理都是通过eq概念，符号m = n进行的，而不是您在此依赖的布尔等式。同样重要的是要知道Coq具有“不等式”或“不等式”的特定表示法：m <> n代表~ (m = n)。
因此，如果您添加键入的以下语句，将会有一个简单的解决方案：
Require Import Arith Lia.
Lemma example1 f m : m <> 0 -> f + m <> 0.
Proof. lia. Qed.
不幸的是，这不适用于您表达陈述的方式：
Lemma example2 f m : (m =? 0) = false -> (f + m =? 0) = false.
Proof.
Fail lia.
如果使用以下模式调用Search，则会看到布尔比较表达式在逻辑上等同于基本相等，但前提是您使用特定的定理来表达此表达式：
Search (_ =? _).
Nat.eqb_refl: forall x : nat, (x =? x) = true
beq_nat_refl: forall n : nat, true = (n =? n)
Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
Nat.eqb_spec: forall x y : nat, Bool.reflect (x = y) (x =? y)
beq_nat_eq: forall n m : nat, true = (n =? m) -> n = m
beq_nat_true: forall n m : nat, (n =? m) = true -> n = m
Nat.eqb_eq: forall n m : nat, (n =? m) = true <-> n = m
beq_nat_false: forall n m : nat, (n =? m) = false -> n <> m
Nat.eqb_neq: forall x y : nat, (x =? y) = false <-> x <> y
Nat.pow2_bits_eqb: forall n m : nat, Nat.testbit (2 ^ n) m = (n =? m)
Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
Nat.eqb_compare:
forall x y : nat, (x =? y) = match x ?= y with
| Eq => true
| _ => false
end
Nat.setbit_eqb:
forall a n m : nat,
Nat.testbit (Nat.setbit a n) m = ((n =? m) || Nat.testbit a m)%bool
Nat.clearbit_eqb:
forall a n m : nat,
Nat.testbit (Nat.clearbit a n) m = (Nat.testbit a m && negb (n =? m))%bool
Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
但是没有一个定理表达与0相等的加法的相互作用。您也可以使用更精确的模式来看到它。
Search (_ =? _) 0 (_ + _).
这不返回任何内容。
另一方面，如果您键入
Search (_ = _) 0 (_ + _).
您看到许多定理，其中一个与您的问题有关。
Nat.eq_add_0: forall n m : nat, n + m = 0 <-> n = 0 /\ m = 0
并且如果用_ = _而不是_ =? _表示，则足以解决问题。因此，要解决您的特定问题，我们首先需要将使用_ =? _的比较转换为等式语句，然后使用可用的定理进行逻辑推理。在第一个搜索结果中，我们有适合您情况的定理Nat.eqb_neq。继续上面的example2证明，我们可以这样写：
Rewrite !Nat.eqb_neq.
The goal becomes:
f, m : nat
============================
m <> 0 -> f + m <> 0
现在，我们可以使用定理Nat.eq_add_0进行逻辑推理。
rewrite Nat.eq_add_0.
我们可以像这样一步一步完成证明。
intros mn0 [fis0 mis0]; case mn0; assumption.
我们也可以要求自动工具为我们完成证明：
tauto.
但是在时间上往后一点，我们也可以在用Nat.eqb_neq重写后观察该语句。这是线性算术中的一条语句（它包含比较，自然数，并且变量之间无积）。这种说法属于该理论的策略范围，现在最常用的是lia。