Applicare una funzione su entrambi i lati di un'uguaglianza in Coq?

Question

sto facendo Coq cercando di dimostrare che

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

sto usando induzione su n. Il caso base è banale, quindi sono il caso induttivo e il mio obiettivo si presenta come:

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

Ora, naturalmente, c'è un assioma fondamentale di funzioni che asserisce

a = b -> f a = f b 

Per tutte le funzioni f : A -> B. Così ho potuto applicare negb ad entrambi i lati, che mi darebbero

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

Il che mi permetteva di usare la mia ipotesi induttiva da destra a sinistra, le negazioni di destra sarebbe annullano a vicenda, e alla definizione di evenb sarebbe completa la prova.

Ora, potrebbe esserci un modo migliore per provare questo particolare teorema (modifica: c'è, l'ho fatto in un altro modo), ma come questo in generale sembra una cosa utile da fare, qual è il modo di modificare un'eguaglianza obiettivo in Coq applicando una funzione su entrambi i lati?

Nota: mi rendo conto che ciò non funzionerebbe con alcuna funzione arbitraria: ad esempio, è possibile utilizzarlo per provare che -1 = 1 applicando abs su entrambi i lati. Tuttavia, vale per qualsiasi funzione iniettiva (una per la quale f a = f b -> a = b), che è negb. Forse una domanda migliore da porre, quindi, viene data una funzione che opera su una proposizione (ad esempio, negb x = negb y -> x = y), come posso usare quella funzione per modificare l'obiettivo corrente?

Answer 1

Sembra che tu voglia solo la tattica apply. Se hai un lemma negb_inj : forall b c, negb b = negb c -> b = c, fare apply negb_inj sul tuo obiettivo ti darebbe esattamente quello.