Применить функцию к обеим сторонам равенства в 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 на вашей цели даст вам именно это.