The Coq mailing list

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

On Tue, Mar 19, 2019 at 5:37 PM Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

 > 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"?

Sadly, no.  "x >= 0" is defined as "Z.compare x 0 <> Lt", i.e. the negation of "Z.compare x 0 = Lt".  Proofs of a negation ~P are functions, so you cannot show that there is only one proof of ~P, even if there is only one proof of P.  Unless you assume function extensionality, of course.

So, "-1 < x", which expands to "Z.compare (-1) x = Lt", has unique proofs, but "0 <= x" or "x >= 0" does not...

With my thanks to Robbert Krebbers, who pointed out all this to me a while ago,

- Xavier Leroy

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