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.