Coq's elimination restriction corner cases -- when can you eliminate Prop's into Type?

Question

In order to ensure soundness, and to keep axioms like proof irrelevance admissible, Coq has an "elimination restriction" on inductive types in Prop.

Consider, for example, the definition of the existential quantifier, reproduced here:

Inductive exT (A:Type) (P : A -> Prop) : Prop :=
  exT_intro : forall (a:A), P a -> exT A P.
Arguments exT_intro {_} {_} _ _.

This quantifier can be eliminated into a Q : Prop, as follows:

Definition elim_exT_Prop {T:Type} {P:T->Prop} (Q:Prop) :
  (forall (a:T), P a -> Q) ->
  (exT T P) -> Q :=
  fun H Hex => match Hex with exT_intro w Hw => H w Hw end.

However, if we want Q to have type Type, this fails:

Fail
Definition elim_exT_Type {T:Type} {P:T->Prop} (Q:Type) :
  (forall (a:T), P a -> Q) ->
  (exT T P) -> Q :=
  fun H Hex => match Hex with exT_intro _ _ w Hw => H w Hw end.

So far, so clear. There are exceptions to this "elimination restriction," namely:

• The type being eliminated has no constructor (False is the main example)
• The type being eliminated has only one constructor, and all arguments of it themselves have type Prop (and P Q is the other example, as is the well-founded recursion type)

This means that the following type, an existential quantifier quantifying over Prop, is not subject to this restriction, i.e. is computational, i.e. can be eliminated into Type:

Inductive exP (A:Prop) (P : A -> Prop) : Prop :=
  exP_intro : forall (a:A), P a -> exP A P.
Arguments exP_intro {_} {_} _ _.

(* exP can be eliminated into Type *)
Definition elim_exP_Type {T:Prop} {P:T->Prop} (Q:Type) :
  (forall (a:T), P a -> Q) ->
  (exP T P) -> Q :=
  fun H Hex => match Hex with exP_intro w Hw => H w Hw end.

However, if we take our old definition exP, and instantiate it with a proposition, it can still not be eliminated:

Fail (* even though T has type **Prop** *)
Definition elim_exT_with_Prop_into_Type {T:Prop} {P:T->Prop} (Q:Type) :
  (forall (a:T), P a -> Q) ->
  (exT T P) -> Q :=
  fun H Hex => match Hex with exT_intro _ _ w Hw => H w Hw end.

My question now is: Why is this? Does Coq's elimination restriction check not see that there is no computational content to be gained here?

If we do some extra work, we can define something of the above type, that even has the same reduction behavior:

Definition exT_to_exP {T:Prop} {P:T->Prop} : exT T P -> exP T P
  := elim_exT_Prop _ exP_intro.
Definition elim_exT_with_Prop_into_Type {T:Prop} {P:T->Prop} (Q:Type) :
  (forall (a:T), P a -> Q) ->
  (exT T P) -> Q := fun H Hex => elim_exP_Type _ H (exT_to_exP Hex).

Again, we can achieve this by doing a round-about way through something in Prop. But why is that step necessary?

Thanks!

PS: I have called this restriction "elimination restriction" following the lecture notes by Prof. Smolka at Saarland University. Is this "the name" for this? Is there another one?

Answer 1

First, let me answer your last question: as far as I know, the reference manual calls the restriction "empty or singleton elimination", I have seen "subsingleton elimination" or simply "singleton elimination" used too. Still, I would say that separating between "elimination restriction" (ie, how you restrict elimination of inductive types in one sort to other sorts) and "singleton elimination" (the particular elimination restriction used for Prop in Coq) is a sensible think to do. For instance, strict propositions have a different elimination restriction.

As for the main question, Coq's singleton elimination is very syntactic and restrictive. I would say this is by design, the idea being to keep it simple enough to be easily explained, rather than relying on a more complex condition which moreover might have a faulty implementation, and be less robust towards small changes in code, both on the user and Coq sides.

Anyway, trying to capture the full extent of irrelevance is a lost battle. If you push the idea of irrelevance to its farthest, you end up with the very semantic notion of being an hProp, a proposition in the sense of homotopy type theory. A type P : Type is an hProp whenever forall p q : P, p = q. While this adequately captures irrelevance, as it is a semantic notion it is not decidable whether a given (inductive) type is a proposition. So there is no good complete criterion, and so Coq goes for a very incomplete one, which is at least simple.

As you noticed, this means that Coq is often not able to tell that something "obviously" carries no information, and you have to explicitly go through some kind of detour to convince it to allow for the elimination you want. If you think about the previous paragraph, this is not surprising: by doing this detour, you are actually proving that what you defined is indeed irrelevant. Seen this way, it is maybe a bit less surprising that you have some work to do?

As for your specific example, the reason why exP and exT look so similar is because of the cumulativity Prop ≤ Type, which is quite a beast of its own, so avoiding interference between it and the elimination criterion seems a cautious thing to do. Moreover, in Coq's design the check of which sorts an inductive type can be eliminated into is done once and for all, when the inductive type is defined. When looking at an elimination from that type, deciding whether that elimination is allowed is just about doing a (cheap) query of a boolean from the environment. Instead, being able to detect on the fly that in a specific instance of an inductive defined with a parameter in Type that parameter is actually in Prop (meaning that in that specific case the inductive type might happen to satisfy the elimination restriction), would force a systematic recomputation of the elimination restriction, which would probably be quite costly for a very small gain.