::

The other day I was working on a project where I was dealing with some finite sets of objects. I had chosen to use Coq’s Ensembles to represent these sets. They’re a nice abstract, high level representation of a set that allows you to not worry about the too many structural details of the set itself.

I reached a point where I needed some functions that could use the decidability of membership in these sets to perform their computations. In other words, I needed to be able to computationally decide if any given item was in a specific set or not. This did not seem unreasonable… at first:

``````
Theorem finite_mem_dec_try : forall E x,
Finite X E ->
{In X E x} + {~In X E x}.
Proof.
intros E x fin.
``````

So I started out with the following proof goal:

``````
E : Ensemble X
x : X
fin : Finite X E
============================
{In X E x} + {~ In X E x}
``````

From here I thought I could break down the cases for Finite and I’d be on my way (one case for Empty_set, and one for the set with an added member). > Error: Case analysis on sort Set is not allowed for inductive definition Finite.

Oh, okay, that made sense. Finite is defined like this:

``````
Inductive Finite : Ensemble U -> Prop :=
| Empty_is_finite : Finite (Empty_set U)
| Union_is_finite :
forall A:Ensemble U,
Finite A -> forall x:U, ~ In U A x -> Finite (Add U A x).
``````

And so it’s just a property built from an Ensemble… which looks like this:

``````
Definition Ensemble := U -> Prop.
``````

So Finite is a Type -> Prop -> Prop… and that makes sense — I’m not allowed to do case analysis on it when the goal is strictly in sort Set (*if the disjunction where not a sumbool (which lives in sort Set) and were instead an or (which lives in sort Prop), we would be able to use induction on the assumption of finiteness).

After seeing this and unfolding several definitions, my proof goal looked like this:

``````
E : Ensemble X
x : X
fin : Finite X E
============================
{E x} + {~ E x}
``````

At this point I was thinking perhaps membership decidability for Ensembles was not possible (*again, for a sumbool conclusion). There was no real “evidence” when restricted to the sort Set regarding the members I wished to inspect.

After a chat or two with some respected colleagues, it appeared this was very similar to the law of excluded middle (*when induction on the finiteness of the Ensemble is not available). What we were looking at was the decidability of some property with little or no evidence to work with. This is fine in classical logic, but not in Coq (which is based on the Calculus of Inductive Constructions and thus restricted to constructive logic). In Coq, evidence to prove either the property or the negation of the property must be present.

At this point I decided I would only be satisfied with this apparent failure by proving this problem was in fact equivalent to the heretical law of excluded middle!

I created a module with a type with decidable equility (the thing populating the sets), an assumption that all Ensembles of this type were finite, and the assumption that membership in these Ensembles was indeed decidable:

``````
Variable X : Type.
Hypothesis eq_X_dec :
forall x y : X, {x=y} + {x<>y}.

Hypothesis all_finite : forall E : Ensemble X, Finite X E.

Theorem finite_mem_dec : forall E x,
{In X E x} + {~In X E x}.
Proof.
``````

I introduced the intended target (the law of excluded middle) and opened a proof to work in:

``````
Definition excluded_mid := forall A, {A} + {~A}.

Theorem fin_mem_imp_excl_mid : forall x : X,
excluded_mid.
Proof.
intros x A.
``````

Now, from my assumption of membership decidability, I didn’t have the decidability of any property… but of any X -> Prop. Hmm… so what if I had a function from X to Prop I could use with membership decidability?

``````
remember (fun x : X => A) as f.
remember (finite_mem_dec f x) as mem_dec.
unfold In in *.
``````

Now we have:

``````
x : X
A : Prop
f : X -> Prop
Heqf : f = (fun _ : X => A)
mem_dec : {f x} + {~ f x}
Heqmem_dec : mem_dec = finite_mem_dec f x
============================
{A} + {~ A}
``````

Substitute out the function (with subst f) leaves us:

``````
x : X
A : Prop
mem_dec : {A} + {~ A}
Heqmem_dec : mem_dec = finite_mem_dec (fun _ : X => A) x
============================
{A} + {~ A}
``````

and there you have it! mem_dec is now our goal, the law of excluded middle. Qed.

Do you ever accidently find yourself trying to prove an axiom of classical logic? Perhaps it’s a “rookie mistake” =)

Source files found here