Anwenden einer Funktion auf beide Seiten einer Gleichheit in Coq?

Question

Ich bin in Coq versuchen zu beweisen, dass

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

Ich bin mit Induktion über n. Der Basisfall ist trivial, also bin ich an der induktiven Fall und mein Ziel wie folgt aussieht:

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

Jetzt natürlich ist es ein fundamentaler Grundsatz von Funktionen, die

a = b -> f a = f b 

Für alle Funktionen f : A -> B behauptet. So konnte ich negb auf beiden Seiten anwenden, die mir geben würde

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

Was ich meine induktive Hypothese von rechts verwenden lassen würde nach links, die Negationen auf dem rechte Seite würde sie gegenseitig aus, und die Defintion von evenb abbrechen würde vervollständige den Beweis.

Nun könnte es vielleicht einen besseren Weg geben, diesen speziellen Satz zu beweisen (edit: da ist, ich habe es anders gemacht), aber da dies im Allgemeinen eine nützliche Sache zu sein scheint, wie kann man eine Gleichheit ändern Ziel in Coq durch Anwendung einer Funktion auf beiden Seiten?

Hinweis: Ich weiß, dass dies für keine beliebige Funktion funktionieren würde: Sie könnten es zum Beispiel verwenden, um -1 = 1 zu beweisen, indem Sie abs auf beide Seiten anwenden. Es gilt jedoch für jede injektive Funktion (eine für die f a = f b -> a = b), die negb ist. Vielleicht ist eine bessere Frage zu stellen, dann ist eine Funktion gegeben, die auf einem Vorschlag funktioniert (zum Beispiel negb x = negb y -> x = y), wie kann ich diese Funktion verwenden, um das aktuelle Ziel zu ändern?

Answer 1

Es scheint, dass Sie nur die apply Taktik wollen. Wenn Sie ein Lemma negb_inj : forall b c, negb b = negb c -> b = c haben, würde apply negb_inj auf Ihr Ziel genau das geben.