coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] finite data types

From: Alix Trieu <alix.trieu AT cs.au.dk>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] finite data types
Date: Tue, 19 Mar 2019 09:31:52 +0000
Accept-language: fr-FR, da-DK, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=alix.trieu AT cs.au.dk; spf=Pass smtp.mailfrom=alix.trieu AT cs.au.dk; spf=Pass smtp.helo=postmaster AT EUR01-DB5-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:aY6hAh0EpAc5gFb1smDT+DRfVm0co7zxezQtwd8ZseIQLPad9pjvdHbS+e9qxAeQG9mCs7Qc0qL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHOfwlEniaxba5vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDkJOSMl8G/ZicJwgqBUoBO9qBJwzIHZe52VNON7fq/BYd8WWXRNU8BMXCJBGIO8aI4PAvIdMOZcron8qEYFowWkBQmtGuzv1yJDi3js0q0+0uQgHhvK3BA6H9IPrnvUsc74O7sJUeyv1qbI0C/PYO5V2Trk7oXDbx4vofaJXb1qcMrRz1EiFwzEjlWMqYzlIiia2v4RvGic6uptU/+khW0/qwxprTWj2t0ghpTVio8X0FzI6CV0zJw1KNC7UEJ3fMKoHIFNuyyYLYd7RsAvT3t1tCs6xbAKoZC7czYJxZg7whPSbuCIfouV7h/gUeueOzh1iXxhdb+6mhq97FSsx+P5W8apzlpHrSpIn9/RvX4XzRPT8NKISv5l80ehxzmP0wfT5/lLL086iaTXN4Mtzqc+mJcOsUnPByj2l17og6OMcUUk5/So5P/gYrX7oJ+TKpV4ihnkMqQphsywH/g3MhQPX2ic/+Swzrrj/VDlQLVOif02larZvIrGKsQco661Gw5V0oA95BajFzqr38gUkWMaIF5Zeh+LlZXlNlHULP34Dvqzm1Gsny1qx/DCML3hGJLNLn3bnbj7ebZ96kFdxBAvzdBF5pJbFKwBLenvVU/qrtDXFAI5PxapzObkENl9zJ8RWXqTAq+FN6PfqUOH5uU2I+WVeIAVvCv9JOM+6v71jX45nEcdcrOz0ZsWbnC4BPVmLF+DbXrimNdSWVsN60A1S/Wvg1mfWxZSYWyzVuQy/HtzXImhFMLIQp2nqL2HxiayWJNMMDNoEFeJRF7sdpXMZ+0NZT/adsZlkyxCSaKgRpIJ3grovRK8x7kxfbmcwTERqZ+2jIs93ObUjxxnrWUlXfTY6HmESiRPpk1NQjY32K5lpkkkkgWIyu5xnrpUFo4Kvq8bYkIBLZfZitdCJZXqQAuYJoWCUxCvX5OqAmNpF49j85o1e094Xu6aoFXD0i6tX+BHuoGxXMVx3oiBmn/7KoB61mrM07Qngx8+WMxTOGa6h6l5sQ/OG4rOlEbfnKGvJ/0R

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

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

[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