The Coq mailing list

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

Dear Michael,

It seems to me that Fin n is the type of numbers (nat) below n,
hence the equivalence:

  Fin n ~=~ { i : nat | i < n }.

Hence Fin 0 has to be an empty type. Fin n is defined
in the Coq Vectors.Fin module of the Standard Library.

Best,

D.


Le 15/09/2017 à 12:05, Soegtrop, Michael a écrit :
> Dear Jeff,
> 
> I wonder what is the advantage of using a definition of Fin n which is 
> equivalent to False for n=0 in connection with Vectors which exist for n=0. 
> What bad things would happen if Fin 0 would be defined and equivalent to a 
> 0-tuple of unit rather than something which doesn't exist at all? Is the 
> fact that Fin 0 -> False used for ex falso quod libet proofs in some 
> places? Since the 0 length constructor of vectors is trivial I don't see 
> many applications for this. So unless you really need ex falso quod libet 
> proofs using Fin 0 somewhere, I have doubts that this is the most efficient 
> (in terms of human time to get things done) way of setting up things.
> 
> Best regards,
> 
> Michael
> 
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928
>