When are the constructors of an inductive type exhaustive?

1
votes

For a simple inductive type like the natural numbers nat, it is easy to prove that the two constructors (zero and successor) give all possible natural numbers,

Lemma nat_destruct (n : nat) : n = O \/ exists m : nat, n = S m.
Proof.
  destruct n. left. reflexivity. right. exists n. reflexivity.
Qed.

However I hear it is not so simple for equality proofs. There is only one equality constructor, eq_refl, but Coq cannot prove that

eq_destruct : forall (A : Type) (x : A) (prEq : x = x), prEq = eq_refl

What exactly blocks this proof ? Probably a first problem is that equality is not just a type, but a type family eq : forall A : Type, A -> A -> Prop. Is there a simpler type family where such a proof is impossible ? With 1 or 2 arguments instead of 3 maybe ?

1
coq

1 Answers

2
votes

I wrote about this issue in a blog post. In general, this arises when you define a type family over a type that does not have decidable equality. For example, consider the following type:

Inductive foo : Type -> Type :=
| Foo : foo unit.

It is not possible to show (I am pretty sure) that every inhabitant of foo unit is of the form Foo.

This phenomenon is easier to see at the level of proof terms. When you destruct a term of such a family, you must generalize over the index of the family. You can only relate this index to a known shape such as unit if the type has decidable equality.