Apply function to both sides of equality in Coq?

Question

I'm in Coq trying to prove that

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

I use induction on n . The base case is trivial, so I'm in an inductive enclosure, and my goal is like this:

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

Now, of course, there is a fundamental axiom of functions that states

 a = b -> fa = fb 

For all functions f : A -> B So I could apply negb to both sides, which would give me

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

Which would allow me to use my inductive hypothesis from right to left, negations from the right would evenb each other out, and evenb would complete the proof.

Now there may be a better way to prove this particular theorem (editing: yes, I did it differently), but since it seems like a useful task at all, how can I change the goal of equality in Coq by applying the function to both sides?

Note. I understand that this will not work for any arbitrary function: for example, you can use it to prove that -1 = 1 , applying abs to both sides. However, it holds for any injective function (for which fa = fb -> a = b ) such that negb . Perhaps then it is better to ask a question by asking a function that works on the sentence (for example, negb x = negb y -> x = y ), how can I use this function to change the current target?

Answer 1

It seems you just need apply tactics. If you have the negb_inj : forall bc, negb b = negb c -> b = c lemma negb_inj : forall bc, negb b = negb c -> b = c , doing apply negb_inj for your purpose will give you exactly that.