coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] finite data types

From: fritjof AT uni-bremen.de
To: coq-club AT inria.fr
Subject: [Coq-Club] finite data types
Date: Mon, 18 Mar 2019 15:10:39 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=SoftFail smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT lnv-91185.sb.dfki.de
Ironport-data: A9a23:Yv2tWqPv3QrQArrvrXNrnJaSY/KYJRDQNY6hA5uTyZEnxcOdPwc1ko NxE7Ho0HSaGSYHDeYRym7LVPUZlMFSpvJYjFDEvnM9O0iUV8ub2y/XwCaXoygLRhx/H/MDlE YBpNhtkBsVFg8sV7mTFQzjpHHutYrdpIh2zDV+pMQgi+zGZkjcEE1rPIGQ8u6+jMgsx1cBfb QqVlYBvi/ow3jhG6FPJ0batOn0Xsn4QCUB02NssQnH7CjVqQFzfBpS9li0kuUsV9hJTJFXOd 6bmmlLYae3WRvb1+wr8jgXBl3f76V2DZCqoFu963B2DmlmD976+yhBkQNs0IeTHrFxnWtYj3 JUf3p1k8uOPzE0+DO2cPgkd/52fhwu/7mOdQtgdRZIJPijIgcDnpVwb9cvHZHypSGoFL0ewH onuC5Ax6XLheBVo16RNzHrdHmQqq98HrM3/9Bt2Rx6VB9gXmlHbgi/cHx0ptcxQ+AdZ8jBbR IVgxesNORAwmNtJcU9RHdqdgSEC9NuerWMr5HBm7Rl6mX6dEJJi2zr8hMW6nTJFwrMlXiB52 nyFbHIjUxIaREfyL7+k+XVSUCCFYgL8Kla3o+qKr6ESSKmndCrqe1wV7Zr0dUate0wPzG6TG OsBDSDhOvJBW+1kgCzyQlwgZpjL5QTbtNw0y57EZHZBB7KeaQHzKrDWpkDdqG6sX8wWvmrGY oPAaROIsv7CzIe9jUPd0RLGogJxPNAvsfE5u0thRkHpViW2z8mUV1TzVJju9uoKlGnTsaXMl S3+1cOhyugO+iUi3bKLoZgo6xAuTgoHefUR8fNr4N6FbBkJqTLN9xDIidjWoJ2SZAUhcuGyG 4nt1tEo6Wa8FfjZoV53PK7C/JFZXmIBKT4hLuMTMR7Wyze7yyKtJXiCNeI+W7s7MYRccetkr VylJM6DSljqqnGBcc=
Ironport-phdr: 9a23:7rYjNhbUXcjOEGk6KHJ7XIL/LSx+4OfEezUN459isYplN5qZocS7bn LW6fgltlLVR4KTs6sC17OO9fi5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7Fs kRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCehbb9oMB m6sBjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3Tb pDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8q xlSgLniD0fOjA38G/ZlNF+gqFUrx29uhNy2JLUbJ2POfZiYq/RYdEXSGxcVchRTSxBBYa8Yp MBD+obPOZYs4v9p1wArRalGAmsAuLvxiZTiX/sw6I61vouEQfc0AM9Ad0DtmnfotbtNKoKTO y4wqbFwS/HYv5Xwzvx9YzFfg07rf2RXr99cdLdxVQhGg7KlFmctJDpMy2P2ugTrmSW7PBsWf yyh2MkrQx6vyKhyd02iobTg4IY0lDE+jt9wIYyPdC4TEh7YcC9HJZUqi2WKoh7T8M4T2Fzoy k20KAJuZC4fCgL0pgo2gDQZ+SGc4iO/B3jSP6cLSp2iX9qYr6ygxe//VK9xuD4S8W4yktGoy lFn9XUs3ACzR3T6syJSvtn+Ueh3C6C1w7J6uFFPUA0l63bK5A6z74tkJoTsF3PETTsmEroia +ZaEMk9vK15Ov5ernmvIOTN5doigHiNaQjgtCwAeMhMgQXQ2eb/fm826b48E3iQLRKi+U2nb PDvJDbI8QbvK+5DBVP3oYt8RbsRwuhhd8fhDwMKE9PUBOBlYngfV/Uc97iCvLqjU6tjDVsyd jbOLykCI/AK3XF1rvsLuU10FJV1AdmlYMX3JlTELxUeKuvCH+0j8TRC1oCCyLx2/zuUYgvy4 UfHGiVD6qUNuXevA3Qv7N9E6y3fIYQ/Q3FBb0g7v/qg2U+nAZAL7Sv3N4dcn29E/IgL0jLOi Ox0OdEKn8Du08FdMKviFCGVmQJNXK0Qedtv2hrVcS9B8HPSIOsxrCMjn+2

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.

[Coq-Club] finite data types, fritjof, 03/18/2019
- Re: [Coq-Club] finite data types, Mario Alvarez Picallo, 03/18/2019
- Re: [Coq-Club] finite data types, Jan Bessai, 03/18/2019
- Re: [Coq-Club] finite data types, Maximilian Wuttke, 03/18/2019
  - Re: [Coq-Club] finite data types, Gregory Malecha, 03/19/2019
- Re: [Coq-Club] finite data types, Alix Trieu, 03/19/2019
  - Re: [Coq-Club] finite data types, Xavier Leroy, 03/19/2019
    - Re: [Coq-Club] finite data types, Gaëtan Gilbert, 03/19/2019
      - Re: [Coq-Club] finite data types, Xavier Leroy, 03/19/2019
        
        Re: [Coq-Club] finite data types, Fritjof Bornebusch, 03/20/2019
        
        Re: [Coq-Club] finite data types, Emilio Jesús Gallego Arias, 03/20/2019