在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你的目标就会给你带来这样的结果。