The Coq mailing list

[Meven LENNON-BERTRAND <Meven.Bertrand AT univ-nantes.fr>]

Dear Sylvain,

Indeed, your assumption is correct: if you look at the definition to 
which case0 is elaborated by using Print case0, you can see that Coq was 
able to infer a return predicate that allows you to put any (typable) 
term in the second branch.
As to your second question, I have no clue as to why the standard 
library chose that one precise term.

Best,

Meven LENNON-BERTRAND
Doctorant, Équipe Gallinette – LS2N – Université de Nantes
www.meven.ac

Le 11/03/2022 à 08:59, Sylvain Salvati a écrit :
> Dear Coq-Club,
>
> Can anyone explain why the following term defined in the standard
> library (c.f. Coq.Vectors.VectorDef) does type-check:
>
> Definition case0 {A} (P:Vector.t A 0 -> Type) (H:P (Vector.nil A)) v:P v :=
> match v with
> |[] => H
> |_ => fun devil => False_ind (@IDProp) devil
> end.
>
> I moreover checked that the following term also type-check:
>
> Definition my_case0 {A} (P:Vector.t A 0 -> Type) (H:P (Vector.nil A)) v:P v :=
> match v with
> |[] => H
> end.
>
> So it seems to me that in the first term coq is able to see that the
> second branch of the match cannot be executed and thus one can put any
> phony term. Is it correct? If so why does the standard library use the
> first term instead of the second one?
>
> I checked the mailing list and found that a similar question has been
> asked 7 years ago but did not receive any answer.
>
> Thanks for your help,
>
> S.