The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear Sylvian,

Let me suggest analyzing what case0 or my_case0 does but removing
the definitions of idProp and IDProp and False_ind and expliciting
the dependent pattern matching at play

(*----------------------*)

Section Vector_0_rect.

  Notation "[]" := (nil _).

  Variable (A : Type)
           (P : t A 0 -> Type) 
           (P_empty : P (nil _)).

  (* Return type for dep. pattern matching *)

  Let rtype X {n} : t A n -> Type :=
    match n with 
      | 0 => fun v => P v 
      | _ => fun _ => X
    end.

  Definition Vector_0_rect (v : t A 0) : P v := 
    match v as v' return rtype unit v' with
      | [] => P_empty
      | _  => tt
    end.

  Definition Vector_0_rect' (v : t A 0) : P v := 
    match v as v' return rtype (Empty_set -> unit) v' with
      | [] => P_empty
      | _  => fun C => match C with end
    end.

End Vector_0_rect.

(*---------------------------*)

It should be clear here why the _ case
in Vector_0_rect or Vector_0_rect' type-checks. 

The reason for preferring the

"match C with end" where C : Empty_set

for instance is that it also gives a term
compatible with the guard checker (structural
decrease). 

Best regards,

Dominique


----- Mail original -----
> De: "Sylvain Salvati" <sylvain.salvati AT univ-lille.fr>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Vendredi 11 Mars 2022 08:59:09
> Objet: [Coq-Club] Type checking in the Vector library

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