將一個函數應用於Coq中的等式兩邊？

Question

我在勒柯克試圖證明

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會給你。