Search code examples
coqproof

Proving a contradiction in Coq

I'm trying to prove a simple lemma with Coq, and I'm having some trouble ruling out an infeasible case. Here is my lemma:

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 *)

The relevant sub-goal is trivially true since the assumption H is false. How do I tell this to Coq?

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

  • When there is an assumption which is an equality between distinct constructors (in this case H : false = true), you can use discriminate.

    In other cases, when you have False as an assumption, you may use contradiction.