I had never completely understood the purpose of the exfalso tactic in Coq until I needed to prove a supporting lemma stating that a double negative boolean assertion can be rewritten to its positive equivalent:

The proof is quite brief; we can start by unfolding the logical negation (~), and then bassn, which is essentially a wrapper around the boolean expression evaluation function beval:

Simplifying replaces the BNot expression with a corresponding call to the negb function, and intros arranges everything into the context:

Based on the common expression shared between the context and the goal, destruction of beval st b is up next, giving us two subgoals:

The first is trivial by reflexivity. The second is more interesting:

When I first started learning how to write Coq proofs, this type of situation confused me to no end. How can we complete a proof if the goal is clearly not provable?

In a handwritten proof, this case would be solved with a single sentence proof by contradiction. Recall that in a proof by contradiction, one assumes P is true but Q is false, but since this leads to a contradiction, Q must be true. A proof of contradiction here would read:

If the statement "true does not equal true" is true, but the statement "false equals true" is false, we have a contradiction, and thus "false equals true" is true.

But in Coq, we actually go in reverse:

We can prove that "false equals true" is a true statement in a world where "true does not equal true," owing to the fact that they are both falsehoods.

In practice, this involves applying the exfalso tactic to replace the goal with False:

We then apply H; essentially, we’re “cancelling out” the falsehood of the goal with the falsehood of the assumption H:

Finally we’re left to prove true = true, which is obvious:

Of course, in keeping with the term “proof by contradiction,” the exfalso and apply H steps can be replaced with contradict H. But I think it’s interesting to consider the actual direction the Coq proof is proceeding in, which to me isn’t so much by contradiction as it is by a “cancelling out” of related falsehoods in the context and the goal. This perspective is what ultimately helped me understand what’s going in proofs such as this one.