## Home

# 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.