January 27, 2018

# Exfalso in Coq

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:

``````Lemma not_bassn_bnot__bassn : forall b st,
~ bassn (BNot b) st -> bassn b st.
``````

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`:

``````Lemma not_bassn_bnot__bassn : forall b st,
~ bassn (BNot b) st -> bassn b st.
Proof.
unfold not. unfold bassn.

(* === GOAL STACK =================================================== *)

1 subgoal
______________________________________(1/1)
forall (b : bexp) (st : state),
(beval st (BNot b) = true -> False) -> beval st b = true

``````

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

``````Lemma not_bassn_bnot__bassn : forall b st,
~ bassn (BNot b) st -> bassn b st.
Proof.
unfold not. unfold bassn. simpl. intros b st H.

(* === GOAL STACK =================================================== *)

1 subgoal
b : bexp
st : state
H : negb (beval st b) = true -> False
______________________________________(1/1)
beval st b = true

``````

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

``````Lemma not_bassn_bnot__bassn : forall b st,
~ bassn (BNot b) st -> bassn b st.
Proof.
unfold not. unfold bassn. simpl. intros b st H.
destruct (beval st b); simpl in H.

(* === GOAL STACK =================================================== *)

2 subgoals
b : bexp
st : state
H : false = true -> False
______________________________________(1/2)
true = true
______________________________________(2/2)
false = true

``````

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

``````Lemma not_bassn_bnot__bassn : forall b st,
~ bassn (BNot b) st -> bassn b st.
Proof.
unfold not. unfold bassn. simpl. intros b st H.
destruct (beval st b); simpl in H.
- reflexivity.
- (* ... ? *)

(* === GOAL STACK =================================================== *)

1 subgoal
b : bexp
st : state
H : true = true -> False
______________________________________(1/1)
false = true

``````

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`:

``````Lemma not_bassn_bnot__bassn : forall b st,
~ bassn (BNot b) st -> bassn b st.
Proof.
unfold not. unfold bassn. simpl. intros b st H.
destruct (beval st b); simpl in H.
- reflexivity.
- exfalso.

(* === GOAL STACK =================================================== *)

1 subgoal
b : bexp
st : state
H : true = true -> False
______________________________________(1/1)
False

``````

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

``````
Lemma not_bassn_bnot__bassn : forall b st,
~ bassn (BNot b) st -> bassn b st.
Proof.
unfold not. unfold bassn. simpl. intros b st H.
destruct (beval st b); simpl in H.
- reflexivity.
- exfalso. apply H.

(* === GOAL STACK =================================================== *)

1 subgoal
b : bexp
st : state
H : true = true -> False
______________________________________(1/1)
true = true

``````

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

``````Lemma not_bassn_bnot__bassn : forall b st,
~ bassn (BNot b) st -> bassn b st.
Proof.
unfold not. unfold bassn. simpl. intros b st H.
destruct (beval st b); simpl in H.
- reflexivity.
- exfalso. apply H. reflexivity.
Qed.
``````

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.