coq - 在 Coq 中对等式两边应用函数？

Question

我在 Coq 试图证明这一点

Theorem evenb_n__oddb_Sn : ∀n : nat,
  evenb n = negb (evenb (S n)).

我在 n 上使用归纳法.基本情况是微不足道的，所以我在归纳情况下，我的目标是这样的:

k : nat
IHk : evenb k = negb (evenb (S k))
============================
 evenb (S k) = negb (evenb (S (S k)))

现在当然有一个基本的函数公理断言

a = b -> f a = f b

对于所有功能 f : A -> B .所以我可以申请 negb双方，这会给我

k : nat
IHk : evenb k = negb (evenb (S k))
============================
 negb (evenb (S k)) = negb (negb (evenb (S (S k))))

这会让我从右到左使用我的归纳假设，右边的否定会相互抵消，以及 evenb 的定义将完成证明。

现在，可能有更好的方法来证明这个特定的定理(编辑:有，我用另一种方式做了)，但是由于这通常看起来是一件有用的事情，所以修改 Coq 中的相等目标的方法是什么？对双方应用一个函数？

注意:我意识到这不适用于任何任意函数:例如，您可以使用它来证明 -1 = 1通过申请 abs到双方。但是，它适用于任何单射函数(其中 f a = f b -> a = b 的单射函数)，其中 negb是。也许一个更好的问题是，给定一个对命题进行运算的函数(例如， negb x = negb y -> x = y )，我如何使用该函数来修改当前目标？

Answer 1

看来你只想要apply战术。如果您有引理 negb_inj : forall b c, negb b = negb c -> b = c , 做 apply negb_inj在你的目标上会给你确切的。