将函数应用于 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 中通过向两边应用函数？

注意：我意识到这不适用于任何任意函数：例如，您可以通过将abs 应用于双方来使用它来证明-1 = 1。但是，它适用于任何单射函数（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 就会给你带来的结果。