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