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

← return home