The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Tue, Mar 19, 2019 at 10:36 AM Alix Trieu <alix.trieu AT cs.au.dk> wrote:

CompCert provides a formalization of machine integers you might be interested to look at: https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v

Actually, this formalization follows the same approach proposed by the original poster, using a subset of Z:

Definition unsigned (max:Z) : Set :=
  { x : Z | x >= 0 /\ x < max}.
Definition unsigned_8 := unsigned (2^8).
 

A nice property of this approach is that it computes relatively efficiently (like type Z) while the Fin.t type does not (like type nat).

To have a good notion of equality over type "unsigned" above, it's better to define it this way:

Definition unsigned (max:Z) : Set :=
  { x : Z | -1 < x /\ x < max}.

so that proofs of the proposition "-1 < x /\ x < max" are unique.

Have fun,

- Xavier Leroy

> On 18 Mar 2019, at 15:10, fritjof AT uni-bremen.de wrote:
>
> Hi,
>
> I want to create a finite data type, like *Unsinged 8*,
> which containes values from 0 to 2^8 -1.
> I came up with an idea like:
>
> Definition unsigned (max:Z) : Set :=
>  { x : Z | x >= 0 /\ x < max}.
>
> Definition unsigned_8 := unsigned (2^8).
>
> But I'm not sure, if this is the right way.
>
> Does someone know if there is a better way to define
> finite types?
>
> --f.
>