The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

I think the coq-bbv opam package provides many definitions about a dependent representation of bitvectors. Unfortunately, storing indicies can be quite costly, so if you are going to do a lot of computation, the definition that you have is actually faster.

On Mon, Mar 18, 2019 at 10:36 AM Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de> wrote:

For the finite type of numbers `0,...,n-1` there already is `Fin.t n` in
Coq's standard library. [1]
It is a classical example for a dependent inductive type.
However, this type can be quite tricky for beginners.

I have heard of implementations of machine integers (like unsigned 8),
but I currently don't have a link.


For general *finite types*, you can do something like

```
Require Import List.

Class finite (X:Type) :=
  {
    enum : list X;
    enum_complete : forall (x:X), In x enum;
  }.

Instance finite_unit : finite unit :=
  {| enum := cons tt nil |}.
Proof. abstract now intros []; constructor. Defined.
```


[1] https://coq.inria.fr/distrib/current/stdlib/Coq.Vectors.Fin.html


Sincerely
Maximilian


On 18/03/2019 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.
>

--

gregory malecha

gmalecha.github.io