The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

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

Isn't that also true with "x >= 0 /\ x < max"?

Gaëtan Gilbert

On 19/03/2019 16:54, Xavier Leroy wrote:
> On Tue, Mar 19, 2019 at 10:36 AM Alix Trieu <alix.trieu AT cs.au.dk 
> <mailto: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
>     
> <mailto: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.
>      >