Доказательство противоречия в Coq

Question

Я пытаюсь доказать простую лемму с помощью Coq, и у меня возникли проблемы с исключением невозможного случая.Вот моя лемма:

Theorem helper : forall (a b : bool),
  ((negb a) = (negb b)) -> (a = b).
Proof.
  intros a b.
  intros H.
  destruct a.
  - destruct b.
    + reflexivity.
    + (** this case is trivially true *)

Соответствующая подцель тривиально верна, поскольку предположение H неверно.Как мне сказать это Coq?

1 subgoal
H : negb true = negb false
______________________________________(1/1)
true = false

Answer 1

Когда есть предположение, которое является равенством между различными конструкторами (в данном случае H : false = true), вы можете использовать discriminate.

В других случаях, когда в качестве предположения указано False, вы можете использовать contradiction.