 # Eliminate from Prop into Set when the prop is effectively singleton?

Consider the following three definitions, where f3 doesn’t typecheck:

``````Inductive function_true : Prop := mk_function_true.
Inductive function_false : Prop := mk_function_false.
Definition function_pred (b : bool) : Prop :=
match b with
| true => function_true
| false => function_false
end.

Definition f1 (p : function_pred true) : unit :=
match p with
| mk_function_true => tt
end.

Inductive family_set : bool -> Set :=
| family_set_true : family_set true
| family_set_false : family_set false.

Definition f2 (p : family_set true) : unit :=
match p with
| family_set_true => tt
end.

Inductive family_pred : bool -> Prop :=
| family_true : family_pred true
| family_false : family_pred false.

Definition f3 (p : family_pred true) : unit :=
match p with
| family_true => tt
end.
``````

It seems like morally f1 and f3 are doing the same thing. I understand that under the hood the return type of the match in f2 and f3 is (if b then unit else IDProp), but even with that is there any reason f3 couldn’t be accepted here?

To be clear, the condition I’m looking for is “if P : Prop is effectively a singleton once its known indices are taken into account, we can eliminate into Set/Type”.

No reason, except that, as you say, a lot of work is already performed under the hood to find the proper return type. In your case, it happens that work is not enough. So, the `f3` function can be written, but you have to help Coq by adding an intermediate step (e.g., `let in`), so that `p` is eliminated into `Prop` before its content can be used into `Set` or `Type`.

I suspect that what @silene means is:

``````Lemma coe {b} : family_pred b -> family_set b.
Proof.
destruct b; constructor.
Defined.

Definition f3 (p : family_pred true) : unit :=
match coe p with
| family_set_true => tt
end.
``````

A related question is the item “Extended detection of computationally-void inductive propositions” in this list of Coq wishes: the syntactic criterion used to detect when an elimination from Prop to Type is legal could in theory be extended a bit further, especially by splitting the constructor into disjoint classes depending on the indices.

Hm, can you give an example of this? It seems like @herbelin’s example is actually matching on the bool, which may get me what I want but I’m curious if your approach is different?

Ah, I think I’ve got it:

``````Definition f (p : family_pred true) : unit :=
let t : True := match p in family_pred t return match t return Prop with
| true => True
| false => IDProp
end with
| family_true => I
| family_false => idProp
end
in match t with
| I => tt
end.``````

A more complete example that really illustrates it

``````Definition f (p : family_pred true) : unit :=
let t : True :=
match p in family_pred t
return match t return Prop with
| true => t = true → True
| false => t = true → False
end
with
| family_true => λ _, I
| family_false =>
λ p, match p in eq _ t
return if t then False else IDProp
with eq_refl => idProp end
end eq_refl
in match t with
| I => tt
end.``````

Yes, that is more or less what I had in mind.

Or rather, I was expecting the following version to work:

``````Definition f3 (p : family_pred true) : unit :=
let p : True :=
match p with
| family_true => I
end in
tt.
``````

But Coq seems confused (due to a bug?), so one has to desugar by hand:

``````Definition f3 (p : family_pred true) : unit :=
let p : True :=
match p as p in family_pred b return ((if b then True else IDProp) : Prop) with
| family_true => I
| family_false => idProp
end in
tt.
``````

Notice the `(_ : Prop)` coercion, which is the part that Coq fails to infer.

But Coq seems confused (due to a bug?)

If I’m correct, the “bug” is that Coq internally uses `if b return Type then True else IDProp` instead of the expected `if b return Prop then True else IDProp` in its inference of the return clause. Notice the `(_ : Prop)` coercion, which is the part that Coq fails to infer.

So, exactly.